ABSTRACT. Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of model checking results, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time.

ABSTRACT. Intuitionistic Strong Löb logic ISL is a well-known intuitionistic modal logic with a provability interpretation. We introduce GbuSL a terminating sequent calculus with the subformula property for ISL. GbuSL modifies the sequent calculus G3iSL for iSL based on G3i, by annotating the sequents to distinguish rule applications into an unblocked phase, where any rule can be backward applied, and a blocked phase where only right rules can be used. We prove that, if proof-search for a sequent s in GbuSL fails, then a Kripke countermodel for s can be constructed.

ABSTRACT. Focusing is a known technique for reducing the number of proofs while preserving derivability. Skolemization is another technique designed to improve proof search, which reduces the number of back-tracking steps by representing dependencies on the term level and instantiate witness terms during unification at the axioms or fail with an occurs-check otherwise. Skolemization for classical logic is well understood, but a practical skolemization procedure for intuitionistic linear logic has been elusive so far. In this paper we present a focused variant of first-order intuitionistic linear logic together with a sound and complete skolemization procedure.

ABSTRACT. We investigate intuitionistic modal logics with local modalities, where both modalities are defined locally, exactly the same as in classical logic. Semantically these logics are characterized by suitable frame properties that ensure the hereditary property, whence conservativity over intuitionistic logic. The basic logic LIK (local IK) is stronger than constructive modal logic CK and incomparable with Fischer-Servi or Simpson's IK. We propose an axiomatization of the basic logic LIK and its extensions on serial, reflexive, and transitive frames. Whereas the basic LIK does not satisfy the disjunctive property, its extension with seriality or reflexivity does. We further propose bi-nested sequent calculi for LIK and its extensions which provide both a decision procedure and finite countermodel extraction.

ABSTRACT. Dependency pairs are one of the most powerful techniques for proving termination of term rewrite systems (TRSs), and they are used in almost all tools for termination analysis of TRSs. Problem #106 of the RTA List of Open Problems asks for an adaption of dependency pairs for relative termination. Here, infinite rewrite sequences are allowed but one wants to prove that a certain subset of the rewrite rules cannot be used infinitely often. Dependency pairs were recently adapted to annotated dependency pairs (ADPs) to prove almost-sure termination of probabilistic TRSs. In this paper, we develop a novel adaption of ADPs for relative termination. We implemented our new ADP framework in our tool AProVE and evaluate it in comparison to state-of-the-art tools for relative termination of TRSs.

ABSTRACT. We show that (local) confluence of terminating locally constrained rewrite systems is undecidable, even when the underlying theory is decidable. Several confluence criteria for logically constrained rewrite systems are known. These were obtained by replaying existing proofs for plain term rewrite systems in a constrained setting, involving a non-trivial effort. We present a simple transformation from logically constrained rewrite systems to term rewrite systems such that critical pairs of the latter correspond to constrained critical pairs of the former. The usefulness of the transformation is illustrated by lifting the advanced confluence results based on (almost) development closed critical pairs as well as on parallel critical pairs to the constrained setting.

ABSTRACT. Naproche-ZF is a new experimental open-source natural theorem prover based on set theory; formalizations in Naproche-ZF are written in a controlled natural language embedded into LaTeX and proof gaps are filled in with automated theorem provers. Naproche-ZF aims to scale natural theorem proving beyond chapter-sized formalizations. In contrast to Naproche-SAD, the new system uses an extensible grammar-based approach, has more efficient proof automation, and enables larger interconnected formalizations based on a standard library.

ABSTRACT. Recently, we showed how to use control-flow refinement (CFR) to improve automatic complexity analysis of integer programs. While up to now CFR was limited to classical programs, in this paper we extend CFR to probabilistic programs and show its soundness for complexity analysis. To demonstrate its benefits, we implemented our new CFR technique in our complexity analysis tool KoAT.

ABSTRACT. The support for higher-order reasoning in the Vampire theorem prover has recently been completely reworked. This rework consists of new theoretical ideas, a new implementation, and a dedicated strategy schedule. The theoretical ideas are still under development, so we discuss them at a high level in this paper. We also describe the implementation of the calculus in the Vampire theorem prover, the strategy schedule construction, and several empirical performance statistics.

ABSTRACT. We turn saturation-based theorem proving into an automated framework for recursive program synthesis. We introduce magic axioms as valid induction axioms and use them together with answer literals in saturation. We introduce new inferences rules for induction in saturation and use answer literals to synthesize recursive functions from these proof steps. Our proof-of-concept implementation in the Vampire theorem prover constructs recursive functions over algebraic data types, while proving inductive properties over these types.

ABSTRACT. We show a projective Beth definability theorem for logic programs under the stable model semantics: For given programs $P$ and $Q$ and vocabulary $V$ (set of predicates) the existence of a program $R$ in $V$ such that $P \cup R$ and $P \cup Q$ are strongly equivalent can be expressed as a first-order entailment. Moreover, our result is effective: A program $R$ can be constructed from a Craig interpolant for this entailment, using a known first-order encoding for testing strong equivalence, which we apply in reverse to extract programs from formulas. As a further perspective, this allows transforming logic programs via transforming their first-order encodings. In a prototypical implementation, the Craig interpolation is performed by first-order provers based on clausal tableaux or resolution calculi. Our work shows how definability and interpolation, which underlie modern logic-based approaches to advanced tasks in knowledge representation, transfer to answer set programming.

ABSTRACT. We investigate how the automated inductive proof capabilities of the first-order prover Vampire can be improved by adding lemmas conjectured by the QuickSpec theory exploration system and by training strategy schedules specialized for inductive proofs. We find that adding lemmas improves performance (measured in number of proofs found for benchmark problems) by 40% compared to Vampire's plain structural induction as baseline. Strategy training alone increases the number of proofs found by 130%, and the two methods in combination provide an increase of 183%. By combining strategy training and lemma discovery we can prove more inductive benchmarks than previous state-of-the-art inductive proof systems (HipSpec and CVC4).

ABSTRACT. Bachmair's and Ganzinger's abstract redundancy concept for the Superposition Calculus justifies almost all operations that are used in superposition provers to delete or simplify clauses, and thus to keep the clause set manageable. Typical examples are tautology deletion, subsumption deletion, and demodulation, and with a more refined definition of redundancy joinability and connectedness can be covered as well. The notable exception is destructive equality resolution, that is, the replacement of a clause x ≉ t ∨ C with x ∉ vars(t) by C{x ↦ t}. This operation is implemented in state-of-the-art provers, and it is clearly useful in practice, but little is known about how it affects refutational completeness. We demonstrate on the one hand that the naive addition of destructive equality resolution to the standard abstract redundancy concept renders the calculus refutationally incomplete. On the other hand, we present several restricted variants of the superposition calculus that are refutationally complete even with destructive equality resolution.