13 citations · 50 across the 19 of their papers we have counts for
19 papers
Schematic Unification
David M. Cerna
We present a generalization of first-order unification to a term algebra where variable indexing is part of the object language. We exploit variable indexing by associating some se…
Anti-unification and Generalization: A Survey
David M. Cerna, Temur Kutsia
Anti-unification (AU) is a fundamental operation for generalization computation used for inductive inference. It is the dual operation to unification, an operation at the foundatio…
Generalisation Through Negation and Predicate Invention
David M. Cerna, Andrew Cropper
The ability to generalise from a small number of examples is a fundamental challenge in machine learning. To tackle this challenge, we introduce an inductive logic programming (ILP…
Differentiable Inductive Logic Programming in High-Dimensional Space
Stanisław J. Purgał, David M. Cerna, Cezary Kaliszyk
Synthesizing large logic programs through symbolic Inductive Logic Programming (ILP) typically requires intermediate definitions. However, cluttering the hypothesis space with inte…
One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus
David M. Cerna, Michal Buran
Generalization techniques have many applications, including template construction, argument generalization, and indexing. Modern interactive provers can exploit advancement in gene…
A Special Case of Schematic Syntactic Unification
David M. Cerna
We present a unification problem based on first-order syntactic unification which ask whether every problem in a schematically-defined sequence of unification problems is unifiable…
Learning Higher-Order Programs without Meta-Interpretive Learning
Stanisław J. Purgał, David M. Cerna, Cezary Kaliszyk
Learning complex programs through inductive logic programming (ILP) remains a formidable challenge. Existing higher-order enabled ILP systems show improved accuracy and learning pe…
A Mobile Application for Self-Guided Study of Formal Reasoning
David M. Cerna, Rafael P. D. Kiesel, Alexandra Dzhiganskaya
In this work, we introduce AXolotl, a self-study aid designed to guide students through the basics of formal reasoning and term manipulation. Unlike most of the existing study aids…
Schematic Refutations of Formula Schemata
David Cerna, Alexander Leitsch, Anela Lolic
Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define…
Higher-Order Equational Pattern Anti-Unification [Preprint]
David M. Cerna, Temur Kutsia
We consider anti-unification for simply typed lambda terms in associative, commutative, and associative-commutative theories and develop a sound and complete algorithm which takes…
Proof Schemata for Theories equivalent to : on the Benefit of Conservative Reflection Principles
David M. Cerna, Anela Lolic
Induction is typically formalized as a rule or axiom extension of the LK-calculus. While this extension of the sequent calculus is simple and elegant, proof transformation and anal…
Integrating a Global Induction Mechanism into a Sequent Calculus
David M. Cerna, Michael Peter Lettmann
Most interesting proofs in mathematics contain an inductive argument which requires an extension of the LK-calculus to formalize. The most commonly used calculi for induction conta…
Clausal Analysis of First-order Proof Schemata
David M. Cerna, Michael Lettmann
Proof schemata are a variant of LK-proofs able to simulate various induction schemes in first-order logic by adding so called proof links to the standard first-order LK-calculus. P…
Arithmetic, Infinite Trees, and Second-order Subsystems: Notes and Observations
David M. Cerna
Work in progress concerning alternative formalizations of arithmetic.
Taking a Detour to Zero: An Alternative Formalization of Functions Beyond PR
David M. Cerna
There are two well known systems formalizing total recursion beyond primitive recursion (\textbf{PR}), system \textbf{T} by Gödel and system \textbf{F} by Girard and Reynolds. syst…
A Generalized Resolution Proof Schema and the Pigeonhole Principle
David M. Cerna
The schematic CERES method is a method of cut elimination for proof schemata, that is a sequence of proofs with a recursive construction. Proof schemata can be thought of as a way…
Total Recursion over Lexicographical Orderings: Elementary Recursive Operators Beyond PR
David Cerna
In this work we generalize primitive recursion in order to construct a hierarchy of terminating total recursive operators which we refer to as {\em leveled primitive recursion of o…
Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]
David Cerna, Alexander Leitsch
In previous work, an attempt was made to apply the schematic CERES method [8] to a formal proof with an arbitrary number of Π 2 cuts (a recursive proof encapsulating the infinitary…
Analysis of Clause set Schema Aided by Automated Theorem Proving: A Case Study [Extended Paper]
David Cerna, Alexander Leitsch
The schematic CERES method [8] is a recently developed method of cut elimination for proof schemata, that is a sequence of proofs with a recursive construction. Proof schemata can…