ABSTRACT. Choices in the semantics and the signature of a theory are integral in determining how the theory is used and how hard it is to reason over it. Our interest in this paper lies in the SMT theory of sequences. Various versions of it exist in the literature and in state-of-the-art SMT solvers, but it has not yet been standardized in the SMT-LIB. We reflect on its existing variants, and we define a set of theory design criteria to help determine what makes a variant of a theory better than another. The criteria we define can be used to appraise theory proposals for other theories as well. Based on these criteria, we propose a series of changes to the SMT theory of sequence as a contribution to the discussion regarding its standardization.

ABSTRACT. In this work, we consider two sets I and O of bounded integer variables, modeling the inputs and outputs of a program. Given a specification Post, which is a Boolean combination of linear or polynomial inequalities with real coefficients over I ∪ O, our goal is to synthesize the weakest possible pre-condition Pre and a program P satisfying the Hoare triple {Pre}P{Post}. We provide a novel, practical, sound and complete algorithm, based on dynamic gridding, Farkas’ Lemma and Handelman’s Theorem, that synthesizes both the program P and the pre-condition Pre, over a bounded integral region. Our approach is exact and guaranteed to find the weakest pre-condition. Moreover, it always synthesizes both P and Pre as linear decision lists. Thus, our output consists of simple programs and pre-conditions that facilitate further static analysis. We also provide experimental results over benchmarks showcasing the real-world applicability of our approach and considerable performance gains over the state-of-the-art.

ABSTRACT. While many of the state-of-art Automated Theorem Provers (ATP) like E and Vampire, were subject to extensive tuning of strategy schedules in the last decade, the classical ATP prover Prover9 has never been optimized in this direction. Both E and Vampire provide the user with an automatic mode to select good proof search strategies based on the properties of the input problem, while Prover9 provides by default only a relatively weak auto mode. Interestingly, Prover9 provides more varied means for proof control than its competitors. These means, however, must be manually investigated and that is possible only by experienced Prover9 users with a good understanding of how Prover9 works.

In this paper, we investigate the possibilities of automatic configuration of Prover9 for user-specified benchmark problems. We employ the automated strategy invention system Grackle to generate Prover9 strategies with both basic and advanced proof search options which require sophisticated strategy space features for Grackle. We test the strategy invention on AIM train/test problem collection and we show that Prover9 can outperform both E and Vampire on these problems. To test the generality of our approach we train and evaluate strategies also on TPTP problems, showing that Prover9 can achieve reasonable complementarity with other ATPs.

ABSTRACT. Intersection type systems have been independently applied to different evaluation strategies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been generalized to different subsuming paradigms being able, in particular, to encode CBN and CBV in a unique unifying framework. However, there are no intersection type systems that explicitly enable CBN and CBV to cohabit together without making use of an encoding into a common target framework. This work proposes an intersection type system for PCF with a specific notion of evaluation, called PCFH. Although this form of evaluation is sometimes referred to as “call-by-value”, evaluation in PCFH actually has a hybrid nature, in the sense that CBN and CBV operational behaviors cohabit together. Indeed, PCFH combines a CBV-like operational behavior for function application with a CBN-like behavior for recursion. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFH: not only that typability implies normalization, but also the converse holds. Moreover, the type system is quantitative, in the sense that the size of typing derivations provides upper bounds for the length of the normalization sequences to normal form. This type system is then refined to a tight one, offering exact information regarding the length of normalization sequences.

ABSTRACT. We present a method and a tool, hol2dk, to automatically translate proofs from the proof assistant HOL-Light to the proof assistant Coq, by using Dedukti as intermediate language. Moreover, a number of types, functions and predicates that are defined in HOL-Light are mapped to their counterparts in the Coq standard library, and these mappings are certified in Coq. Therefore, the obtained library can directly be used and applied in other Coq developments.

