ABSTRACT. Verification of equivalence between two quantum circuits is a hard problem, that is nonetheless crucial in compiling and optimizing quantum algorithms for real-world devices. This paper introduces O(n + m)-length encoding realizing a Turing reduction of the (universal) quantum circuits equivalence problem to weighted model counting, where n is the number of qubits and $m$ the number of gates. To achieve this, we generalize a deterministic equivalence-checking algorithm based on the stabilizer formalism, which enables reasoning about universal quantum computing in the discrete domain. With an open-source implementation, we demonstrate that our approach works well in practice and often outperforms state-of-the-art equivalence checking tool based on ZX-calculus and decision diagrams. Our work paves the way to transfer the successes of classical reasoning tools to the quantum domain.

ABSTRACT. Our main result is a doubly exponential decision procedure for the first-order equality theory of streams with both arithmetic and control-oriented stream operations. This stream logic is shown to be expressive for solving basic problems of stream calculus.

ABSTRACT. The predicate definitions in Separation Logic (SL) play an important role: they introduce disjunctions and existential quantifications in fragments of SL not allowing the complete boolean fragment, and they capture a large spectrum of unbounded heap shapes due to their inductiveness. This expressiveness power comes with a limitation: the entailment problem is undecidable if predicates have general inductive definitions (ID). Iosif et al. proposed syntactic and semantic conditions, called PCE, on the ID of predicates to ensure the decidability of the entailment problem. We provide a (possibly non terminating) algorithm to transform arbitrary ID into equivalent PCE definitions, when possible. We show that the existence of an equivalent PCE definition for a given ID is undecidable, but we identify necessary conditions that are decidable.

ABSTRACT. This paper introduces a uniform substitution calculus for differential refinement logic dRL. The logic dRL extends the differential dynamic logic dL such that one can simultaneously reason about properties of and relations between hybrid systems. Uniform substitution is the key to parsimonious prover kernels. It enables the verbatim use of axioms instead of axiom schemata with soundness-critical side conditions scattered across the proof calculus. The uniform substitution rule can then be used to instantiate all axioms soundly. Access to differential variables enables more control over the notion of refinement, which is shown to be decidable on a fragment of hybrid programs.

ABSTRACT. Enhancing cut-free expressiveness through minimal structural additions to sequent calculus is a natural step. We focus on Aqvist's system F with cautious monotonicity (CM), a deontic logic extension of S5, for which we define a sequent calculus employing (semi) analytic cuts. The transition to hypersequents is key to develop modular and cut-free calculi for F+(cm) and G, also supporting countermodel construction.

ABSTRACT. In this paper we explore the design of sequent calculi operating on graphs. For this purpose, we introduce logical connectives allowing us to extend the well-known correspondence between classical propositional formulas and cographs. We define sequent systems operating on formulas containing such connectives, and we prove, using an analyticity argument based on cut-elimination, that our systems provide conservative extensions of multiplicative linear logic (without and with mix) and classical propositional logic. We conclude by showing that one of our systems captures graph isomorphism as logical equivalence, and that it is sound and complete for the graphical logic \GS.

ABSTRACT. We investigate the proof theory of regular expressions with fixed points, construed as a notation for context-free (omega-)grammars. Starting with a hypersequential system for regular expressions due to Das and Pous, we define its extension by least fixed points, and prove soundness and completeness of its non-wellfounded proofs for the standard language model. From here we apply proof theoretic techniques to recover an infinitary axiomatisation of the resulting equational theory, complete for inclusions of context-free languages. Finally we extend our syntax by greatest fixed points, now computing context-free omega-languages. We show soundness and completeness of the corresponding system using a mixture of proof theoretic and game theoretic techniques.

