Accepted Papers

The accepted papers at PAAR 2024 are (sorted alphabetically by first author’s last name):

• Bruno Andreotti, Haniel Barbosa and Oliver Flatt. Producing shorter congruence closure proofs in a state-of-the-art SMT solver
  

  Abstract: The satisfiability of constraints in the theory of equality and uninterpreted functions, a core component of SMT solving, can be decided via a congruence closure algorithm. Classical congruence closure algorithms can provide machine checkable proofs when explaining why terms are equal. Recently, Flatt et al. presented a modified congruence closure algorithm producing demonstrably shorter proofs. The algorithm was implemented and evaluated in the context of equality saturation tools. In this extended abstract we present initial work on implementing this new congruence closure algorithm in cvc5, a state-of-the-art SMT solver. We discuss the challenges from adapting a high-performance implementation and how to address them effectively. We evaluate the implementation on a large set of SMT-LIB benchmarks, and demonstrate experimentally how this new algorithm results in smaller proofs in real-world scenarios. Moreover, we evaluate the performance impact of the new algorithm and determine whether the smaller explanations that can be generated from the shorter proofs are worth the performance overhead of the more expensive algorithm.

• Guy Axelrod and Willem Conradie. Prefixed Tableaux and Decision Procedures for Many-Valued Modal Logics
  Abstract: We introduce prefixed tableau systems for many-valued model logics (MVMLs). Semantically, we follow Fitting (1991, 1992) in allowing both the truth values of propositional variables at states as well as relational links between states in many-valued Kripke frames to take values in an arbitrary, finite Heyting algebra. Fitting (1995) introduced tableau systems for these logics which, however, are not amenable to specialization to the MVMLs of certain frame classes, e.g. generalized symmetric frames. We overcome this difficulty through the use of prefixes which keep explicit track of the many-valued accessibility relation constructed on each branch. We prove soundness and completeness of the systems for the MVMLs of the classes of all many-valued frames and all generalized symmetric many-valued frames. We prove that these systems provide decision procedures and discuss and demonstrate their implementations. Lastly we derive the finite model property for the the two logics under consideration.

• Filip Bártek, Karel Chvalovský and Martin Suda. Cautious Specialization of Strategy Schedules
  Abstract: Combining theorem proving strategies into schedules is a well-known recipe for improving prover performance, as a well-chosen set of complementary strategies in practice covers many more problems within a predetermined time budget than a single strategy could. A strategy schedule can be a monolithic sequence, but may also consist of multiple schedule branches, intended to be selected based on certain problem’s features and thus to specialize to solving the corresponding problem classes. When allowing schedule branching, there is an intuitive trade-off between covering the known (training) problems quickly, by splitting them into many classes, and the generalization of the obtained branching schedule, i.e., its ability to solve previously unseen (test) problems.
  In this paper, we attempt to shed more light on this trade-off. Starting with a large set of proving strategies of the automatic theorem prover Vampire evaluated on the first-order part of the TPTP library, we report on several experiments with building branching schedules while keeping track of how well they generalize to test problems.

• Julie Cailler and Simon Guilloud. SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
  Abstract: Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify a text format to describe proofs in first order logic: -SC-TPTP. To avoid multiplication of standards, our proposed format is a super-specification of the TPTP derivation format. Our format focuses on sequent-calculus-like formalisms, which provide a high level of details, are faithful to the mathematical dogma and cover multiple existing tools and in particular tableaux-based strategies. In addition, we made use of this format to allow interactions between the Lisa proof assistant and the Goéland automated theorem prover, and implemented a tool able to reconstruct proofs from this format and export it into Lisa and Coq to be checked.

• Adam Dingle. A Natural-Language Proof Assistant for Higher-Order Logic (Work in Progress)
  Abstract: Natty is a new proof assistant in an early stage of development. It can read input written in a controlled natural language that looks like mathematical English with a restricted grammar and vocabulary. It translates this input to a series of formulas of classical higher-order logic. It can export these formulas to files in the standard THF format, or can attempt to prove them itself using a built-in automatic prover based on a pragmatic, incomplete variant of the higher-order superposition calculus. The built-in prover clausifies formulas incrementally to preserve as much structure as possible as it performs inferences. Although Natty is small (fewer than 3000 lines of OCaml code), its performance seems to be competitive with established provers such as E and Vampire in proving some basic arithmetic identities involving induction over natural numbers. In addition, the THF files that it generates for arithmetic identities may serve as a useful test set for other higher-order provers.

• Alexander Steen and Geoff Sutcliffe. TPTP World Infrastructure for Non-classical Logics
  Abstract: The TPTP World is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. Until now the TPTP World has focused on classical logic, while many real-world applications of ATP also require non-classical reasoning. This paper describes the latest extensions to the TPTP World, providing languages, problems, solutions, and infrastructure for non-classical logics. These are the keys steps towards releasing TPTP v9.0.0, with normal modal logic problems.