ABSTRACT. The logical framework of Constrained Horn Clauses (CHC) models verification tasks from a variety of domains, ranging from verification of safety properties in transition systems to modular verification of programs with procedures. In this work we present Golem, a flexible and efficient solver for satisfiability of CHC over linear real and integer arithmetic. Golem provides flexibility with modular architecture and multiple back-end model-checking algorithms, as well as efficiency with tight integration with the underlying SMT solver. This paper describes the architecture of Golem and its back-end engines, which include our recently introduced model-checking algorithm TPA for deep exploration. The description is complemented by extensive evaluation, demonstrating the competitive nature of the solver.

ABSTRACT. Achieving high test coverage is important when developing blockchain smart contracts, but it could be challenging witout automated reasoning tools. In this paper, we present SolTG, an automated test case generator for Solidity smart contracts based on Constrained Horn clauses (CHC). Test cases synthesized by SolTG have the form of a sequence of function calls over concrete values of input parameters, which lead to a specific execution scenario. SolTG exhaustively enumerates CHC-based symbolic constraints that encode the given contract and finds those input values. The tool supports multiple Solidity-specific features and is capable of generating high coverage for industrial-grade Solidity code. We present a detailed architecture of SolTG and the translation of smart contracts into their CHC representation that the tool relies on. We also present the experimental results for test generation on a set of public benchmarks.

ABSTRACT. We propose a translation from eBPF (extended Berkeley Packet Filter) code to CHC (Constrained Horn Clause sets) over the combined theory of bitvectors and arrays. eBPF is in particular used in the Linux kernel where user code is executed under kernel privileges. In order to protect the kernel, a well-known verifier statically checks the code for any harm and a number of research efforts have been performed to secure and improve the performance of the verifier. This paper is about verifying the functional properties of the eBPF code itself. Our translation procedure bpfverify is precise and covers almost all details of the eBPF language. Functional properties are automatically verified using z3. We prove termination of the procedure and show by real world eBPF code examples that full-fledged automatic verification is actually feasible.

ABSTRACT. Hyperedge-Replacement grammars (HR) have been introduced by Courcelle in order to extend the notion of context-free sets from words and trees to graphs of bounded tree-width. While for words and trees syntactic grammar restrictions are known that guarantee that the associated languages of words resp. trees are regular - and hence, MSO definable - the situation is more complicated for graphs. Here, Courcelle proposed the notion of regular graph grammars, a syntactic restriction of HR grammars that guarantees the definability of the associated languages of graphs in Counting Monadic Second Order Logic (CMSO). However, these grammars are not complete in the sense that not every CMSO definable set of graphs of bounded tree-width can be generated by a regular graph grammar. In this paper, we introduce a new syntactic restriction of HR grammars, called tree-verifiable graph grammars, and a new notion of bounded tree-width, called embeddable bounded tree-width, where the later restricts the trees of a tree-decomposition to be a subgraph of the analyzed graph. The main property of tree-verifiable graph grammars is that their associated languages are CMSO definable and that the have bounded embeddable tree-width. We show further that they strictly generalize the regular graph grammars of Courcelle. Finally, we establish a completeness result, showing that every language of graphs that is CMSO definable and of bounded embeddable tree-width can be generated by a tree-verifiable graph grammar.

ABSTRACT. Sorting networks are sorting algorithms that execute a sequence of operations independently of the input. Since they can be implemented directly as circuits, sorting networks are easy to implement in hardware -- but they are also used often in software to improve performance of base cases of standard recursive sorting algorithms. For this purpose, they are translated them into machine-code instructions in a systematic way.

Recently, a deep-learning system discovered better implementations than previously known of some sorting networks with up to 8 inputs. In this article, we show that all these examples are instances of a general pattern whereby some instructions are removed. We show that this removal can be done when a particular set of constraints on integers is satisfiable, and identify conditions where we can reduce this problem to propositional satisfiability. We systematically apply this general construction to improve the best-known implementations of sorting networks of size up to 128, which are the ones most commonly found in software implementations.

