arXiv subjects

David M. Cerna

Publications and source records attributed to David M. Cerna.

At least 19 recordsLinked to original sources

arXiv2025

Symmetry breaking for inductive logic programming

The goal of inductive logic programming is to search for a hypothesis that generalises training data and background knowledge. The challenge is searching vast hypothesis spaces, which is exacerbated because many logically equivalent hypotheses exist. To address this challenge, we introduce a method to break symmetries in the hypothesis space. We implement our idea in answer set programming. Our experiments on multiple domains, including visual reasoning and game playing, show that our approach can reduce solving times from over an hour to just 17 seconds.

cs.AI↗

arXiv2025

Honey, I shrunk the hypothesis space (through logical preprocessing)

Inductive logic programming (ILP) is a form of logical machine learning. The goal is to search a hypothesis space for a hypothesis that generalises training examples and background knowledge. We introduce an approach that 'shrinks' the hypothesis space before an ILP system searches it. Our approach uses background knowledge to find rules that cannot be in an optimal hypothesis regardless of the training examples. For instance, our approach discovers relationships such as "even numbers cannot be odd" and "prime numbers greater than 2 are odd". It then removes violating rules from the hypothesis space. We implement our approach using answer set programming and use it to shrink the hypothesis space of a constraint-based ILP system. Our experiments on multiple domains, including visual reasoning and game playing, show that our approach can substantially reduce learning times whilst maintaining predictive accuracies. For instance, given just 10 seconds of preprocessing time, our approach can reduce learning times from over 10 hours to only 2 seconds.

cs.AI↗

arXiv2025

Efficient rule induction by ignoring pointless rules

The goal of inductive logic programming (ILP) is to find a set of logical rules that generalises training examples and background knowledge. We introduce an ILP approach that identifies pointless rules. A rule is pointless if it contains a redundant literal or cannot discriminate against negative examples. We show that ignoring pointless rules allows an ILP system to soundly prune the hypothesis space. Our experiments on multiple domains, including visual reasoning and game playing, show that our approach can reduce learning times by 99% whilst maintaining predictive accuracies.

cs.AI↗

arXiv2024

A Note On Square-free Sequences and Anti-unification Type

Error: Peer-review process exposed an error in Theorem 1 that, unfourtunately, is not repairable. Idempotent semigroups are always finite. See Green and Rees [1952], Siekmann and Szab\'o [1981] for details Anti-unification is a fundamental operation used for inductive inference. It is abstractly defined as a process deriving from a set of symbolic expressions a new symbolic expression possessing certain commonalities shared between its members. We consider anti-unification over term algebras where some function symbols are interpreted as associative-idempotent $(f (x, f (y, z)) = f (f (x, y), z)$ and $f (x, x) = x$, respectively) and show that there exists generalization problems for which a minimal complete set of solutions does not exist (Nullary), that is every complete set must contain comparable elements with respect to the generality relation. In contrast to earlier techniques for showing the nullarity of a generalization problem, we exploit combinatorial properties of complete sets of solutions to show that comparable elements are not avoidable. We show that every complete set of solutions contains an infinite chain of comparable generalizations whose structure is isomorphic to a subsequence of an infinite square-free sequence over three symbols.

cs.LO↗

arXiv2024

Learning Rules Explaining Interactive Theorem Proving Tactic Prediction

Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theorem provers (ITP). Deriving the most appropriate subsequent proof step, and reasoning about it, given the multitude of possibilities, remains a daunting task for novice users. To improve the situation, several investigations have developed machine learning based guidance for tactic selection. Such approaches struggle to learn non-trivial relationships between the chosen tactic and the structure of the proof state and represent them as symbolic expressions. To address these issues we (i) We represent the problem as an Inductive Logic Programming (ILP) task, (ii) Using the ILP representation we enriched the feature space by encoding additional, computationally expensive properties as background knowledge predicates, (iii) We use this enriched feature space to learn rules explaining when a tactic is applicable to a given proof state, (iv) we use the learned rules to filter the output of an existing tactic selection approach and empirically show improvement over the non-filtering approaches.

cs.LO↗

arXiv2024

Scalable Knowledge Refactoring using Constrained Optimisation

