ABSTRACT. In this talk, I will focus on one of the most fundamental problems in automated reasoning: functional synthesis, which seeks to synthesize a system from a given relational specification. The synthesis problem is as old as propositional logic, tracing its origins to Boole's seminal work in the 1850's. Despite decades of work, scalability remains the fundamental challenge in functional synthesis. I will discuss a new data-driven approach, Manthan, that combines the power of machine learning with symbolic reasoning to achieve dramatic improvements in scalability.  In particular, Manthan views functional synthesis as a classification problem, relies on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification. The significant performance improvements call for interesting future work at the intersection of machine learning and symbolic reasoning.

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. 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. 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. 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. 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. 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. 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. 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. 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 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. 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. 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 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. 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. 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.