ABSTRACT. Modal logics extend classical first-order logic with the modalities of necessity (□) and possibility (♢). A model of a set of modal logic formulae can be represented by a Kripke structure. This paper describes a method and implementation for finding finite Kripke models for formulae in first-order modal logics. The approach relies on translating the modal logic formulae to classical logic formulae, using an SMT solver to generate a finite model of the classical logic formulae, then translating the classical model to a finite Kripke model. This process has been implemented in the new model finding system MoMo, which produces TPTP-compliant Kripke model representations. An evaluation on the modal logic problems in the TPTP problem library confirms the practicality of this approach. Up to the authors' knowledge, MoMo is the first model finder for first-order modal logics.

ABSTRACT. Program synthesis is the task of automatically deriving a program that has been specified by a user in advance. Combining automated theorem proving with program synthesis enables the automated construction of proven-to-be-correct programs, thereby ensuring software reliability. In this paper, we consider the superposition-based calculus extended to support synthesis of recursion-free programs allowing reasoning with uncomputable symbols. We present cases where the calculus fails and refine it to solve them. We prove that the refined calculus is sound. Finally, we also prove completeness in the following sense: if at least one computable program satisfying the given specification exists, we show that the modified calculus finds one.

ABSTRACT. Certificates are machine-checkable witnesses that help increase confidence in verification results by providing independently verifiable evidence beyond a simple yes/no answer. In this short paper, we present two certificate checkers for hardware model checking, Certifaiger and Cerbtora, which target bit-level and word-level verification of hardware designs, respectively. Certifaiger has been adopted in recent editions of the Hardware Model Checking Competition, but not described in the literature before. Cerbtora extends the same theoretical framework to the word level, in which certificates are expressed in the same modeling language as the design under test and are validated using efficient automated reasoning engines. We describe the architecture and main components of both tools and evaluate them on competition benchmarks.

ABSTRACT. This paper introduces Pgeon, a meta-prover framework that generates tableau-based automated theorem provers from declarative specifications. In Pgeon, the syntax of a given calculus, its tableau inference rules, and the proof-search strategy are described in a small domain-specific language that closely follows textbook presentations. From such a specification, Pgeon instantiates a fully functional prover, handling tableau construction, rule instantiation, branching, and backtracking in a logic-agnostic manner. Proof-search is driven by a strategy engine that gives users explicit control over exploration order while keeping logical content separate from operational concerns. Pgeon supports first-order reasoning through binders, capture-avoiding substitution, and extensible term generators required for Skolemization and free variable introduction. We describe the design of the specification language, the execution model of the tool, and the strategy mechanism, and illustrate the approach on case studies covering classical and intuitionistic propositional calculi and classical first-order tableau calculi.

ABSTRACT. In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover. We introduce a proof minimization tool called Krympa. Using a combination of brute force and heuristics, and exploiting both Vampire and the Twee equational prover, the tool reduces the 62-step proof to 20 steps, each corresponding to a rewrite. In an empirical evaluation, it also performs well on 1431 equational problems originating from the same project, reducing in particular a 151-step proof to only 10 steps.

ABSTRACT. We address generating theorems from a given set of axioms, without proof goal, aiming at value from a mathematical point of view or as lemmas for automated proving. As benchmark, we convert a fragment of the Metamath database set.mm. Our techniques are centered on proof terms and condensed detachment. This ties in with automated first-order proving by proof structure enumeration, and links to Metamath and formulas-as-types. Our methods for generating theorems are based on partitioning the set of proof terms into inductively characterized levels. We study two ideas for improvement: Lemma synthesis by DAG compression of proof term sets, and incorporating combinators into proof terms. Our lemmas significantly improve solution rates of provers, e.g., of Vampire from 74% to 94%, and of leanCoP from 7% to 44%.

ABSTRACT. Lifting Boolean-reasoning techniques to the SMT level most often requires producing theory lemmas that rule out theory-inconsistent truth assignments. With standard SMT solving, it is common to "lazily" generate such lemmas on demand during the search. With some harder SMT-level tasks ---such as unsat-core extraction, MaxSMT, T-OBDD or T-SDD compilation--- it may be beneficial or even necessary to "eagerly" pre-compute all the needed theory lemmas upfront. Whereas in principle "classic" eager SMT encodings could do the job, they are specific for very few and easy theories, they do not comply with theory combination, and may produce lots of unnecessary lemmas. In this paper, we present theory-agnostic methods for enumerating complete sets of theory lemmas tailored to a given formula. Starting from AllSMT as a baseline approach, we propose several improved lemma-enumeration techniques, including divide&conquer, projected enumeration, and theory-driven partitioning, which are highly parallelizable and which may drastically improve scalability. An experimental evaluation demonstrates that these techniques significantly enhance efficiency and enable the method to scale to substantially more complex instances.

ABSTRACT. This paper presents a novel extension of the superposition calculus for reasoning about formulas in Separation Logic (SL). Our approach integrates the efficiency of saturation-based theorem proving with the expressive power of SL, which is widely used to describe and reason about memory heaps. The target logic strictly extends first-order equational logic with SL constructs built from points-to atoms and separating conjunctions. The resulting calculus retains the core strengths of the superposition paradigm while addressing the distinctive semantic challenges of SL. We prove that the calculus is sound and complete with respect to the standard redundancy criterion.

ABSTRACT. Several successful strategies in automated reasoning rely on human-supplied guidance about which term or clause shapes are interesting. In this paper we aim to discover interesting term shapes automatically. Specifically, we discover abstractions : term patterns that occur over and over again in relevant proofs. We present our tool Twitch which discovers abstractions with the help of Stitch, a tool originally developed for discovering reusable library functions in program synthesis tasks. Twitch can produce abstractions in two ways: (1) from a partial, failed proof of a conjecture; (2) from successful proofs of other theorems in the same domain. We have also extended Twee, an equational theorem prover, to use these abstractions. We evaluate Twitch on a set of unit equality (UEQ) problems from TPTP, and show that it can prove 12 rating-1 problems as well as yielding significant speed-ups on many other problems.

ABSTRACT. Let ${\cal T}$ be a theory allowing a form of elimination of existential quantifiers (possibly for formulae in a certain class). We analyze possibilities of constructing (most general) solutions w.r.t.\ ${\cal T}$ for formulae of the form $\exists x_1, \dots, \exists x_n \phi(x_1, \dots, x_n, y_1, \dots, y_m)$, where $\phi$ is a quantifier-free conjunction of literals in the signature of ${\cal T}$, and the free variables $y_1, \dots, y_m$ are regarded as parameters. We show that in the presence of function symbols which describe "{\sf if}-{\sf then}-{\sf else}" constructions in certain models of ${\cal T}$, we can describe the most general solution of such formulae, thus generalizing results about the existence of most general unifiers in discriminator varieties. We illustrate the ideas on examples.

ABSTRACT. We present a variant of the multiset path order for untyped applicative term rewriting. Compared to existing work, our variant incorporates two distinctive features, dubbed arity assignment and reification, to overcome difficulties in handling partial and variable application.

ABSTRACT. We report on the new ARI infrastructure that supports tools and competitions in term rewriting. It offers ARI-COPS, a database for confluence problems and competition results, and ARIWeb, a convenient web interface for tools that participate in the annual confluence competition. These are built on top of the new ARI format for rewrite systems, a format converter, certifiers for competition results, and a duplicate checker.