Knowledge refactoring compresses a logic program by introducing new rules. Current approaches struggle to scale to large programs. To overcome this limitation, we introduce a constrained optimisation refactoring approach. Our first key idea is to encode the problem with decision variables based on literals rather than rules. Our second key idea is to focus on linear invented rules. Our empirical results on multiple domains show that our approach can refactor programs quicker and with more compression than the previous state-of-the-art approach, sometimes by 60%.

cs.LO↗

arXiv2024

One is all you need: Second-order Unification without First-order Variables

We introduce a fragment of second-order unification, referred to as \emph{Second-Order Ground Unification (SOGU)}, with the following properties: (i) only one second-order variable is allowed, and (ii) first-order variables do not occur. We study an equational variant of SOGU where the signature contains \textit{associative} binary function symbols (ASOGU) and show that Hilbert's 10$^{th}$ problem is reducible to ASOGU unifiability, thus proving undecidability. Our reduction provides a new lower bound for the undecidability of second-order unification, as previous results required first-order variable occurrences, multiple second-order variables, and/or equational theories involving \textit{length-reducing} rewrite systems. Furthermore, our reduction holds even in the case when associativity of the binary function symbol is restricted to \emph{power associative}, i.e. f(f(x,x),x)= f(x,f(x,x)), as our construction requires a single constant.

cs.LO↗

arXiv2023

Equational Anti-Unification over Absorption Theories

Interest in anti-unification, the dual problem of unification, is on the rise due to applications within the field of software analysis and related areas. For example, anti-unification-based techniques have found uses within clone detection and automatic program repair methods. While syntactic forms of anti-unification are enough for many applications, some aspects of software analysis methods are more appropriately modeled by reasoning modulo an equational theory. Thus, extending existing anti-unification methods to deal with important equational theories is the natural step forward. This paper considers anti-unification modulo pure absorption theories, i.e., some operators are associated with a special constant satisfying the axiom $f(x,\varepsilon_f) \approx f(\varepsilon_f,x) \approx \varepsilon_f$. We provide a sound and complete rule-based algorithm for such theories. Furthermore, we show that anti-unification modulo absorption is infinitary. Despite this, our algorithm terminates and produces a finitary algorithmic representation of the minimal complete set of solutions. We also show that the linear variant is finitary.

cs.LO↗

arXiv2023

Schematic Unification

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 sequences of variables ($X_0,\ X_1,\ X_2,\dots$) with a mapping $\sigma$ whose domain is the variable sequence and whose range consist of terms that may contain variables from the sequence. From a given term $t$, an infinite sequence of terms may be produced by iterative application of $\sigma$. Given a unification problem $U$ and mapping $\sigma$, the \textit{schematic unification problem} asks whether all unification problems $U$, $\sigma(U)$, $\sigma(\sigma(U))$, $\dots$ are unifiable. We provide a terminating and sound algorithm. Our algorithm is \textit{complete} if we further restrict ourselves to so-called $\infty$-stable problems. We conjecture that this additional requirement is unnecessary for completeness. Schematic unification is related to methods of inductive proof transformation by resolution and inductive reasoning.

cs.LO↗

arXiv2023

Anti-unification and Generalization: A Survey

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 foundation of automated theorem proving. Interest in AU from the AI and related communities is growing, but without a systematic study of the concept nor surveys of existing work, investigations often resort to developing application-specific methods that existing approaches may cover. We provide the first survey of AU research and its applications and a general framework for categorizing existing and future developments.

cs.LO↗

arXiv2023

Generalisation Through Negation and Predicate Invention

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) approach that combines negation and predicate invention. Combining these two features allows an ILP system to generalise better by learning rules with universally quantified body-only variables. We implement our idea in NOPI, which can learn normal logic programs with predicate invention, including Datalog programs with stratified negation. Our experimental results on multiple domains show that our approach can improve predictive accuracies and learning times.

cs.AI↗

arXiv2022

Differentiable Inductive Logic Programming in High-Dimensional Space

Synthesizing large logic programs through symbolic Inductive Logic Programming (ILP) typically requires intermediate definitions. However, cluttering the hypothesis space with intensional predicates typically degrades performance. In contrast, gradient descent provides an efficient way to find solutions within such high-dimensional spaces. Neuro-symbolic ILP approaches have not fully exploited this so far. We propose extending the {\delta}ILP approach to inductive synthesis with large-scale predicate invention, thus allowing us to exploit the efficacy of high-dimensional gradient descent. We show that large-scale predicate invention benefits differentiable inductive synthesis through gradient descent and allows one to learn solutions for tasks beyond the capabilities of existing neuro-symbolic ILP systems. Furthermore, we achieve these results without specifying the precise structure of the solution within the language bias.

