ABSTRACT. Lambda-superposition is a proof calculus for higher-order logic (simple type theory) developed in collaboration with Alexander Bentkamp, Simon Cruanes, Visa Nummelin, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. To a large extent, the calculus is a graceful generalization of standard superposition, which is a highly successful calculi for first-order logic. On the theory side, we proved the lambda-superposition refutationally complete. On the practical side, we implemented it in the Zipperposition prover and, together with Stephan Schulz, in the E prover. Zipperposition finished first in the higher-order theorem division of the CADE ATP System Competition in 2020, 2021, and 2022, suggesting that superposition is a valuable approach also in a higher-order setting.

ABSTRACT. This paper describes the formal verification of NP-hardness of two key problems relevant in algebraic lattice theory: the closest vector problem and the shortest vector problem, both in the infinity norm. The formalization uncovered a number of problems with the existing proofs in the literature. The paper describes how these problems were corrected in the formalization. The work was carried out in the proof assistant Isabelle.

ABSTRACT. Resolution and superpostion provers rely on the given clause procedure to saturate the clause set. Using Isabelle/HOL, we formally verify four variants of the procedure: the well-known Otter and DISCOUNT loops as well as the lesser-known iProver and Zipperposition loops. For each of the variants, we show that given a fair data structure to store the formulas that wait to be selected, the procedure guarantees saturation. Our formalization of the Zipperposition loop clarifies some fine points previously misunderstood in the literature.

ABSTRACT. We present an Isabelle/HOL formalization of Simple Clause Learning for first-order logic without equality: SCL(FOL). The main results are formal proofs of soundness, non-redundancy of learned clauses, termination, and refutational completeness. Compared to the unformalized version, the formalized calculus is simpler, a number of results could be generalized, and the non-redundancy strengthened. We found one bug in a previously published version of the SCL Backtrack rule. Compared to related formalizatons, we introduce a new technique for showing termination based on non-redundant clause learning.

ABSTRACT. Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a rich type system but has rather substantial conceptual differences to HOL, including a much more difficult treatment of equality.

We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL while adding the expressivity of dependent types, specifically dependent function types and predicate subtypes. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to the Leo theorem prover for HOL, thereby obtaining a theorem prover for DHOL.

ABSTRACT. Several new algorithms for deciding emptiness of boolean combinations of regular languages and of languages of alternating automata (AFA) have been proposed recently, especially in the context of analysing regular expressions and in string constraint solving. The new algorithms demonstrated a significant potential, but they have never been systematically compared, neither among each other nor with the state-of-the art implementations of existing (non)deterministic automata-based methods. In this paper, we provide the first such comparison as well as an overview of the existing algorithms and their implementations. We collect a diverse benchmark mostly originating in or related to practical problems from string constraint solving, analysing LTL properties, and regular model checking, and evaluate collected implementations on it. The results reveal the best tools and hint on what the best algorithms and implementation techniques are. Roughly, although some advanced algorithms are fast, such as antichain algorithms and reductions to IC3/PDR, they are not as overwhelmingly dominant as sometimes presented and there is no clear winner. Even simple NFA/DFA-based technology may be the best choice, depending on the problem source and implementation style. We believe that our findings are highly relevant for further development of these techniques as well as for related fields such as string constraint solving.

ABSTRACT. We present a theory of Cartesian arrays, which are multi-dimensional arrays with support for the projection of n-dimensional arrays to (n-1)-dimensional sub-arrays, as well as for updating sub-arrays. The resulting logic is an extension of Combinatorial Array Logic (CAL) and is motivated by the analysis of quantum circuits: using projection, we can succinctly encode the semantics of quantum gates as quantifier-free formulas and verify the end-to-end correctness of quantum circuits. Since the logic is expressive enough to represent quantum circuits succinctly, it necessarily has a high complexity; as we show, it suffices to encode the k-color problem of a graph under a succinct circuit representation, a NEXPTIME-complete problem. We present an NEXPTIME decision procedure for the logic and report on preliminary experiments with the analysis of quantum circuits using this decision procedure.

ABSTRACT. We present a simple calculus for deriving statements about the local behaviour of partial, continuous functions over the reals, within a collection of such functions associated with the elements of a finite partial order. We show that the calculus is sound in general and complete for particular partial orders and statements. The motivation for this work is drawn from an attempt to foster digitalisation in secondary-eduction classrooms, in particular in experimental lessons in natural science classes. This provides a way to formally model experiments and to automatically derive the truth of hypotheses made about certain phenomena in such experiments.

ABSTRACT. We describe an experimental implementation of a logic-based end-to-end pipeline of giving explained answers to questions posed in natural language. The main components of the pipeline are semantic parsing, integration with large knowledge bases, automated reasoning using extended first order logic, and finally the translation of proofs back to natural language. While able to answer relatively simple questions on its own, the implementation is targeting research into building hybrid neurosymbolic systems for gaining trustworthiness and explainability. The end goal is to combine machine learning and large language models with the components of the implementation and to use the automated reasoner as an interface between natural language and external tools like database systems and scientific calculations.

ABSTRACT. We recently proposed Acceleration Driven Clause Learning (ADCL), a novel calculus to analyze satisfiability of Constrained Horn Clauses (CHCs). Here, we adapt ADCL to transition systems and introduce ADCL-NT, a variant for disproving termination. We implemented ADCL-NT in our tool LoAT and evaluate it against the state of the art.

ABSTRACT. Dependency pairs are one of the most powerful techniques to analyze termination of term rewrite systems (TRSs) automatically. We adapt the dependency pair framework to the probabilistic setting in order to prove almost-sure innermost termination of probabilistic TRSs. To evaluate its power, we implemented the new framework in our tool AProVE.

ABSTRACT. There are many techniques and tools to prove termination of C programs, but up to now these tools were not very powerful for fully automated termination proofs of programs whose termination depends on recursive data structures like lists. We present the first approach that extends powerful techniques for termination analysis of C programs (with memory allocation and explicit pointer arithmetic) to lists.

ABSTRACT. We revisit AC completion for left-linear term rewrite systems where AC unification is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows to switch from the former to the latter at any point during a completion process. Finally, we present experimental results for our implementation of left-linear AC completion in the tool accompll.