ABSTRACT. The various possible semantics of Dijkstra’s guarded commands are elucidated by means of a new graph-based low-level, generic specification language designed for asynchronous nondeterministic algorithms. The graphs incorporate vertices for actions and edges indicating control flow alongside edges for data flow. This formalism allows one to specify, not just input-output behavior nor only what actions take place, but also precisely how often and in what order they transpire.

ABSTRACT. Algorithm certification or program verification have an increasing importance in the current technological landscape, due to the sharp increase in the complexity of software and software using systems and the high potential of adverse effects in case of failure. For instance robots constitute a particular class of systems that can present high risks of such failures. Sorting on the other hand has a growing area of applications, in particular the ones where organizing huge data collections is critical, as for instance in environmental applications.

We present an experiment in formal certification of an original version of the Bubble-Sort algorithm that is functional and tail recursive. The certification is performed in parallel both in Theorema and in Coq, this allows to compare the characteristics and the performance of the two systems. In Theorema the proofs are produced automatically in natural style (similar to human proofs), while in Coq they are based on scripts. However, the background theory, the algorithms, and the proof rules in \tma are composed by the user without any restrictions -- thus error prone, while in Coq one can only use the theories and the proof rules that are rigurously checked by the system, and the algorithms are checked for termination.

The goal of our experiments is to contribute to a better understanding and estimation of the complexity of such certification tasks and to create a basis for further increase of the level of automation in the two systems and for their possible integration.

ABSTRACT. Certifying results by checking proofs and models is an essential feature of modern SAT solving. Even though incremental solving with assumptions and core extraction is crucial for many applications support for incremental proof certificates is lacking. We propose a proof format for incremental SAT solving and corresponding checkers. We further extend it to make use of resolution hints. Experiments on incremental SAT solving for satisfiability modulo theories and bounded model checking show the feasibility of our approach, again also confirming that resolution hints substantially reduce checking time.

ABSTRACT. We introduce a simple game of resource-conscious reasoning. In this two-player game, players Proponent and Opponent simultaneously place tokens of positive and negative polarity onto a game board. Proponent wins if she manages to match every negative token with a corresponding positive token.

We study the game using methods from computational complexity and proof theory. Specifically, we show complexity results for various fragments of the game, including PSPACE-completeness of a finite restriction of the game and undecidability of the full game featuring infinite plays. Determinacy, that is the existence of a winning strategy for one of the players, can be shown for the full game. Moreover, we show that the finitary version of the game is axiomatisable and can be faithfully embedded into exponential-free linear logic. The full game satisfies the exponential rules of linear logic, but is not fully captured by it.

ABSTRACT. We demonstrate utility of generic automated reasoning (AR) methods in the computational topology domain, evidencing the benefit of the use of existing AR machinery within the domain on the one hand, whilst providing a pathway into a rich playground with potential to drive future AR requirements. We also progress towards quantum software verification contribution, via a recent proposal to use tangles as a representation of a certain class of quantum programs. The general methodology is, roughly speaking, to transform tasks of equivalence of topological objects (tangles) into equivalence of algebraic objects (pointed quandles) and those in turn translate into AR tasks. To enhance trust in automated checks, this can be followed by interpretation of AR outputs as human-readable output, either in symbolic algebraic form suitable for domain experts or ideally in visual topological form, potentially suitable for all. We provide formalisation via an appropriate class of labelled tangles (suitable for Quantum Verification) with associated algebraic invariants (pointed involutory quandles) and translate equivalence checking of these invariants to equational reasoning tasks. Furthermore, subsequent to automated proof creation for simple quantum verification (QV) examples, we demonstrate manual extraction of visual proof rules and visual equivalence, utilising proof graphs as a bridging step, progressing towards the automation of human-readable visual proofs.

ABSTRACT. Group polarization, the phenomenon where individuals' opinions become more extreme after interacting, has gaining attention, specially with the rise of social media influencing social, political, and democratic processes. Recent interest has emerged in formal reasoning about group polarization using logical systems. In this paper we consider the modal logic PNL that captures the notion of agents agreeing or disagreeing on a given topic.Our contribution is to endow PNL with more effective formal reasoning techniques, instead of reasoning about group polarization using Hilbert axiomatic systems. First, we introduce a semantic game for (hybrid) extensions of PNL, which supports a dynamic form of reasoning about concrete network models. We show how this semantic game leads to a provability game, by systemically exploring the truth in all models. This leads to the first Gentzen-style cut-free sequent systems for some variants of PNL. Interestingly enough, using polarization of formulas, the proposed sequent systems can be modularly adapted to consider different frame properties of the underlying model.