ABSTRACT. Guarded Kleene Algebra with Tests (GKAT for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about simple imperative while-programs. Following earlier work by Das and Pous on Kleene Algebra, we study GKAT from a proof-theoretical perspective. The deterministic nature of GKAT makes ordinary sequents sufficient for achieving regular completeness, unlike the situation with Kleene Algebra, where hypersequents are required. Moreover, the proof search induces a coNP decision procedure, rather than one in PSPACE.

ABSTRACT. The TPTP World is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. This work uses data in the TPTP World to assess progress in ATP from 2015 to 2023.

ABSTRACT. Modern superposition inference systems aim at reducing the search space by introducing redundancy criteria on clauses and inferences. This paper focuses on reducing the number of superposition inferences with a single clause by blocking inferences into some terms, provided there were previously made inferences of a certain form performed with predecessors of this clause. Other calculi based on blocking inferences, for example basic superposition, rely on variable abstraction or equality constraints to express irreducibility of terms, resulting however in blocking inferences with all subterms of the respective terms. Here we introduce reducibility constraints in superposition to enable a more expressive blocking mechanism for inferences. We show that our calculus remains (refutationally) complete and present redundancy notions. Our implementation in the Vampire prover demonstrates a great reduction in the size of the search space when using our new calculus.

ABSTRACT. Given a finite consistent set of ground literals, we present an algorithm that generates a complete first-order logic interpretation, i.e., an interpretation for all ground literals over the signature and not just those in the input set, that is also a model for the input set. The interpretation is represented by first-order linear literals. It can be effectively used to evaluate clauses. A particular application are SCL stuck states. The SCL calculus always computes with respect to a finite number of ground literals. It then finds either a contradiction or a stuck state being a model with respect to the considered ground literals. Our algorithm builds a complete literal interpretation out of such a stuck state model that can then be used to evaluate the clause set. If all clauses are satisfied an overall model has been found. If it does not satisfy some clause, this information can be effectively explored to extend the scope of ground literals considered by SCL.

ABSTRACT. To achieve the best performance, automatic theorem provers often rely on schedules of diverse proving strategies to be tried out (either sequentially or in parallel) on a given problem. In the Vampire prover, schedules were for a long time constructed by Andrei Voronkov using a tool called Spider, about which little was officially known until recently. After Andrei Voronkov's talk at the Vampire Workshop 2023, we decided to analyse this powerful technology on our own.

In this paper, we report on a large-scale experiment with discovering Vampire strategies targeting the FOF fragment of the TPTP library and constructing a schedule for it, based on the ideas of Spider. We examine the process from various angles, discuss the difficulty (or ease) of obtaining a strong Vampire schedule for the CASC competition, but also estimate how well can a schedule be expected to generalize to unseen problems and what factors influence this property.

ABSTRACT. This system description introduces an enhancement to the Yices2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits into the model-constructing satisfiability (MCSat) framework and is based on zero decomposition techniques, which find finite basis explanations for theory conflicts over finite fields. As the MCSat solver within Yices2 can support (and combine) several theories via theory plugins, we implemented our reasoning approach as a new plugin for finite fields and extended Yices2's frontend to parse finite field problems, making our implementation the first MCSat-based reasoning engine for finite fields. We present its evaluation on finite field benchmarks, comparing it against cvc5. Additionally, our work leverages the modular architecture of the MCSat solver in Yices2 to provide a foundation for the rapid implementation of further reasoning techniques for this theory.

ABSTRACT. In this work, we verify the mutable LongMap from the Scala standard library, a hash table using open addressing within a single array, using the Stainless program verifier. As a reference implementation, we write an immutable map based on a list of tuples. We then show that LongMap's operations correspond to operations of this association list. To express the resizing of the hash table array, we introduce a new reference swapping construct in Stainless. This allows us to apply the decorator pattern without introducing aliasing. Our verification effort led us to find and fix a bug in the original implementation that manifests for large hash tables. Our performance analysis shows the verified version to be within a 1.5 factor of the original data structure.

ABSTRACT. Recent approaches on verification and reasoning solve SAT and QBF encodings using state-of-the-art SMT solvers, as it "makes implementation much easier". The ease-of-use of these solvers make SAT and QBF solvers less visible to users of solvers---who are maybe from different research communities---potentially not exploiting the power of state-of-the-art tools. In this work, we motivate the need to build bridges over the widening solver-gap and introduce Booleguru, a tool to convert between formats for logic formulas. It makes SAT and QBF solvers more accessible by using techniques known from SMT solvers, such as advanced Python interfaces like Z3Py and easily generatable languages like SMT-LIB, integrating them to our conversion tool. We then introduce a language to manipulate and combine multiple formulas, optionally applying transformations for quickly prototyping encodings. Booleguru's advanced scripting capabilities form a programming environment specialized for Boolean logic, offering a more efficient way to develop novel problem encodings.