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 PRON- TOQA benchmark. We show how accuracy can be improved with a neuro-symbolic ar- chitecture 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. How- ever, 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 er- ror 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 contribu- tion. We demonstrate that this approach reduces semantic errors significantly and further increases the accurracy of LLM logical reasoning.
Continuous double auctions are commonly used to match orders at currency, stock, and commodities exchanges. A verified implementation of continuous double auctions is a useful tool for market regulators as they give rise to automated checkers that are guaranteed to detect errors in the trade logs of an existing exchange if they contain trades that violate the matching rules. We provide an efficient and formally verified implementation of continuous double auctions that takes O(nlogn) time to match n orders. This improves an earlier O(n2) verified implementation. We also prove a matching Ω(nlogn) lower bound on the running time for continuous double auctions. Our new implementation takes only a couple of minutes to run on ten million randomly generated orders as opposed to a few days taken by the earlier implementation. Our new implementation gives rise to an efficient automatic checker. We use the Coq proof assistant for verifying our implementation and extracting a verified OCaml program. While using Coq’s standard library implementation of red-black trees to obtain our improvement, we observed that its specification has serious gaps, which we fill in this work; this might be of independent interest.
Inductive proofs can be represented as a proof schemata, i.e. as a parameterized se- quence 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 ex- pressivity of proof schemata as defined in [10]. We show that proof schemata can simulate primitive recursive arithmetic as defined in [12]. Future research will focus on an extension of the simulation to primitive recursive arithmetic using quantification as defined in [7]. The translation of proofs in arithmetic to proof schemata can be considered as a crucial step in the analysis of inductive proofs.
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.
Choices in the semantics and the signature of a theory are integral in determining how the theory is used and how challenging 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 one 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 sequences as a contribution to the discussion regarding its standardization.
We introduce and discuss a term-rewriting technique to convert numbers from any nu- meric base to any other one without explicitly 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 implemen- tation and benchmarks in the Dedukti type checker. This work extends and generalizes a previous work by Delahaye, published in a vulgarization scientific review.
LPTP (Logic Program Theorem Prover) is an interactive natural-deduction-based the- orem 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. Sta ̈rk. It is written in ISO-Prolog and comes with an Emacs user-interface.From a theoretical point of view, in his publications about LPTP, Sta ̈rk 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 auto- mated 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 veri- fication. 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.
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 or postcedents in the sequent: all occurrences of the corresponding variable in any of the other formulae are replaced by the appropriate 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 based 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.
We demonstrate utility of generic automated reasoning (AR) methods in the com- putational 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 soft- ware 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.
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 MSn(w∗) of trivial group presentations for n = 3, 4, 5, 6, 7, 8 (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 MSn(w∗), n ≥ 3. This is an extended and updated version of the abstract [11] presented at AITP 2023 conference.
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.
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 Theorema 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.
We introduce a notion of extensional metamodeling that can be used to extend knowl- edge 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.
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.
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 op- erations. We support reasoning 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. Furthermore, we add the ability to reason about tables with null values by introducing a theory of nullable sorts based on an extension of the theory of algebraic datatypes. We implemented solvers for these theories in the SMT solver cvc5 and evaluated them on a set of benchmarks derived from public sets of SQL equivalence problems.
Group polarization, the phenomenon where individuals become more extreme after in- teracting, has been gaining attention, especially with the rise of social media shaping peo- ple’s opinions. Recent interest has emerged in formal reasoning about group polarization using logical systems. In this work we consider the modal logic PNL that captures the no- tion of agents agreeing or disagreeing on a given topic. Our contribution involves enhancing PNL with advanced formal reasoning techniques, instead of relying on axiomatic systems for analyzing group polarization. To achieve this, we introduce a semantic game tailored for (hybrid) extensions of PNL. This game fosters dynamic reasoning about concrete net- work models, aligning with our goal of strengthening PNL’s effectiveness in studying group polarization. We show how this semantic game leads to a provability game by systemically exploring the truth in all models. This leads to the first cut-free sequent systems for some variants of PNL. Using polarization of formulas, the proposed calculi can be modularly adapted to consider different frame properties of the underlying model.
This is a part of an ongoing research project, with the aim of finding the connections between properties related to theory combination in Satisfiability Modulo Theories. In pre- vious work, 7 properties were analyzed: convexity, stable infiniteness, smoothness, finite witnessability, strong finite witnessability, the finite model property, and stable finiteness. The first two properties are related to Nelson-Oppen combination, the third and fourth to polite combination, the fifth to strong politeness, and the last two to shininess. However, the remaining key property of shiny theories, namely, the ability to compute the cardinal- ities of minimal models, was not yet analyzed. In this paper we study this property and its connection to the others.
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 the syntactic restrictions that guarantee that the associated languages of words resp. trees are regular - and hence, MSO-definable - are known, the situation is far 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.
In this paper we present the proof that there is no elementary translation from cut- free derivations in the sequent calculus variant of the epsilon calculus to LK-proofs with bounded cut-complexity. This is a partial answer to a question by Toshiyasu Arai. Fur- thermore, we show that the intuitionistic format of the sequent calculus variant of the epsilon calculus is not sound for intuitionistic logic, due to the presence of all classical quantifier-shift rules.
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.