cs.AI↗

arXiv2022

One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus

Generalization techniques have many applications, including template construction, argument generalization, and indexing. Modern interactive provers can exploit advancement in generalization methods over expressive type theories to further develop proof generalization techniques and other transformations. So far, investigations concerned with anti-unification (AU) over $\lambda$-terms and similar type theories have focused on developing algorithms for well-studied variants. These variants forbid the nesting of generalization variables, restrict the structure of their arguments, and are \textit{unitary}. Extending these methods to more expressive variants is important to applications. We consider the case of nested generalization variables and show that the AU problem is \textit{nullary} (using \textit{capture-avoiding} substitutions), even when the arguments to free variables are severely restricted.

cs.LO↗

arXiv2022

Learning Higher-Order Programs without Meta-Interpretive Learning

Learning complex programs through inductive logic programming (ILP) remains a formidable challenge. Existing higher-order enabled ILP systems show improved accuracy and learning performance, though remain hampered by the limitations of the underlying learning mechanism. Experimental results show that our extension of the versatile Learning From Failures paradigm by higher-order definitions significantly improves learning performance without the burdensome human guidance required by existing systems. Our theoretical framework captures a class of higher-order definitions preserving soundness of existing subsumption-based pruning methods.

cs.AI↗

arXiv2022

A Special Case of Schematic Syntactic Unification

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, so called loop unification. Alternatively, our problem may be formulated as a recursive procedure calling first-order syntactic unification on certain bindings occurring in the solved form resulting from unification. Loop unification is closely related to Narrowing as the schematic constructions can be seen as a rewrite rule applied during unification, and primal grammars, as we deal with recursive term constructions. However, loop unification relaxes the restrictions put on variables as fresh as well as used extra variables may be introduced by rewriting. In this work we consider an important special case, so called semiloop unification. We provide a sufficient condition for unifiability of the entire sequence based on the structure of a sufficiently long initial segment. It remains an open question whether this condition is also necessary for semiloop unification and how it may be extended to loop unification.

cs.LO↗

arXiv2020

A Mobile Application for Self-Guided Study of Formal Reasoning

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 for formal reasoning, AXolotl is an Android-based application with a simple touch-based interface. Part of the design goal was to minimize the possibility of user errors which distract from the learning process. Such as typos or inconsistent application of the provided rules. The system includes a zoomable proof viewer which displays the progress made so far and allows for storage of the completed proofs as a JPEG or LaTeX file. The software is available on the google play store and comes with a small library of problems. Additional problems may be opened in AXolotl using a simple input language. Currently, AXolotl supports problems that can be solved using rules which transform a single expression into a set of expressions. This covers educational scenarios found in our first-semester introduction to logic course and helps bridge the gap between propositional and first-order reasoning. Future developments will include rewrite rules which take a set of expressions and return a set of expressions, as well as a quantified first-order extension.

cs.LO↗

arXiv2018

Proof Schemata for Theories equivalent to $PA$: on the Benefit of Conservative Reflection Principles

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 analysis can be quite difficult. Theories with an induction rule, for example Peano arithmetic do not have a {\em Herbrand} theorem. In this work we extend an existing meta-theoretic formalism, so called proof schemata, a recursive formulation of induction particularly suited for proof analysis, to Peano arithmetic. This relationship provides a meaningful conservative reflection principle between \PA and an alternative proof formalism. Proof schemata have been shown to have a variant of Herbrand's theorem for classical logic which can be lifted to the subsystem of our new formalism equivalent to primitive recursive arithmetic.

math.LO↗

arXiv2018

Higher-Order Equational Pattern Anti-Unification [Preprint]

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 two lambda terms and computes their generalizations in the form of higher-order patterns. The problem is finitary: the minimal complete set of generalizations contains finitely many elements. We define the notion of optimal solution and investigate special fragments of the problem for which the optimal solution can be computed in linear or polynomial time.

cs.LO↗