Ekaterina Komendantskaya

Guy Katz

Clark W. Barrett

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023

Logic of Differentiable Logics: Towards a Uniform Semantics of DL.

[BibT_eX]

[DOI]

Natalia Slusarz

Kathrin Stark

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Towards a Certified Proof Checker for Deep Neural Network Verification.

[BibT_eX]

[DOI]

Guy Katz

Proceedings of the Logic-Based Program Synthesis and Transformation, 2023

Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively.

[BibT_eX]

[DOI]

Robert Atkey

Luca Arnaboldi

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

The Vehicle Tutorial: Neural Network Verification with Vehicle.

[BibT_eX]

[DOI]

Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems, 2023

ANTONIO: Towards a Systematic Method of Generating NLP Benchmarks for Verification.

[BibT_eX]

[DOI]

Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems, 2023

Neuro-Symbolic AI + Agent Systems: A First Reflection on Trends, Opportunities and Challenges.

[BibT_eX]

[DOI]

Vaishak Belle

Michael Fisher

Alessandra Russo

Alistair Nottle

Proceedings of the Autonomous Agents and Multiagent Systems. Best and Visionary Papers - AAMAS 2023 Workshops, London, UK, May 29, 2023

2022

CheckINN: Wide Range Neural Network Verification in Imandra (Extended).

[BibT_eX]

[DOI]

Remi Desmartin

Grant O. Passmore

CoRR, 2022

Why Robust Natural Language Understanding is a Challenge.

[BibT_eX]

[DOI]

Marco Casadio

CoRR, 2022

Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers.

[BibT_eX]

[DOI]

CoRR, 2022

CheckINN: Wide Range Neural Network Verification in Imandra.

[BibT_eX]

[DOI]

Remi Desmartin

Grant O. Passmore

Proceedings of the PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming, Tbilisi, Georgia, September 20, 2022

Differentiable Logics for Neural Network Training and Verification.

[BibT_eX]

[DOI]

Natalia Slusarz

Proceedings of the Software Verification and Formal Methods for ML-Enabled Autonomous Systems, 2022

Neural Networks in Imandra: Matrix Representation as a Verification Choice.

[BibT_eX]

[DOI]

Remi Desmartin

Grant O. Passmore

Proceedings of the Software Verification and Formal Methods for ML-Enabled Autonomous Systems, 2022

Neural Network Robustness as a Verification Property: A Principled Case Study.

[BibT_eX]

[DOI]

Marco Casadio

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Comparing Complexities of Decision Boundaries for Robust Training: A Universal Approach.

[BibT_eX]

[DOI]

Michael A. Lones

Proceedings of the Computer Vision - ACCV 2022, 2022

The Effect of Manifold Entanglement and Intrinsic Dimensionality on Learning.

[BibT_eX]

[DOI]

Michael A. Lones

Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence, 2022

2021

Property-driven Training: All You (N)Ever Wanted to Know About.

[BibT_eX]

[DOI]

Marco Casadio

Rob Stewart

CoRR, 2021

Actions you can handle: dependent types for AI plans.

[BibT_eX]

[DOI]

Alasdair Hill

Ronald P. A. Petrick

Proceedings of the TyDe 2021: Proceedings of the 6th ACM SIGPLAN International Workshop on Type-Driven Development, 2021

2020

The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them.

[BibT_eX]

[DOI]

Dmitry Rozplokhas

Henning Basold

Theory Pract. Log. Program., 2020

Continuous Verification of Machine Learning: a Declarative Programming Approach.

[BibT_eX]

[DOI]

Proceedings of the PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming, 2020

Proof-Carrying Plans: a Resource Logic for AI Planning.

[BibT_eX]

[DOI]

Alasdair Hill

Ronald P. A. Petrick

Proceedings of the PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming, 2020

Relative Robustness of Quantized Neural Networks Against Adversarial Attacks.

[BibT_eX]

[DOI]

Kirsty Duncan

Michael A. Lones

Proceedings of the 2020 International Joint Conference on Neural Networks, 2020