ABSTRACT. We present a reasoning framework in support of establishing the functional correctness of programs with recursive data structures with automated first-order theorem proving. Specifically, we focus on functional programs implementing sorting algorithms.

We formalize the semantics of recursive programs in many-sorted first-order logic while introducing sortedness/permutation properties as part of our first-order formalization. Rather than focusing on sorting lists of elements of specific first-order theories such as integer arithmetic, our list formalization relies on a sort parameter abstracting (arithmetic) theories and, hence, concrete sorts. Additionally we formalize the permutation property of lists in first-order logic in an effective way that allows to automatically discharge verification conditions of such algorithms purely by means of first-order theorem proving.

Proof search is powered by automated theorem proving: we adjust recent efforts for automating inductive reasoning in saturation-based first-order theorem proving. Importantly, we advocate a compositional reasoning approach for automating proofs by induction required to verify functional programs implementing and preserving sorting and permutation properties over parameterized list structures. We showcase the applicability of our framework over recursive sorting algorithms, including Mergesort and Quicksort; to this end, we turn first-order theorem proving into an automated verification engine by guiding automated inductive reasoning with manual proof splits.

ABSTRACT. We give an evaluation system for the admissibility of rules in intuitionistic proportional logic. The system is based on recent work on the proof-theoretic semantics of IPL.

ABSTRACT. We provide the first proof of confluence for cut elimination in multiplicative-exponential linear logic proof-nets that is not based on Newman's lemma or strong normalization, not even indirectly. To achieve our goal, we take inspiration from Tait and Martin-Lof's method based on parallel reduction for the lambda-calculus, even though the wilder realm of untyped proof-nets makes the proof subtler and more challenging.

ABSTRACT. Rewriting techniques based on reduction orderings generate “just enough” consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem proving, but for at least one approach to inductive reasoning we show that we are missing crucial consequences. We therefore extend the superposition calculus with rewriting-based techniques to generate sufficient consequences for automating induction in saturation. When applying our work within the unit-equational fragment, our experiments with the theorem prover Vampire show significant improvements for inductive reasoning.

ABSTRACT. Epistemic processes describe the dynamic behaviour of multi-agent systems driven by the knowledge of agents, which perform epistemic actions that may lead to knowledge updates. Executing epistemic processes directly on epistemic states, given in the traditional way by pointed Kripke structures, quickly becomes computationally expensive due to the semantic update constructions. Based on an abstraction to formulae of interest, we introduce a symbolic epistemic state representation and a notion of representable epistemic action with efficient symbolic updates. In contrast to existing work on belief or knowledge bases, our approach can handle epistemic actions modelled by arbitrary action models. We introduce an epistemic process calculus and a propositional dynamic logic for specifying process properties that can be interpreted both on the concrete semantic and the symbolic level. We show that our abstraction technique preserves and reflects dynamic epistemic process properties whenever processes are started in a symbolic state that is an abstraction of a semantic epistemic state.

ABSTRACT. We introduce and discuss a term-rewriting technique to convert numbers from any numeric base to any other one without explicitely appealing to division. The rewrite system is purely local and conversion has a quadratic complexity, matching the one of the standard base-conversion algorithm. We prove confluence and termination, and give an implementation and benchmarks in the Dedukti type checker. This work extends and generalizes a previous work by Delahaye, published in a vulgarization scientific review.

