Sound and Complete SLD-Resolution for Bilattice-Based Annotated Logic Programs. - Ekaterina Komendantskaya; Anthony Karel Seda (MFCSIT, 2006)

First-order deduction in neural networks. - Ekaterina Komendantskaya (LATA, 2007)

A Sequent Calculus for Bilattice-Based Logic and Its Many-Sorted Representation. - Ekaterina Komendantskaya (TABLEAUX, 2007)

Connectionist Representation of Multi-Valued Logic Programs. - Ekaterina Komendantskaya; Máire Lane; Anthony Karel Seda (Perspectives of Neural-Symbolic Integration, 2007)

Fibrational Semantics for Many-Valued Logic Programs: Grounds for Non-Groundness. - Ekaterina Komendantskaya; John Power (JELIA, 2008)

Unification by Error-Correction. - Ekaterina Komendantskaya (NeSy, 2008)

Using Structural Recursion for Corecursion. - Yves Bertot; Ekaterina Komendantskaya (TYPES, 2008)

Inductive and Coinductive Components of Corecursive Functions in Coq. - Yves Bertot; Ekaterina Komendantskaya (CMCS, 2008)

Parallel Rewriting in Neural Networks. - Ekaterina Komendantskaya (IJCCI, 2009)

Neurons or Symbols - Why does OR Remain Exclusive?. - Ekaterina Komendantskaya (IJCCI, 2009)

Coalgebraic Semantics for Parallel Derivation Strategies in Logic Programming. - Ekaterina Komendantskaya; Guy McCusker; John Power (AMAST, 2010)

Neuro-symbolic Representation of Logic Programs Defining Infinite Sets. - Ekaterina Komendantskaya; Krysia Broda; Artur S. d'Avila Garcez (ICANN (1), 2010)

Coalgebraic Semantics for Derivations in Logic Programming. - Ekaterina Komendantskaya; John Power (CALCO, 2011)

Coalgebraic Derivations in Logic Programming. - Ekaterina Komendantskaya; John Power (CSL, 2011)

Machine Learning Coalgebraic Proofs. - Ekaterina Komendantskaya (ILP (Late Breaking Papers), 2011)

SHERLOCK - An Interface for Neuro-Symbolic Networks. - Ekaterina Komendantskaya; Qiming Zhang (NeSy, 2011)

Unification neural networks: unification by error-correction learning. - Ekaterina Komendantskaya (Log. J. IGPL, 2011)

Neural Networks for Proof-Pattern Recognition. - Ekaterina Komendantskaya; Kacper Lichota (ICANN (2), 2012)

Machine Learning in Proof General: Interfacing Interfaces - Ekaterina Komendantskaya; Jónathan Heras; Gudmund Grov (UITP, 2012)

Proof-Pattern Recognition and Lemma Discovery in ACL2. - Jónathan Heras; Ekaterina Komendantskaya; Moa Johansson; Ewen Maclean (LPAR, 2013)

ML4PG in Computer Algebra Verification. - Jónathan Heras; Ekaterina Komendantskaya (MKM/Calculemus/DML, 2013)

Proof-Pattern Recognition in ACL2. - Jónathan Heras; Ekaterina Komendantskaya; Moa Johansson; Ewen Maclean (CoRR, 2013)

Statistical Proof-Patterns in Coq/SSReflect - Jónathan Heras; Ekaterina Komendantskaya (CoRR, 2013)

ML4PG: proof-mining in Coq - Jónathan Heras; Ekaterina Komendantskaya (CoRR, 2013)

Statistical Proof Pattern Recognition: Automated or Interactive? - Jónathan Heras; Ekaterina Komendantskaya (CoRR, 2013)

Exploiting Parallelism in Coalgebraic Logic Programming. - Ekaterina Komendantskaya; Martin Schmidt 002; Jónathan Heras (WACT, 2013)

Proof Pattern Search in Coq/SSReflect. - Jónathan Heras; Ekaterina Komendantskaya (CoRR, 2014)

HoTT formalisation in Coq: Dependency Graphs & ML4PG. - Jónathan Heras; Ekaterina Komendantskaya (CoRR, 2014)

