| Publication | Date of Publication | Type |
|---|
| Taming differentiable logics with Coq formalisation | 2026-02-10 | Paper |
| Proof-carrying neuro-symbolic code | 2025-11-19 | Paper |
| Logic of differentiable logics: towards a uniform semantics of DL | 2025-02-19 | Paper |
| ACL2(ml): machine-learning for ACL2 | 2024-08-19 | Paper |
Coinduction in uniform: foundations for corecursive proof search with Horn clauses
Programming Languages and Systems | 2023-11-24 | Paper |
| scientific article; zbMATH DE number 7447759 (Why is no real title available?) | 2021-12-17 | Paper |
scientific article; zbMATH DE number 7447759 (Why is no real title available?)
(available as arXiv preprint) | 2021-12-17 | Paper |
The new normal: we cannot eliminate cuts in coinductive calculi, but we can explore them
Theory and Practice of Logic Programming | 2020-12-13 | Paper |
| Structural resolution for logic programming | 2019-04-24 | Paper |
Structural resolution for logic programming
(available as arXiv preprint) | 2019-04-24 | Paper |
Logic programming: laxness and saturation
Journal of Logical and Algebraic Methods in Programming | 2018-11-01 | Paper |
Productive corecursion in logic programming
Theory and Practice of Logic Programming | 2017-11-08 | Paper |
A productivity checker for logic programming
(available as arXiv preprint) | 2017-10-13 | Paper |
Coinductive soundness of corecursive type class resolution
(available as arXiv preprint) | 2017-10-13 | Paper |
Proof mining with dependent types
(available as arXiv preprint) | 2017-07-21 | Paper |
Operational semantics of resolution and productivity in Horn clause logic
Formal Aspects of Computing | 2017-06-01 | Paper |
Category theoretic semantics for theorem proving in logic programming: embracing the laxness
Coalgebraic Methods in Computer Science | 2016-07-15 | Paper |
Coalgebraic logic programming: from Semantics to Implementation
Journal Of Logic And Computation | 2016-07-07 | Paper |
Exploiting parallelism in coalgebraic logic programming
(available as arXiv preprint) | 2016-05-06 | Paper |
Proof relevant corecursive resolution
Functional and Logic Programming | 2016-04-04 | Paper |
Proof relevant corecursive resolution
Functional and Logic Programming | 2016-04-04 | Paper |
A type-theoretic approach to resolution
Logic-Based Program Synthesis and Transformation | 2016-02-05 | Paper |
| scientific article; zbMATH DE number 6528605 (Why is no real title available?) | 2016-01-11 | Paper |
Sound and complete SLD-resolution for bilattice-based annotated logic programs
Electronic Notes in Theoretical Computer Science | 2015-03-23 | Paper |
Recycling proof patterns in Coq: case studies
Mathematics in Computer Science | 2014-11-26 | Paper |
Inductive and coinductive components of corecursive functions in Coq
Electronic Notes in Theoretical Computer Science | 2014-01-24 | Paper |
Proof-pattern recognition and lemma discovery in ACL2
Logic for Programming, Artificial Intelligence, and Reasoning | 2014-01-17 | Paper |
ML4PG in computer algebra verification
Lecture Notes in Computer Science | 2013-08-09 | Paper |
| Coalgebraic derivations in logic programming | 2012-09-18 | Paper |
Unification neural networks: unification by error-correction learning
Logic Journal of the IGPL | 2012-06-08 | Paper |
Coalgebraic semantics for derivations in logic programming
Algebra and Coalgebra in Computer Science | 2011-09-02 | Paper |
Coalgebraic semantics for parallel derivation strategies in logic programming
Algebraic Methodology and Software Technology | 2011-01-21 | Paper |
Using Structural Recursion for Corecursion
Lecture Notes in Computer Science | 2009-07-02 | Paper |
Fibrational Semantics for Many-Valued Logic Programs: Grounds for Non-Groundness
Logics in Artificial Intelligence | 2008-10-27 | Paper |
A Sequent Calculus for Bilattice-Based Logic and Its Many-Sorted Representation
Lecture Notes in Computer Science | 2008-01-04 | Paper |