ABSTRACT. We introduce a software tool for reasoning about belief change in situations where information is received from reports and observations. Our focus is on the interaction between trust and belief. The software is based on a formal model where the level of trust in a reporting agent increases when they provide accurate reports and it decreases when they provide innaccurate reports. If trust in an agent drops below a given threshold, then their reports no longer impact our beliefs at all. The notion of accuracy is determined by comparing reports to observations, as well as to reports from more trustworthy agents. The emphasis of this paper is not on the formalism; the emphasis is on the development of the prototype system for automatically calculating the result of iterated revision problems involving trust. We present an implemented system that allows users to flexibly specify and solve complex revision problems involving reports from partially trusted sources.

ABSTRACT. For tutorial purposes we realized a propositional prover in the Theorema system that works in natural style and is based on sequent calculus with unit propagation.

The version of the sequent calculus that we use is a reductionist one: at each step a formula is decomposed according to a fixed rule attached to its main logical connective. Optionally the prover may use unit propagation. Unit propagation in sequent calculus is a novel inference method introduced by the author that consists in propagating literals that occur either as antecedents of postcedents in the sequent: all occurrences of such a literal in any of the other formulae are replaced by the corresponding truth value and the respective formula is simplified by rewriting.

By natural style we understand a style similar to human activity. This applies to syntax of formulae, to inference steps, and to proof presentation. Although bases on sequent calculus, the prover does not produce proofs as sequent proof trees, but as natural style narratives.

The purpose of the tool is tutorial for the understanding of natural style proving, of sequent calculus, and of the implementation in the Theorema system as a set of rewrite rules for the inferences, and a set of accompanying patterns for the explanatory text produced by the prover.

ABSTRACT. Deep inference is a proof theoretical formalism that generalises the “shallow inference” of the sequent calculus by permitting the application of inference rules like term rewriting rules. Deep inference makes it possible to access shorter proofs than sequent calculus; however, with the cost of increased nondeterminism, an obstacle in front of proof search applications. Deep inference is essential for designing system BV, an extension of multiplicative linear logic (MLL) with a self-dual non-commutative operator. MLL has shallow inference systems, whereas BV is impossible with a shallow-only system. As Tiu showed, any restriction on rule depth makes a system incomplete for BV. This paper shows that any restriction that rules out shallow rules makes the system incomplete, too. Our results indicate that for system BV, shallow and deep rules must coexist for completeness. We provide extensive empirical evidence that deep inference can still be faster than shallow inference when used strategically with a proof theoretical technique for reducing nondeterminism. We show that prioritising deeper rule instances reduces the cost of proof search by reducing the size of the managed contexts, consequently providing more immediate access to shorter proofs. Moreover, we identify a class of MLL formulae with deep inference proof search times that grow linearly in the number of atoms in contrast to an exponential growth pattern with shallow inference. We introduce a large and exhaustive benchmark for MLL, with and without mix, and a proof search framework to apply various search strategies, which should be of independent interest.

ABSTRACT. One of the main challenges in the area of Neuro-symbolic AI is to perform logical reasoning in the presence of neural and symbolic datasets. This requires the combination of heterogeneous data sources such as knowledge graphs, neural model predictions, structured databases, crowd-sourced data, and many more. In this paper we introduce $t$-Datalog$^\exists$ as a formalism for such reasoning tasks, $t$-Datalog$^\exists$ generalises of Datalog with existential rules or Datalog$^\exists$ (also commonly referred to as tuple-generating dependencies) by allowing the use of arbitrary t-norms in place of classical conjunction in rule bodies. The resulting formalism combines the best of both worlds. It extends the power and flexibility of Datalog$^\exists$ to neuro-symbolic reasoning tasks while preserving many of the desirable properties of the classical case. In particular, we show that natural extensions of the chase to our setting produces \emph{fuzzy universal models}, and that the complexity of reasoning in important decidable fragments remains the same as in the classical setting.

ABSTRACT. We present recent developments in the applications of automated theorem proving in the investigation of the Andrews-Curtis conjecture. We demonstrate previously unknown simplifications of groups presentations from a parametric family $MS_{n}(w_{\ast})$ of trivial group presentations for $n = 3,4,5,6,7$ (subset of well-known Miller-Schupp family). Based on the human analysis of these simplifications we formulate two conjectures on the structure of simplifications for the infinite family $MS_{n}(w_{\ast})$, $n \ge 3$.