Accuracy, Training Time and Hardware Efficiency Trade-Offs for Quantized Neural Networks on FPGAs.

[BibT_eX]

[DOI]

Pascal Bacchus

Proceedings of the Applied Reconfigurable Computing. Architectures, Tools, and Applications, 2020

Neural Networks, Secure by Construction - An Exploration of Refinement Types.

[BibT_eX]

[DOI]

Robert Atkey

David Aspinall

Proceedings of the Programming Languages and Systems - 18th Asian Symposium, 2020

2019

Neural Network Verification for the Masses (of AI graduates).

[BibT_eX]

[DOI]

CoRR, 2019

Coinductive Uniform Proofs.

[BibT_eX]

[DOI]

CoRR, 2019

Proof-Carrying Plans.

[BibT_eX]

[DOI]

Christopher Schwaab

Proceedings of the Practical Aspects of Declarative Languages, 2019

Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses.

[BibT_eX]

[DOI]

Henning Basold

Proceedings of the Programming Languages and Systems, 2019

2018

Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis.

[BibT_eX]

[DOI]

Kevin Hammond

Theory Pract. Log. Program., 2018

Logic programming: Laxness and saturation.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2018

Towards Coinductive Theory Exploration in Horn Clause Logic: Position Paper.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis, 2018

2017

Productive corecursion in logic programming.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2017

Operational semantics of resolution and productivity in Horn clause logic.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2017

Proof Mining with Dependent Types.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

2016

Coalgebraic logic programming: from Semantics to Implementation.

[BibT_eX]

[DOI]

J. Log. Comput., 2016

Structural Resolution for Abstract Compilation of Object-Oriented Languages.

[BibT_eX]

[DOI]

Luca Franceschini

Davide Ancona

Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types, 2016

CoALP-Ty'16.

[BibT_eX]

[DOI]

CoRR, 2016

Coinductive Soundness of Corecursive Type Class Resolution.

[BibT_eX]

[DOI]

Kevin Hammond

CoRR, 2016

Operational Semantics of Resolution in Horn Clause Logic.

[BibT_eX]

[DOI]

CoRR, 2016

A Productivity Checker for Logic Programming.

[BibT_eX]

[DOI]

Patricia Johann

Proceedings of the Logic-Based Program Synthesis and Transformation, 2016

Coinductive Soundness of Corecursive Type Class Resolution.

[BibT_eX]

[DOI]

Kevin Hammond

Proceedings of the Logic-Based Program Synthesis and Transformation, 2016

Proof Relevant Corecursive Resolution.

[BibT_eX]

[DOI]

Tom Schrijvers

Andrew Pond

Proceedings of the Functional and Logic Programming - 13th International Symposium, 2016

Category Theoretic Semantics for Theorem Proving in Logic Programming: Embracing the Laxness.

[BibT_eX]

[DOI]

Proceedings of the Coalgebraic Methods in Computer Science, 2016

2015

Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic.

[BibT_eX]

[DOI]

Patricia Johann

CoRR, 2015

A Type-Theoretic Approach to Structural Resolution.

[BibT_eX]

[DOI]

CoRR, 2015

A Type-Theoretic Approach to Resolution.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2015

Structural Resolution for Logic Programming.

[BibT_eX]

[DOI]

Patricia Johann

Vladimir Komendantskiy

Proceedings of the Technical Communications of the 31st International Conference on Logic Programming (ICLP 2015), Cork, Ireland, August 31, 2015

2014

Recycling Proof Patterns in Coq: Case Studies.

[BibT_eX]

[DOI]

Math. Comput. Sci., 2014

Guarding (Co)Recursion in Coalgebraic Logic Programming.

[BibT_eX]

[DOI]

CoRR, 2014

ACL2(ml): Machine-Learning for ACL2.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

HoTT formalisation in Coq: Dependency Graphs \& ML4PG.

[BibT_eX]

[DOI]

CoRR, 2014

Proof Pattern Search in Coq/SSReflect.

[BibT_eX]

[DOI]