ACL2(ml): Machine-Learning for ACL2. - Jónathan Heras; Ekaterina Komendantskaya (ACL2, 2014)

Guarding (Co)Recursion in Coalgebraic Logic Programming. - Jónathan Heras; Ekaterina Komendantskaya; Martin Schmidt 002 (CoRR, 2014)

Recycling Proof Patterns in Coq: Case Studies. - Jónathan Heras; Ekaterina Komendantskaya (Math. Comput. Sci., 2014)

Structural Resolution for Logic Programming. - Patricia Johann; Ekaterina Komendantskaya; Vladimir Komendantskiy (ICLP (Technical Communications), 2015)

A Type-Theoretic Approach to Resolution. - Peng Fu 001; Ekaterina Komendantskaya (LOPSTR, 2015)

A Type-Theoretic Approach to Structural Resolution. - Peng Fu 001; Ekaterina Komendantskaya (CoRR, 2015)

Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic. - Ekaterina Komendantskaya; Patricia Johann (CoRR, 2015)

Category Theoretic Semantics for Theorem Proving in Logic Programming: Embracing the Laxness. - Ekaterina Komendantskaya; John Power (CMCS, 2016)

Proof Relevant Corecursive Resolution. - Peng Fu 001; Ekaterina Komendantskaya; Tom Schrijvers; Andrew Pond (FLOPS, 2016)

Coinductive Soundness of Corecursive Type Class Resolution. - Frantisek Farka; Ekaterina Komendantskaya; Kevin Hammond (LOPSTR, 2016)

A Productivity Checker for Logic Programming. - Ekaterina Komendantskaya; Patricia Johann; Martin Schmidt 002 (LOPSTR, 2016)

Operational Semantics of Resolution in Horn Clause Logic. - Peng Fu 001; Ekaterina Komendantskaya (CoRR, 2016)

Coinductive Soundness of Corecursive Type Class Resolution. - Frantisek Farka; Ekaterina Komendantskaya; Kevin Hammond; Peng Fu 001 (CoRR, 2016)

CoALP-Ty'16. - Ekaterina Komendantskaya; Frantisek Farka (CoRR, 2016)

Structural Resolution for Abstract Compilation of Object-Oriented Languages. - Luca Franceschini; Davide Ancona; Ekaterina Komendantskaya (CoALP-Ty, 2016)

Coalgebraic logic programming: from Semantics to Implementation. - Ekaterina Komendantskaya; John Power; Martin Schmidt 002 (J. Log. Comput., 2016)

Proof Mining with Dependent Types. - Ekaterina Komendantskaya; Jónathan Heras (CICM, 2017)

Operational semantics of resolution and productivity in Horn clause logic. - Peng Fu 001; Ekaterina Komendantskaya (Formal Aspects Comput., 2017)

Productive corecursion in logic programming. - Ekaterina Komendantskaya; Yue Li 021 (Theory Pract. Log. Program., 2017)

Towards Coinductive Theory Exploration in Horn Clause Logic: Position Paper. - Ekaterina Komendantskaya; Yue Li 021 (HCVS, 2018)

Logic programming: Laxness and saturation. - Ekaterina Komendantskaya; John Power (J. Log. Algebraic Methods Program., 2018)

Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis. - Frantisek Farka; Ekaterina Komendantskaya; Kevin Hammond (Theory Pract. Log. Program., 2018)

Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses. - Henning Basold; Ekaterina Komendantskaya; Yue Li 021 (ESOP, 2019)

Proof-Carrying Plans. - Christopher Schwaab; Ekaterina Komendantskaya; Alasdair Hill; Frantisek Farka; Ronald P. A. Petrick; Joe B. Wells; Kevin Hammond (PADL, 2019)

Coinductive Uniform Proofs. - Ekaterina Komendantskaya; Yue Li 021 (CoRR, 2019)

Neural Network Verification for the Masses (of AI graduates). - Ekaterina Komendantskaya; Rob Stewart 001; Kirsty Duncan; Daniel Kienitz; Pierre Le Hen; Pascal Bacchus (CoRR, 2019)

Neural Networks, Secure by Construction - An Exploration of Refinement Types. - Wen Kokke; Ekaterina Komendantskaya; Daniel Kienitz; Robert Atkey; David Aspinall 001 (APLAS, 2020)