This is an extended and updated version of the abstract presented at AITP 2023 conference.

ABSTRACT. The epsilon calculus gives the impression to provide shorter proofs than other proof mechanisms. Consequently, Toshio Arai asked "What is the expense to translate a derivation with cuts in the sequent formulation of epsilon calculus to LK derivations with cuts?". We provide as partial answer to the question a proof that there is no function Psi such that a cut-free derivation in a sequent calculus variant of the epsilon calculus with size n can be elementarily translated to an LK derivation with size and cut degree Psi(n). The main property of the epsilon calculus used is its ability to overbind bound variables.

ABSTRACT. Inductive proofs can be represented as a proof schemata, i.e. as a parameterized sequence of proofs defined in a primitive recursive way. Applications of proof schemata can be found in the area of automated proof analysis where the schemata admit (schematic) cut-elimination and the construction of Herbrand systems. This work focuses on the expressivity of proof schemata. We show that proof schemata can simulate primitive recursive arithmetic as defined Takeuti's Proof Theory. Future research will focus on an extension of the simulation to primitive recursive arithmetic using quantification. The translation of proofs in arithmetic to proof schemata can be considered as a crucial step in the analysis of inductive proofs.

ABSTRACT. An inductive proof can be represented as a proof schema, i.e. as a parameterized sequence of proofs defined in a primitive recursive way. A corresponding cut-elimination method, called schematic CERES, can be used to analyze these proofs, and to extract their (schematic) Herbrand sequents, even though Herbrand's theorem in general does not hold for proofs with induction inferences. This work focuses on the most crucial part of the schematic cut-elimination method, which is to construct a refutation of a schematic formula that represents the cut-structure of the original proof schema. Moreover, we show that this new formalism allows the extraction of a structure from the refutation schema, called a Herbrand schema, which represents its Herbrand sequent.

ABSTRACT. In this paper we demonstrate how logic programming systems and Automated first-order logic Theorem Provers (ATPs) can improve the accuracy of Large Language Models (LLMs) for logical reasoning tasks where the baseline performance is given by direct LLM solutions. We first evaluate LLM reasoning on steamroller problems using the PRONTOQA benchmark. We show how accuracy can be improved with a neuro-symbolic architecture where the LLM acts solely as a front-end for translating a given problem into a formal logic language and an automated reasoning engine is called for solving it. However, this approach critically hinges on the correctness of the LLM translation. To assess this translation correctness, we secondly define a framework of syntactic and semantic error categories. We implemented the framework and used it to identify errors that LLMs make in the benchmark domain. Based on these findings, we thirdly extended our method with capabilities for automatically correcting syntactic and semantic errors. For semantic error correction we integrate first-order logic ATPs, which is our main and novel contribution. We demonstrate that this approach reduces semantic errors significantly and further increases the accurracy of LLM logical reasoning.

ABSTRACT. LPTP (Logic Program Theorem Prover) is an interactive natural-deduction-based theorem prover for pure Prolog programs with negation as failure, unification with the occurs check, and a restricted but extensible set of built-in predicates. With LPTP, one can formally prove termination and partial correctness of such Prolog programs. LPTP was designed in the mid 90's by Robert F. Staerk. It is written in ISO-Prolog and comes with an Emacs user-interface.

From a theoretical point of view, in his publications about LPTP, Staerk associates a set of first-order axioms IND(P) to the considered Prolog program P. IND(P) contains the Clark's equality theory for P, definitions of success, failure and termination for each user-defined logic procedure in P, axioms relating these three points of view, and an axiom schema for proving inductive properties. LPTP is thus a dedicated proof editor where these axioms are hard-wired.

We propose to explicit these axioms as first-order formulas (FOFs), and apply automated theorem provers to check the property of interest. Using FOF as an intermediary language, we experiment the use of automated theorem provers for Prolog program verification. We evaluate the approach over a benchmark of about 400 properties of Prolog programs from the library available with LPTP. Both the compiler which generates a set of FOF files from a given input Prolog program together with its properties and the benchmark are publicly available.

