Research Papers

    2019
  1. C.Schwaab, E.Komendantskaya, A.Hill, F.Farka, J.Wells, R.Petrick, K.Hammond. Proof-Carrying Plans. PADL 2019, 14-15 January 2019, Cascais/Lisbon, Portugal.
  2. 2018
  3. E.Komendantskaya and J.Power. Logic programming: laxness and saturation. Journal of Logic and Algebraic Methods in Programming. 36 pages, 2018.
  4. F.Farka, E.Komendantskaya and H.Hammond Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis. International Conference on Logic Programming ICLP'18, FLoC'18, 14-17 July 2018, Oxford. To appear in the journal of Theory and Practice of Logic Programming.
  5. A.Hill and E.Komendantskaya Automation by Analogy, in Coq. 3rd Conference on Artificial Intelligence and Theorem Proving AITP 2018 Aussois, France, 25 - 30 March 2018.
  6. 2017
  7. E.Komendantskaya and Y.Li Productive Corecursion in Logic Programming. International Conference on Logic Programming ICLP'17, 28-31 August 2017, Melbourne. Selected papers published in J. of Theory and Practice of Logic Programming TPLP 17(5-6): 906-923. 2017.
  8. P.Fu and E.Komendantskaya. Operational Semantics of Resolution and Productivity in Horn Clause Logic. Journal ``Formal Aspects of Computing", 29(3): 453-474, 2017. Project's webpage.
  9. E.Komendantskaya and J.Heras Proof Mining with Dependent Types, CICM'17 in Edinburgh, 17-21 July 2017, Edinburgh. LNCS 10383: 303-318, 2017.
  10. L.Franceschini, D.Ancona and E.Komendantskaya. Structural Resolution for Abstract Compilation of Object-Oriented Languages. Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types, CoALP-Ty 2016, Edinburgh, UK, 28-29 November 2016. EPTCS 258, 2017. See also MSc thesis of L.Franceschini, U.Genova, 2016.
  11. 2016
  12. E.Komendantskaya, J.Power and M.Schmidt. Coalgebraic Logic Programming: from Semantics to Implementation. Journal of Logic and Computation, 26(2), 745-783, 2016. CoALP's mini-page.
  13. F.Farka, E.Komendantskaya, K.Hammond and P.Fu. Coinductive Soundness of Corecursive Type Class Resolution. Pre- and post- proceedings of LOPSTR'16, Edinburgh, UK.
  14. E.Komendantskaya, P.Johann and M.Schmidt. A Productivity Checker for Logic Programming. Pre- and post- proceedings of LOPSTR'16, Edinburgh, UK.
  15. E.Komendantskaya and J.Power. Category theoretic semantics for theorem proving in logic programming: embracing the laxness. Coalgebaric methods in Computer Sceince (CMCS'16): Revised selected papers. Lecture Notes in Computer Science 9608, 94--113, 2016. Project's webpage.
  16. P.Fu, E.Komendantskaya, T.Schrijvers, A.Pond. Proof Relevant Corecursive Resolution FLOPS'2016, Japan, 3-6 March 2016. Springer LNCS 9613, 126-143. Project's webpage.
  17. 2015
  18. P.Fu and E.Komendantskaya. A Type Theoretic Approach to Resolution. LOPSTR 2015: Revised and Selected papers, Lecture Notes in Computer Science 9527, pages 91--106.
  19. C.Warburton and E. Komendantskaya Scaling Automated Theory Exploration. Workshop AI4FM, Edinburgh, 2015.
  20. 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.
  21. P. Johann, E. Komendantskaya and V.Komendantskiy. Structural Resolution for Logic Programming. Technical Communications of ICLP 2015. Project's webpage.
  22. P.Fu and E.Komendantskaya. A Type Theoretic Approach to Structural Resolution. Pre-proceedings of LOPSTR 2015. Project's webpage.
  23. 2014
  24. J. Heras and E. Komendantskaya. Proof-Pattern Search in Coq/SSReflect. Proceedings Coq Workshop, FLoC 2014. Electronic Proceedings in Theoretical Computer Science, pp. 61-75, 2014.
  25. J. Heras and E. Komendantskaya. ACL2(ml): Machine-Learning for ACL2. Proceedings ACL2 Workshop, FLoC 2014.
  26. 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.
  27. J.Heras, E.Komendantskaya, Recycling Proof Patterns in Coq: Case Studies. Mathematics in Computer Science 8(1): 99-116 (2014). Arxiv version. ML4PG page.
  28. 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
  29. 2013
  30. 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.
  31. 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.
  32. 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.
  33. J.Heras and E.Komendantskaya. Statistical Proof Pattern Recognition: Automated or Interactive? (slides), the 20th Automated Reasoning Workshop (ARW'13), 11-12 April 2013.
  34. 2012
  35. 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.
  36. 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.
  37. 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.
  38. E.Komendantskaya. Machine-Learning Coalgebraic Proofs. Post-proceedings of the International Conference on Inductive Logic Programming'11, Windsor, UK. Imperial College Tech. Report.
  39. 2011
  40. 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.
  41. E.Komendantskaya and J.Power. Coalgebraic derivations in logic programming. International conference Computer Science Logic, CSL'11. LIPICS proceedings, Vol 12, pp.352-366.
  42. 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.
  43. 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.
  44. 2010
  45. 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.
  46. 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.
  47. 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.
  48. 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.
  49. E.Komendantskaya. Unification Neural Networks: Unification by Error-Correction Learning. Logic Journal of the IGPL (Oxford Journals) 19(6): 821-847 (2011)
  50. 2009
  51. E.Komendantskaya. Neurons OR Symbols: Why Does OR Remain Exclusive? Position paper. Proceedings of the International Conference on Neural Computation (ICNC), 2009.
  52. E.Komendantskaya. Parallel Rewriting in Neural Networks. Proceedings of the International Conference on Neural Computation (ICNC), 2009.
  53. Y.Bertot and E.Komendantskaya. Using Structural Recursion for Corecursion TYPES'08 LNCS 5497, Springer, 2009; pages 220-236.
  54. E.Komendantskaya. Intermediate three -valued regular logics of Kleene(In Russian) Logic Studies, 15: 116-128. 2009. Editor: A.S.Karpenko. Moscow.
  55. 2008, Postdoctoral Year in INRIA, France
  56. 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.
  57. 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.
  58. 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.
  59. 2007, Year-3 of PhD
  60. 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.
  61. 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.
  62. 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.
  63. 2006, Year-2 of PhD
  64. 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.
  65. 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.
  66. 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.
  67. 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.
  68. 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.
  69. 2005, Year-1 of PhD
  70. 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.
  71. 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.
  72. Before PhD
  73. 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.
  74. E. Komendantskaya. Kleene Regular Intermediate Three-Valued Logics. Proceedings of Smirnov Readings, 4th Interantional Conference. IPhRAS, 2003, p.80--82.