CoRR, 2014

2013

Exploiting Parallelism in Coalgebraic Logic Programming.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Algebra, Coalgebra and Topology, 2013

Statistical Proof Pattern Recognition: Automated or Interactive?

[BibT_eX]

[DOI]

CoRR, 2013

ML4PG: proof-mining in Coq

[BibT_eX]

[DOI]

CoRR, 2013

Statistical Proof-Patterns in Coq/SSReflect

[BibT_eX]

[DOI]

CoRR, 2013

Proof-Pattern Recognition in ACL2.

[BibT_eX]

[DOI]

Moa Johansson

Ewen Maclean

CoRR, 2013

ML4PG in Computer Algebra Verification.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 2013

Proof-Pattern Recognition and Lemma Discovery in ACL2.

[BibT_eX]

[DOI]

Moa Johansson

Ewen Maclean

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

2012

Machine Learning in Proof General: Interfacing Interfaces

[BibT_eX]

[DOI]

Gudmund Grov

Proceedings of the Proceedings 10th International Workshop On User Interfaces for Theorem Provers, 2012

Neural Networks for Proof-Pattern Recognition.

[BibT_eX]

[DOI]

Kacper Lichota

Proceedings of the Artificial Neural Networks and Machine Learning - ICANN 2012, 2012

2011

Unification neural networks: unification by error-correction learning.

[BibT_eX]

[DOI]

Log. J. IGPL, 2011

SHERLOCK - An Interface for Neuro-Symbolic Networks.

[BibT_eX]

[DOI]

Qiming Zhang

Proceedings of the Seventh International Workshop on Neural-Symbolic Learning and Reasoning, 2011

Machine Learning Coalgebraic Proofs.

[BibT_eX]

[DOI]

Proceedings of the Latest Advances in Inductive Logic Programming, 2011

Coalgebraic Derivations in Logic Programming.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 2011

Coalgebraic Semantics for Derivations in Logic Programming.

[BibT_eX]

[DOI]

Proceedings of the Algebra and Coalgebra in Computer Science, 2011

2010

Neuro-symbolic Representation of Logic Programs Defining Infinite Sets.

[BibT_eX]

[DOI]

Krysia Broda

Artur S. d'Avila Garcez

Proceedings of the Artificial Neural Networks - ICANN 2010, 2010

Coalgebraic Semantics for Parallel Derivation Strategies in Logic Programming.

[BibT_eX]

[DOI]

Guy McCusker

Proceedings of the Algebraic Methodology and Software Technology, 2010

2009

Neurons or Symbols - Why does OR Remain Exclusive?.

[BibT_eX]

Proceedings of the IJCCI 2009, 2009

Parallel Rewriting in Neural Networks.

[BibT_eX]

Proceedings of the IJCCI 2009, 2009

2008

Inductive and Coinductive Components of Corecursive Functions in Coq.

[BibT_eX]

[DOI]

Yves Bertot

Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, 2008

Using Structural Recursion for Corecursion.

[BibT_eX]

[DOI]

Yves Bertot

Proceedings of the Types for Proofs and Programs, International Conference, 2008

Unification by Error-Correction.

[BibT_eX]

[DOI]

Proceedings of the Fourth International Workshop on Neural-Symbolic Learning and Reasoning, 2008

Fibrational Semantics for Many-Valued Logic Programs: Grounds for Non-Groundness.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence, 11th European Conference, 2008

2007

Connectionist Representation of Multi-Valued Logic Programs.

[BibT_eX]

[DOI]

Máire Lane

Anthony Karel Seda

Proceedings of the Perspectives of Neural-Symbolic Integration, 2007

A Sequent Calculus for Bilattice-Based Logic and Its Many-Sorted Representation.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2007

First-order deduction in neural networks.

[BibT_eX]

Proceedings of the LATA 2007. Proceedings of the 1st International Conference on Language and Automata Theory and Applications., 2007

2006

Sound and Complete SLD-Resolution for Bilattice-Based Annotated Logic Programs.

[BibT_eX]

[DOI]