ABSTRACT. We present a number of first- and second-order extensions to SMT theories specifically aimed at representing and analyzing SQL queries with join, projection, and selection operations. We support rea- soning about SQL queries with either bag or set semantics for database tables. We provide the former via an extension of a theory of finite bags and the latter via an extension of the theory of finite relations. Fur- thermore, we add the ability to reason about tables with null values by introducing a theory of nullable sorts based on an extension of the the- ory of algebraic datatypes. We implemented solvers for these theories in the SMT solver cvc5 and evaluated them on two sets of benchmarks derived from public sets of SQL equivalence problems. A comparative evaluation with the state of the art in automated SQL verification shows competitive performance in the benchmarks we support. While follow- ing bag semantics cvc5 proves less benchmarks compared to SPES and SQLSolver tools, it finds counterexamples for inequivalent queries that are claimed to be proven by other tools. When analyzing the same set of benchmarks with set semantics, our implementation of cvc5 shows compelling advantages compared to SPES.

ABSTRACT. We present our tool FuncTion-V for the automatic identification of the minimal sets of program variables that an attacker can control to ensure an undesirable program property. FuncTion-V supports program properties expressed in Computation Tree Logic (CTL), and builds upon an abstract interpretation-based static analysis for CTL properties that we extend with an abstraction refinement process. We showcase our tool on benchmarks collected from the literature and SV-COMP 2023.

ABSTRACT. The CVC5 solver is today one of the strongest systems for solving first order problems with theories but also without them. In this work we equip the enumeration-based instantiation method with a neural network that guides the choice of instantiated quantifiers and their ground instances. For that we develop a relatively fast graph neural network that repeatedly scores all available instantiation options with respect to the available formulas. The network runs directly on a CPU without the need for any special hardware. We train the neural guidance on a large set of proofs generated by the e-matching instantiation strategy and evaluate its performance on a set of previously unseen problems.

ABSTRACT. We present the CheckMate tool for the automated verification of game-theoretic security properties, with application to blockchain protocols. CheckMate applies automated reasoning techniques to determine whether a game-theoretic protocol model is game-theoretically secure, that is, Byzantine fault tolerant and incentive compatible. We describe CheckMate’s input format and its various components, modes, and output. CheckMate is evaluated on 14 benchmarks, including models of decentralized protocols, board games, and game-theoretic examples.

ABSTRACT. Recently an extension to higher-order logic — called DHOL — was introduced, enrich- ing the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice can be added to DHOL. We extend the DHOL term structure by Hilbert’s indefinite choice operator ϵ, define a translation of the choice terms to HOL choice that extends the existing translation and show that the extension of the translation is sound and complete. We finally evaluate the extended translation on a set of dependent HOL problems that require choice.

ABSTRACT. In this paper, we present a general strategy that enables the translation of tableau proofs using different Skolemization rules into machine-checkable proofs. It is part of a framework that enables (i) instantiation of the strategy into algorithms for different set of tableau rules (e.g., different logics) and (ii) easy soundness proof which relies on the local extensibility of user-defined rules. Furthermore, we propose an instantiation of this strategy for first-order tableaux that handles notably δ++ rules, which is, as far as the authors know, the first one in the literature. Additionally, this deskolemization strategy has been implemented in the Goéland automated theorem prover, enabling an export of its proofs in Coq and Lambdapi. Finally, we have evaluated the algorithm performances for δ+ and δ++ rules through the certification of proofs from some categories of the TPTP library.

ABSTRACT. We introduce Virtual Integer-Real Arithmetic Substitution (VIRAS), a quantifier elimination procedure for deciding quantified linear mixed integer-real arithmetic problems. VIRAS combines the framework of virtual substitutions with conflict-driven proof search and linear integer arithmetic reasoning based on Cooper’s method. We demonstrate that VIRAS gives an exponential speedup over state-of-the-art methods in quantified arithmetic reasoning, proving problems that SMT-based techniques fail to solve.