Accuracy, Training Time and Hardware Efficiency Trade-Offs for Quantized Neural Networks on FPGAs. - Pascal Bacchus; Robert J. Stewart 001; Ekaterina Komendantskaya (ARC, 2020)

Relative Robustness of Quantized Neural Networks Against Adversarial Attacks. - Kirsty Duncan; Ekaterina Komendantskaya; Robert J. Stewart 001; Michael A. Lones (IJCNN, 2020)

Proof-Carrying Plans: a Resource Logic for AI Planning. - Alasdair Hill; Ekaterina Komendantskaya; Ronald P. A. Petrick (PPDP, 2020)

Continuous Verification of Machine Learning: a Declarative Programming Approach. - Ekaterina Komendantskaya; Wen Kokke; Daniel Kienitz (PPDP, 2020)

The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them. - Ekaterina Komendantskaya; Dmitry Rozplokhas; Henning Basold (Theory Pract. Log. Program., 2020)

Actions you can handle: dependent types for AI plans. - Alasdair Hill; Ekaterina Komendantskaya; Matthew L. Daggitt; Ronald P. A. Petrick (TyDe@ICFP, 2021)

Property-driven Training: All You (N)Ever Wanted to Know About. - Marco Casadio; Matthew L. Daggitt; Ekaterina Komendantskaya; Wen Kokke; Daniel Kienitz; Rob Stewart 001 (CoRR, 2021)

The Effect of Manifold Entanglement and Intrinsic Dimensionality on Learning. - Daniel Kienitz; Ekaterina Komendantskaya; Michael A. Lones (AAAI, 2022)

Comparing Complexities of Decision Boundaries for Robust Training: A Universal Approach. - Daniel Kienitz; Ekaterina Komendantskaya; Michael A. Lones (ACCV (6), 2022)

Neural Network Robustness as a Verification Property: A Principled Case Study. - Marco Casadio; Ekaterina Komendantskaya; Matthew L. Daggitt; Wen Kokke; Guy Katz; Guy Amir; Idan Refaeli (CAV (1), 2022)

Neural Networks in Imandra: Matrix Representation as a Verification Choice. - Remi Desmartin; Grant O. Passmore; Ekaterina Komendantskaya (NSV/FoMLAS@CAV, 2022)

Differentiable Logics for Neural Network Training and Verification. - Natalia Slusarz; Ekaterina Komendantskaya; Matthew L. Daggitt; Robert J. Stewart 001 (NSV/FoMLAS@CAV, 2022)

CheckINN: Wide Range Neural Network Verification in Imandra. - Remi Desmartin; Grant O. Passmore; Ekaterina Komendantskaya; Matthew L. Daggitt (PPDP, 2022)

Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers. - Matthew L. Daggitt; Wen Kokke; Robert Atkey; Luca Arnaboldi 001; Ekaterina Komendantskaya (CoRR, 2022)

Why Robust Natural Language Understanding is a Challenge. - Marco Casadio; Ekaterina Komendantskaya; Verena Rieser; Matthew L. Daggitt; Daniel Kienitz; Luca Arnaboldi 001; Wen Kokke (CoRR, 2022)

CheckINN: Wide Range Neural Network Verification in Imandra (Extended). - Remi Desmartin; Grant O. Passmore; Ekaterina Komendantskaya; Matthew L. Daggitt (CoRR, 2022)

Neuro-Symbolic AI + Agent Systems: A First Reflection on Trends, Opportunities and Challenges. - Vaishak Belle; Michael Fisher 001; Alessandra Russo; Ekaterina Komendantskaya; Alistair Nottle (AAMAS Workshops, 2023)

ANTONIO: Towards a Systematic Method of Generating NLP Benchmarks for Verification. - Marco Casadio; Luca Arnaboldi 001; Matthew L. Daggitt; Omri Isac; Tanvi Dinkar; Daniel Kienitz; Verena Rieser; Ekaterina Komendantskaya (FoMLAS@CAV, 2023)

