Research Papers

    2016
  1. E.Komendantskaya and J.Power. Category theoretic semantics for theorem proving in logic programming: embracing the laxness. Coalgebaric methods in Computer Sceince (CMCS'16). Project's webpage.
  2. P.Fu, E.Komendantskaya, T.Schrijvers, A.Pond. Proof Relevant Corecursive Resolution Accepted to FLOPS'2016, Japan, 3-6 March 2016. Project's webpage.
  3. 2015
  4. E.Komendantskaya and P.Johann. Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic. Submitted to ACM Transcations in Computational Logic. 36 pages, November 2015. Project's webpage.
  5. P.Fu and E.Komendantskaya. A Type Theoretic Approach to Resolution. LNCS post-proceedings of LOPSTR 2015. Project's webpage.
  6. C.Warburton and E. Komendantskaya Scaling Automated Theory Exploration. Workshop AI4FM, Edinburgh, 2015.
  7. E. Komendantskaya, P. Fu and P. Johann. Structural Resolution for Automated Verification, "Ideas paper"; 15th International Workshop on Automated Verification of Critical Systems AVOCS'15, Edinburgh. Project's webpage.
  8. P. Johann, E. Komendantskaya and V.Komendantskiy. Structural Resolution for Logic Programming. Technical Communications of ICLP 2015. Project's webpage.
  9. P.Fu and E.Komendantskaya. A Type Theoretic Approach to Structural Resolution. Pre-proceedings of LOPSTR 2015. Project's webpage.
  10. 2014
  11. J. Heras and E. Komendantskaya. Proof-Pattern Search in Coq/SSReflect. Proceedings Coq Workshop, FLoC 2014.
  12. J. Heras and E. Komendantskaya. ACL2(ml): Machine-Learning for ACL2. Proceedings ACL2 Workshop, FLoC 2014.
  13. J.Heras, E.Komendantskaya and M.Schmidt. (Co)recursion in Logic Programming: Lazy versus Eager. Technical Communications of International Conference on Logic Programming (ICLP'14) at FLoC'14. Benchmarks for this paper. CoALP's mini-page.
  14. J.Heras, E.Komendantskaya, Recycling Proof Patterns in Coq: Case Studies. Mathematics in Computer Science 8(1): 99-116 (2014). Arxiv version. ML4PG page.
  15. E.Komendantskaya, M.Schmidt and J.Heras. Exploiting Parallelism in Coalgebraic Logic Programming. Electr. Notes Theor. Comput. Sci. 303: 121-148 (2014). CoALP's mini-page
  16. E.Komendantskaya, J.Power and M.Schmidt. Coalgebraic Logic Programming: from Semantics to Implementation. Journal of Logic and Computation, 2014, 40 pages. CoALP's mini-page.
  17. 2013
  18. J.Heras, E.Komendantskaya, M.Johansson, and E.Maclean. Proof-Pattern Recognition and Lemma Discovery in ACL2 LPAR'13, Stellenbosch, South Africa, 15th-19th December 2013. LNCS 8312, pp. 389-406, 2013.
  19. E.Komendantskaya, J.Heras and G.Grov. Machine-Learning for Proof General: interfacing interfaces. Post-proceedings of User Interfaces for Theorem Provers (UITP 2012), EPTCS, vol. 118, pp. 15-41, 2013. ML4PG has its own page: here.
  20. J.Heras and E.Komendantskaya. ML4PG in Computer Algebra Verification. Systems & Projects session of CICM 2013. Lecture Notes in Computer Science, vol. 7961, pp. 354-358, 2013. Arxiv version.
  21. J.Heras and E.Komendantskaya. Statistical Proof Pattern Recognition: Automated or Interactive? (slides), the 20th Automated Reasoning Workshop (ARW'13), 11-12 April 2013.
  22. 2012
  23. E.Komendantskaya, J.Power and M.Schmidt. Coalgebraic Logic Programming: implicit versus explicit resource handling. Workshop on Coinductive Logic Programming at ICLP'12, Budapest, September 2012. Slides are available here.
  24. E.Komendantskaya and K.Lichota. Neural Networks for Proof-Pattern Recognition. International Conference on Artificial Neural Networks, ICANN'12, September 2012, Lausanne, Switzerland. Lecture Notes in Computer Science, vol. 7553, pp. 427-434, 2012. The supporting documentation and data sets are available here.
  25. G.Grov, E.Komendantskaya and A.Bundy. A Statistical Relational Learning Challenge - extracting proof strategies from exemplar proofs. ICML'12 worshop on Statistical Relational Learning, Edinburgh, 30 July 2012.
  26. E.Komendantskaya. Machine-Learning Coalgebraic Proofs. Post-proceedings of the International Conference on Inductive Logic Programming'11, Windsor, UK. Imperial College Tech. Report.
  27. 2011
  28. E.Komendantskaya and Q.Zhang. SHERLOCK - An Inteface for Neuro-Symbolic Networks. NeSy version, longer version. The software package is available here. System presentation at NeSy'11 workshop at ECAI'11. CEUR Workshop Proceedings.
  29. E.Komendantskaya and J.Power. Coalgebraic derivations in logic programming. International conference Computer Science Logic, CSL'11. LIPICS proceedings, Vol 12, pp.352-366.
  30. E.Komendantskaya and J.Power. Coalgebraic semantics for derivations in logic programming. International conference on Algebra and Coalgebra CALCO'11. Springer LNCS 6859, pp. 268-282.
  31. E.Komendantskaya and J.Power. Coalgebraic proofs in logic programming. Proceedings of the 18th Workshop on Automated Reasoning, Dept of Computing Science, University of Glasgow (Tech Report), 2011.
  32. 2010
  33. A.Bove, E. Komendantskaya and M.Niqui. Proceedings of the PAR'10 workshop on Partiality and Recursion at FLoC'10. Edinburgh, UK. Electronic Proceedings in Theoretical Computer Science. 2010.
  34. E. Komendantskaya, K. Broda and A. d'Avila Garcez. Neuro-Symbolic Representation of Logic Programs Defining Infinite Sets. In K. Diamantaras, et al.(Eds.): ICANN 2010, Part I, LNCS 6352, Springer, pp.301-304.
  35. Ekaterina Komendantskaya, Guy McCusker and John Power. Coalgebraic semantics for parallel derivation strategies in logic programming. Proceedings of AMAST'2010 - 13th International Conference on Algebraic Methodology and Software Technology (AMAST2010), 23-25 June 2010, Manoir St-Castin Quebec, Canada. Lecture Notes in Computer Science, 6486, pp. 111-127, 2011.
  36. Ekaterina Komendantskaya, Krysia Broda and Artur d'Avila Garcez. Using Inductive Types for Ensuring Correctness of Neuro-Symbolic Computations. Proceedings of CiE'2010 - Computability in Europe 2010 - Programs, Proofs, Processes. Ponta Delgada, Portugal, 30 June - 4 July 2010.
  37. E.Komendantskaya. Unification Neural Networks: Unification by Error-Correction Learning. Logic Journal of the IGPL (Oxford Journals) 19(6): 821-847 (2011)
  38. 2009
  39. E.Komendantskaya. Neurons OR Symbols: Why Does OR Remain Exclusive? Position paper. Proceedings of the International Conference on Neural Computation (ICNC), 2009.
  40. E.Komendantskaya. Parallel Rewriting in Neural Networks. Proceedings of the International Conference on Neural Computation (ICNC), 2009.
  41. Y.Bertot and E.Komendantskaya. Using Structural Recursion for Corecursion TYPES'08 LNCS 5497, Springer, 2009; pages 220-236.
  42. E.Komendantskaya. Intermediate three -valued regular logics of Kleene(In Russian) Logic Studies, 15: 116-128. 2009. Editor: A.S.Karpenko. Moscow.
  43. 2008, Postdoctoral Year in INRIA, France
  44. E.Komendantskaya and J.Power. Fibrational Semantics for Many-Valued Logic Programs: Grounds for Non-Groundness. Proceedings of JELIA'08, 28 September - 1 October 2008, Dresden, Germany. LNCS 5293, pages 258-271.
  45. E.Komendantskaya. Unification by Error-Correction, Proceedings of NeSy'08 workshop at ECAI'08, 21-25 July 2008, Patras, Greece. CEUR Workshop Proceedings, Vol. 366, 2008. ISSN 1613-0073.
  46. Y. Bertot and E. Komendantskaya. Inductive and Coinductive Components of Corecursive Functions in Coq, Proceedings of CMCS'08, the 9th International Workshop on Coalgebraic Methods in Computer Science, Budapest, Hungary, April 4 - April 6, 2008. ENTCS 203/5 pp.25--47, 2008.
  47. 2007, Year-3 of PhD
  48. E Komendantskaya. A Sequent Calculus for Bilattice-Based Logics and its Many-Sorted Representation. In Automated Reasoning with Analytic TABLEAUX and Related Methods, N.Olivetti, ed.; Proceedings of the 16th International Conference TABLEAUX'2007, Aix en Provence, France, 3-6 July, 2007; LNAI 4548, Springer, pages 165-182.
  49. E. Komendantskaya, M. Lane and A. Seda. Connectionist Representation of Multi-Valued Logic Programs, 2007. In Perspectives of Neural-Symbolic Integration, Barbara Hammer and Pascal Hizler, eds, in Springer Series Computational Intelligence, editor-in-chief Janusz Kacprzyk; pages 259-289.
  50. E. Komendantskaya. First-order Deduction in Neural Networks, In pre-Proceedings of LATA'07, the 1st Conference on Language and Automata Theory and Applications, March 29--April 4, 2007, Tarragona, Spain; pages 307-318.
  51. 2006, Year-2 of PhD
  52. E. Komendantskaya and A. K. Seda. Sound and Complete SLD-resolution for Bilattice-Based Annotated Logic Programs. Electr. Notes Theor. Comput. Sci. 225: 141-159 (2009). Postproceedings volume of the 4th Irish Conf. on Mathematical Foundations of Computer Science and Information Technology (MFCSIT'06), Cork, Ireland, August 1-5, 2006.
  53. E. Komendantskaya and A. K. Seda. Logic Programs with Uncertainty: Neural Computations and Automated Reasoning. In Logical Approaches to Computational Barriers, Proc. of the 2nd Conference on Computability in Europe, A. Beckmann, U. Berger, B. Lowe, J.V.Tucker, eds., CiE 2006, Swansea, UK, June/July 2006; pp. 170-182.
  54. E. Komendantskaya and V. Komendantsky. On Uniform Proof-Theoretical Operational Semantics for Logic Programming. In Perspectives on Universal Logic, J.-Y. Beziau and A.~Costa-Leite, editors, Post-Proceedings volume of the 1st World Congress on Universal Logic (UNILOG-05), 26 March -- 3 April, 2005, Montreux, Switzerland, 2006. Publisher: Polimetrica, Monza, Italy. 16~pages. In print. Available as a BCRI pre-print.
  55. E. Komendantskaya. Many-Sorted Semantics for Many-Valued Annotated Logic Programs. Proc. 4th Irish Conf. Mathematical Foundations of Computer Science and Information Technology (MFCSIT'06), Cork, Ireland, August 1-5, 2006, pp. 225--229.
  56. E. Komendantskaya and A.Seda. Operational Semantics for Bilattice-Based Annotated Logic Programs. Proc. 4th Irish Conf. Mathematical Foundations of Computer Science and Information Technology (MFCSIT'06), Cork, Ireland, August 1-5, 2006, pp. 229--233.
  57. 2005, Year-1 of PhD
  58. E. Komendantskaya, A. K. Seda, and V. Komendantsky. On Approximation of the Semantic Operators Determined by Bilattice-Based Logic Programs. In Proc. 7th International Workshop on First-Order Theorem Proving (FTP'05), pages 112--130, Koblenz, Germany, September 15--17, 2005.
  59. E. Komendantskaya and V. Komendantsky. Uniform Operational Semantics of Logic Programming and Sequent Calculus. Proceedings of the 1st World Congress on Universal Logic (UNILOG-05), 26 March -- 3 April, 2005, Montreux, Switzerland, 2006. pp.73--74.
  60. Before PhD
  61. E. Komendantskaya. Non-Commutative Many-Valued Functions. Proceedings of the XI International Conference for Undergraduate and Graduate Students and Young Scientists "Lomonosov", 12--15 April 2004, Moscow, Russia; pp. 419--421.
  62. E. Komendantskaya. Kleene Regular Intermediate Three-Valued Logics. Proceedings of Smirnov Readings, 4th Interantional Conference. IPhRAS, 2003, p.80--82.