ABSTRACT. Adding blocked clauses to a CNF formula can substantially speed SAT-solving up, both in theory and practice. In theory, the addition of blocked clauses can exponentially reduce the length of the shortest refutation for a formula. In practice, it has been recently shown that the runtime of CDCL solvers decreases significantly on certain instance families when blocked clauses are added as a preprocessing step. This fact is in contrast, but not contradiction, with Blocked-Clause Elimination (BCE) being known as a sometimes effective preprocessing step for over a decade, and suggests that the practical role of blocked clauses in SAT-solving might be richer than expected. In this paper we propose a theoretical study of the complexity of Blocked-Clause Addition (BCA) as a preprocessing step for SAT-solving, and in particular, consider the problem of adding the maximum number of blocked clauses of a given arity k to an input formula F. While BCE is a confluent process, meaning that the order in which blocked clauses are eliminated is irrelevant, this is not the case for BCA: adding a blocked clause to a formula might unblock a different clause that was previously blocked, and this order-sensitivity turns out to be a crucial obstacle for carrying out BCA efficiently as a preprocessing step. Our main result is that computing the maximum number of k-ary blocked clauses that can be added to an input formula F is NP-hard for every k >= 2.

ABSTRACT. Simulation is an important aspect of model checking, serving as an invaluable pre-processing step that can quickly generate a set of reachable states. This is evident in model checking tools at the Hardware Model Checking Competitions, where Btor2 is used to represent verification problems. Recently, Btor2MLIR was introduced as a novel format for representing safety and correctness constraints for hardware circuits. It provides an executable semantics for circuits represented in Btor2 by providing an equivalent program in LLVM-IR. One challenge in simulating Btor2 circuits is the use of persistent (i.e., immutable) arrays to represent memorys. Persistent arrays work well for symbolic reasoning in SMT but they require copy-on-write semantics when being simulated natively. We provide an algorithm for converting persistent arrays to transient (i.e., mutable) arrays with efficient native execution. This opens the door for rapid prototyping, dynamic verification techniques and random testing using established tool chains such as LibFuzzer and KLEE.

ABSTRACT. Most high-end automated theorem provers for first order logic (FOL) split available time between short runs of a large portfolio of search strategies. These runs are typically independent and can be parallelized to exploit all the available processor cores. We explore several avenues of re-using clauses generated by earlier runs and present experimental results of their usefulness or lack thereof.

ABSTRACT. This is part of an ongoing research project, with the aim of studying the connections between model-theoretic properties related to theory combination in Satisfiability Modulo Theories. In previous work, 7 properties were analyzed: convexity, stable infiniteness, smoothness, finite witnessibility, strong finite witnessibility, the finite model property, and stable finiteness.

The first two properties are needed for Nelson-Oppen combination, the third and fourth are related to polite combination, the third and fifth correspond to strong politeness, and the last two are related to the combination of shiny theories.

However, the remaining key property of shiny theories, namely, the ability to compute the cardinalities of minimal models, was not yet analyzed. In this paper we study this property.

ABSTRACT. Symbolic derivatives of extended regular expressions or regexes provide a mechanism for incremental unfolding of regexes into symbolic automata. The underlying representation is in form of so called transition regexes, that are particularly useful in the context of SMT for supporting lazy propagation of Boolean operations such as complement. Here we introduce symbolic derivatives of further operations on regexes, including fusion and lookaheads, that are currently not supported in the context of SMT but have been used in many application domains ranging from matching to temporal logic specifications. We argue that those operators could also be supported in the context of SMT and motivate why such direct support would be beneficial.

ABSTRACT. We introduce a notion of extensional metamodeling that can be used to extend knowledge representation languages, and show that this feature does not increase computational complexity of reasoning in many cases. We sketch the relation of our notion to various existing logics with metamodeling and to non-wellfounded sets, and discuss applications. We also comment on the usability of black-box reductions to develop reasoning algorithms for metamodeling.