The Vehicle Tutorial: Neural Network Verification with Vehicle. - Matthew L. Daggitt; Wen Kokke; Ekaterina Komendantskaya; Robert Atkey; Luca Arnaboldi 001; Natalia Slusarz; Marco Casadio; Ben Coke; Jeonghyeon Lee (FoMLAS@CAV, 2023)

Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. - Matthew L. Daggitt; Robert Atkey; Wen Kokke; Ekaterina Komendantskaya; Luca Arnaboldi 001 (CPP, 2023)

Towards a Certified Proof Checker for Deep Neural Network Verification. - Remi Desmartin; Omri Isac; Grant O. Passmore; Kathrin Stark; Ekaterina Komendantskaya; Guy Katz (LOPSTR, 2023)

Logic of Differentiable Logics: Towards a Uniform Semantics of DL. - Natalia Slusarz; Ekaterina Komendantskaya; Matthew L. Daggitt; Robert J. Stewart 001; Kathrin Stark (LPAR, 2023)

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. - Haoze Wu 001; Omri Isac; Aleksandar Zeljic; Teruhiro Tagomori; Matthew L. Daggitt; Wen Kokke; Idan Refaeli; Guy Amir; Kyle Julian; Shahaf Bassan; Pei Huang 002; Ori Lahav 002; et al. (CAV (2), 2024)

Generating Traffic-Level Adversarial Examples from Feature-Level Specifications. - Robert Flood; Marco Casadio; David Aspinall 001; Ekaterina Komendantskaya (ESORICS Workshops (2), 2024)

Taming Differentiable Logics with Coq Formalisation. - Reynald Affeldt; Alessandro Bruni; Ekaterina Komendantskaya; Natalia Slusarz; Kathrin Stark (ITP, 2024)

Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs. - Matthew L. Daggitt; Wen Kokke; Robert Atkey; Natalia Slusarz; Luca Arnaboldi 001; Ekaterina Komendantskaya (CoRR, 2024)

NLP Verification: Towards a General Methodology for Certifying Robustness. - Marco Casadio; Tanvi Dinkar; Ekaterina Komendantskaya; Luca Arnaboldi 001; Omri Isac; Matthew L. Daggitt; Guy Katz; Verena Rieser; Oliver Lemon (CoRR, 2024)

A Certified Proof Checker for Deep Neural Network Verification. - Remi Desmartin; Omri Isac; Ekaterina Komendantskaya; Kathrin Stark; Grant O. Passmore; Guy Katz (CoRR, 2024)

A Neurosymbolic Framework for Bias Correction in CNNs. - Parth Padalkar; Natalia Slusarz; Ekaterina Komendantskaya; Gopal Gupta 001 (CoRR, 2024)

A Neurosymbolic Framework for Bias Correction in Convolutional Neural Networks. - Parth Padalkar; Natalia Slusarz; Ekaterina Komendantskaya; Gopal Gupta 001 (Theory Pract. Log. Program., 2024)

Proof-Carrying Neuro-Symbolic Code. - Ekaterina Komendantskaya (CiE, 2025)

Neural Network Verification is a Programming Language Challenge. - Lucas C. Cordeiro; Matthew L. Daggitt; Julien Girard-Satabin; Omri Isac; Taylor T. Johnson; Guy Katz; Ekaterina Komendantskaya; Augustin Lemesle; Edoardo Manino; Artjoms Sinkarovs; Haoze Wu 001 (ESOP (1), 2025)

Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk). - Matthew L. Daggitt; Wen Kokke; Robert Atkey; Ekaterina Komendantskaya; Natalia Slusarz; Luca Arnaboldi 001 (FSCD, 2025)

Formally Verifying Robustness and Generalisation of Network Intrusion Detection Models. - Robert Flood; Marco Casadio; David Aspinall 001; Ekaterina Komendantskaya (SAC, 2025)

A Generalised Framework for Property-Driven Machine Learning. - Thomas Flinkow; Marco Casadio; Colin Kessler; Rosemary Monahan; Ekaterina Komendantskaya (CoRR, 2025)

Neural Network Verification for Gliding Drone Control: A Case Study. - Colin Kessler; Ekaterina Komendantskaya; Marco Casadio; Ignazio Maria Viola; Thomas Flinkow; Albaraa Ammar Othman; Alistair Malhotra; Robbie McPherson (CoRR, 2025)