A Decision Procedure for String to Code Point Conversion

code points, each of which can be represented as a natural number. We

present a decision procedure for a (concatenation-free) theory of strings that

includes length and a conversion function from strings to integer code points.

Furthermore, we show that many common string operations, such as conversions

between lowercase and uppercase, can be naturally encoded using this conversion

function. We implement our approach in the SMT solver CVC4, which contains a

state-of-the-art string subsolver, and show that the use of a native procedure

for code points significantly improves its performance with respect to other

state-of-the-art string solvers.

Validating Mathematical Structures

Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description)

designed for high performance, but to clearly demonstrate the core

concepts of a saturating theorem prover. The system is written in

extensively commented Python, explaining data structures,

algorithms, and many of the underlying theoretical concepts. The

prover implements binary resolution with factoring and optional

negative literal selection. Equality is handled by adding the basic

axioms of equality. PyRes uses the given-clause algorithm,

optionally controlled by weight- and age evaluations for clause

selection. The prover can read TPTP CNF/FOF input files and produces

TPTP/TSTP proof objects.

Evaluation shows, as expected, mediocre performance compared to

modern high-performance systems, with relatively better performance

for problems without equality. However, the system seems to be sound and

complete in practice.

The Resolution of Keller's Conjecture

Mechanised Modal Model Theory

The focus on models is novel: previous work in mechanisations of modal logic have centered on proof systems and applications in model-checking. We have formalised a number of fundamental results from the first two chapters of a standard textbook (Blackburn et al.). Among others, one important result, the Van Benthem characterisation theorem, characterises the connection between modal logic and first order logic. This latter captures the desired saturation property of ultraproduct models on countably incomplete ultrafilters.

A Knuth-Bendix-Like Ordering for Orienting Combinator Equations

A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (system description)

Quotients of Bounded Natural Functors

For example, inductive and coinductive datatypes can be built modularly from so-called bounded natural functors (BNFs), a class of particularly well-behaved type constructors.

Composition, fixpoints, and---under certain conditions---subtypes are known to preserve the BNF structure.

In this paper, we tackle the preservation question for quotients, the last important principle for introducing new types in HOL.

We identify sufficient conditions under which a quotient inherits the BNF structure from its underlying type.

We implement in the Isabelle proof assistant a command that automates the registration of a quotient type as a BNF by lifting the underlying type's BNF structure.

We demonstrate the command's usefulness through several case studies.

Soft subexponentials and multiplexing

ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)

Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper)

Verification of Closest Pair of Points Algorithms

Combined Covers and Beth Definability

Verified Approximation Algorithms

An SMT Theory of Fixed-Point Arithmetic

embedded systems. Existing work on the verification of fixed-point programs

relies on custom formalizations of fixed-point arithmetic, which makes it hard

to compare the described techniques or reuse the implementations. In this

paper, we address this issue by proposing and formalizing an SMT theory of

fixed-point arithmetic. We present an intuitive yet comprehensive syntax of the

fixed-point theory, and provide formal semantics for it based on rational

arithmetic. We also describe two decision procedures for this theory: one based

on the theory of bit-vectors and the other on the theory of reals. We implement

the two decision procedures, and evaluate our implementations using existing

mature SMT solvers on a benchmark suite we created. Finally, we perform a case

study of using the theory we propose to verify properties of quantized neural

networks.

Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages

not only crucial to lower the cognitive burden of manipulating complex

mathematical objects, but plays a critical role in developing reusable ab-

stractions in libraries. Most ITPs support such extensions in the form

of restrictive “syntax sugar” substitutions and other ad hoc mechanisms,

which are too rudimentary to support many desirable abstractions. As

a result, libraries are littered with unnecessary redundancy. Tactic lan-

guages in these systems are plagued by a seemingly unrelated issue: ac-

cidental name capture, which often produces unexpected and counterin-

tuitive behavior. We take ideas from the Scheme family of programming

languages and solve these two problems simultaneously by proposing a

novel hygienic macro system for ITPs. We further describe how our ap-

proach can be extended to cover type-directed macro expansion resulting

in a single, uniform system offering multiple abstraction levels that range

from supporting simplest syntax sugars to elaboration of formerly baked-

in syntax. We have implemented our new macro system and integrated

it into the upcoming version (v4) of the Lean theorem prover. Despite

its expressivity, the macro system is simple enough that it can easily be

integrated into other systems.

Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols

A Combinator-Based Superposition Calculus for Higher-Order Logic

A Polymorphic Vampire

Practical proof search for Coq by type inhabitation

For efficiency, our procedure is not complete for the Calculus of Inductive Constructions, but it is complete for a first-order fragment. Even in pure intuitionistic first-order logic, with large enough time limit our method outperforms Coq’s "firstorder" tactic, achieving a 29.5% success rate on the ILTP library of first-order intuitionistic problems.

Algebraically Closed Fields in Isabelle/HOL

A Lean tactic for normalising ring expressions with exponents (short paper)

The Face Lattice of Polyhedra

Deciding Simple Infinity Axiom Sets with one Binary Relation by Superpostulates

Formal Proof of the Group Law for Edwards Elliptic Curves

law for Edwards elliptic curves. The associative law is expressed as

a polynomial identity over the integers that is directly checked by

polynomial division. Unlike other proofs, no preliminaries such as

intersection numbers, Bezout's theorem, projective geometry,

divisors, or Riemann Roch are required. The proof of the group law

has been formalized in the Isabelle/HOL proof assistant.

Description Logics with Concrete Domains and General Concept Inclusions Revisited

Sequoia: a playground for logicians

properties due to the regularity of rules, proofs, and meta-property proofs

across logics. However, even simple proofs can be large, and writing them by

hand is often messy. Moreover, the combinatorial nature of the calculus makes it

easy for humans to make mistakes or miss cases. Sequoia aims to alleviate these

problems.

Sequoia is a web-based application for specifying sequent calculi and performing

basic reasoning about them. The goal is to be a user-friendly program, where

logicians can specify and "play" with their calculi. For that purpose, we

provide an intuitive interface where inference rules can be input in LaTeX and

are immediately rendered with the corresponding symbols. Users can then build

proof trees in a streamlined and minimal-effort way, in whichever calculus they

defined. In addition to that, we provide checks for some of the most important

meta-theoretical properties, such as weakening admissibility and identity

expansion, given that they proceed by the usual structural induction. In this

sense, the logician is only left with the tricky and most interesting cases of

each analysis.

Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL

Constructive Hybrid Games

adversarial dynamics. Game logic enables proving existence of

(perhaps noncomputable) winning strategies. We introduce

constructive differential game logic (CdGL) for hybrid games, where

proofs that a player can win the game correspond to computable

winning strategies. This is the logical foundation for synthesis of

correct control and monitoring code for safety-critical

cyber-physical systems. Our contributions include novel static and

dynamic semantics as well as results such as soundness and

consistency.

Verifying Faradžev-Read type Isomorph-Free Exhaustive Generation

objects with certain properties, that do not contain

isomorphs. Several efficient general schemes for this problem

exist. One is described independently by I. A. Faradžev and

R. C. Read and has since been applied to catalogue many different

combinatorial structures. We present an Isabelle/HOL verification of

this abstract scheme. To show its practicality, we instantiate it on

two concrete problems: enumerating digraphs and enumerating

union-closed families of sets. In the second example abstract

algorithm specification is refined to an implementation that can

quite efficiently enumerate all canonical union-closed families over

a six element universe (there is more than 100 million such

families).

The Imandra Automated Reasoning System

bridge the gap between decision procedures such as SMT, semi-automatic inductive

provers of the Boyer-Moore family like ACL2, and interactive proof assistants

for typed higher-order logics. Imandra's logic is computational, based on a pure

subset of OCaml in which all functions are terminating, with restrictions on

types and higher-order functions that allow conjectures to be translated into

multi-sorted first-order logic with theories, including arithmetic and

datatypes. Imandra has novel features supporting large-scale industrial

applications, including a seamless integration of bounded and unbounded

verification, first-class computable counterexamples, efficiently executable

models and a cloud-native architecture supporting live multiuser collaboration.

%

The core reasoning mechanisms of Imandra are

\begin{inparaenum}[(i)]

\item a semi-complete procedure for finding models of formulas in the logic

mentioned above, centered around the lazy expansion of recursive functions,

\item an inductive waterfall and simplifier which ``lifts'' many Boyer-Moore

ideas to our typed higher-order setting.

\end{inparaenum}

%

These mechanisms are tightly integrated and subject to many forms of user control.

Imandra's user interfaces include an interactive toplevel, Jupyter notebooks and

asynchronous document-based verification (in the spirit of Isabelle's Prover IDE)

with VS Code.

Subsumption Demodulation in First-Order Theorem Proving

we introduce a new inference rule, called subsumption demodulation, to improve

support for reasoning with conditional equalities in superposition-based

theorem proving. We show that subsumption demodulation is a simplification

rule that does not require radical changes to the underlying superposition

calculus. We implemented subsumption demodulation in the theorem prover

Vampire, by extending Vampire with a new clause index and adapting its

multi-literal matching component. Our experiments, using the TPTP and SMT-LIB

repositories, show that subsumption demodulation in Vampire can solve many new

problems that could so far not be solved by state-of-the-art reasoners.

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs

Using this approach, we complete the first proof-generating pipeline that goes automatically from high-level specifications to assembly code. In our main case study, the original specifications are phrased to resemble SQL-style queries, while the final assembly code does manual memory management, calls out to foreign data structures and functions, and is suitable to deploy on resource-constrained platforms. The pipeline runs entirely within the Coq proof assistant, leading to final, linked assembly code with overall full-functional-correctness proofs in separation logic.

N-PAT: A Nested Model-Checker (System Description)

Trakhtenbrot's Theorem in Coq

in the constructive setting of dependent type theory.

Employing synthetic accounts of enumerability and decidability,

we give a full classification of FSAT depending on

the first-order signature of non-logical symbols.

On the one hand,

our development focuses on Trakhtenbrot's theorem, stating

that FSAT is undecidable as soon as the signature contains an at least binary

relation symbol. Our proof proceeds by a many-one reduction chain

starting from the Post correspondence problem.

On the other hand, we establish the decidability of FSAT for monadic

first-order logic, i.e. where the signature only

contains at most unary function and relation symbols, as well as the enumerability

of FSAT for arbitrary

enumerable signatures.

All our results are mechanised in the framework of a growing Coq library of synthetic undecidability proofs.

Possible Models Computation and Revision - A Practical Approach

reasoning for estimating the current state of a system as it

evolves over time. The main motivation is situational awareness,

which requires to being able to understand and explain a system's

current state, at any time, and at a level that matters to the

user, even if only partial or incorrect information about the

external events leading to that state is available.

The paper proposes to represent such states as models of a

logical specification of the properties of interest and a given a

set of external timestamped events up to ``now''. The underlying

modeling language is a grounded in logic programming, and models

are computed in a bottom-up way. It adopts notions of

stratification, default negation and a possible model semantics

for its (disjunctive) program rules. In order to deal with

less-than-perfect event data, the modeling language features a

novel model revision operator that allows the programmer to

formulate conditions under which a model computation with a

corrected set of events should be attempted in an otherwise

inconsistent state.

Model computation and revision has a long history in the area of

logic programming. The novelty of our approach lies in the

specifics of the stratification employed, in terms of time and in

terms of whether a fact is an external event or derived, and in

the specifics of the model revision operator. Our approach

deliberately compromises on generality for the benefit of low

complexity and any-time reasoning capabilities as needed to

support situational awareness application well.

The paper provides the technical details of the approach. The

main theoretical results are soundness and completeness of the

proposed model computation algorithm. On the applied side, the

paper describes an implementation as a shallow embedding into the

Scala programming language by means of the Scala macro

mechanism. This is important in practice, as it gives the

programmer built-in access to a full-fledged programming language

and its associated libraries. The paper sketches the usefulness

of this feature and the model revision operator with a small

example for supply chain situational awareness.

Formalization of Forcing in Isabelle/ZF

HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics

How QBF Expansion Makes Strategy Extraction Hard

While expansion reasoning used in other QBF calculi can admit polynomial time strategy extraction, we find this is conditional on a property studied in proof complexity theory. We show that strategy extraction on expansion based systems can only happen when the underlying propositional calculus has the property of feasible interpolation.

Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)

Make E Smart Again

In this work we strip E to the barebones: we replace the KBO6 term ordering with an identity relation as the minimal possible ordering, disable literal selection, and replace evolved strategies with the simple combination of the clause weight and FIFO (first in first out) evaluatino functions.

We experimentally demonstrate that ENIGMA can learn to guide E as well as the smart, evolved strategies even without these staple automated theorem prover functionalities.

To do this we need to experiment with XGBoost's meta-parameters over a dozen loops.

Automatically Proving and Disproving Feasibility Conditions

mu-term: Verify Termination Properties Automatically (System Description)

Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates

Constrained Horn Clauses (CHCs) with Algebraic Data Types (ADTs),

such as lists and trees.

We propose a technique that transforms sets of CHCs with

ADTs into CHCs where predicates are defined over basic types, such as

integers and booleans, only.

We show that if the set of transformed clauses is satisfiable,

then so is the set of the original clauses.

Thus, our technique avoids the explicit use of inductive proof rules

during satisfiability proofs.

The main extension over previous techniques is that the transformation

automatically generates new predicates corresponding to the lemmata

that are often needed by inductive proofs.

By an experimental evaluation,

we show that our approach is competitive with respect to techniques that

extend CHC solving with induction.

Prolog Technology Reinforcement Learning Prover

SGGS Decision Procedures

A Comprehensive Framework for Saturation Theorem Proving

A Fast Verified Liveness Analysis in SSA form

optimizations such as deadcode elimination. The SSA form is a popular compiler

intermediate language allowing for simple and fast optimizations. Boissinot et

al. designed a fast liveness analysis by combining

the specific properties of SSA with graph-theoretic ideas such as

depth-first search and dominance. We formalize their approach in the Coq proof

assistant, inside the CompCertSSA verified C compiler. We also compare

experimentally this approach on CompCert's benchmarks with respect to the

classic dataflow-based liveness analysis, and observe performance gains.

Efficient Verified Implementation of Introsort and Pdqsort

both, their correctness and efficiency is crucial for many applications.

As generic sorting algorithm, the GNU C++ Standard Library implements the Introsort algorithm,

a combination of quicksort, heapsort, and insertion sort. The Boost C++ library implements Pdqsort,

an extension of Introsort that achieves linear runtime on inputs with certain patterns.

We verify Introsort and Pdqsort in the Isabelle LLVM verification framework,

including most of the optimizations from the GNU and Boost implementations.

On an extensive benchmark set, our verified algorithms perform on par with the originals.

A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic

Covered Clauses Are Not Propagation Redundant

Integrating Induction and Coinduction via Closure Operators and Proof Cycles

Politeness for The Theory of Algebraic Datatypes

automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest

stable version, the SMT-LIB standard defines a theory of algebraic datatypes,

which is currently supported by several mainstream SMT solvers.

In this paper, we study this particular theory of datatypes and prove that it is strongly polite,

showing also how it can be combined with other arbitrary disjoint theories using polite combination.

Our results cover both inductive and finite datatypes, as well as their union.

The combination method uses a new, simple, and natural notion of additivity,

that enables deducing strong politeness from (weak) politeness.

Implementing superposition in iProver

We have developed a flexible simplification setup that subsumes and generalises common architectures such as Discount or Otter. This also includes the concept of "immediate simplification", wherein newly derived clauses are more aggressively simplified among themselves, which can make the given clause redundant and thus its children discarded, and the concept of "light normalisation", wherein ground unit equations are stored in an interreduced TRS which is then used to simplify new clauses. We have also added support for associative-commutative theories (AC), namely by deletion of AC-joinable clauses, semantic detection of AC axioms, and preprocessing normalisation.

Layered Clause Selection for Theory Reasoning (short paper)

Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis

with a given set of axioms that when added to these axioms

suffices to entail a goal.

We propose an approach for solving the abduction problem that is based on

syntax-guided enumeration in the Satisfiability Modulo Theories (SMT) solver CVC4.

For scalability, we use a novel algorithm that incrementally constructs

a solution in disjunctive normal form that is built from enumerated predicates.

The algorithm can be configured to generate progressively weaker

and simpler solutions over the course of a run of the algorithm.

Our approach is fully general and can be applied over any background logic

that is handled by the underlying SMT solver in our approach.

Our experiments show our approach compares favorably with other tools

for abductive reasoning.

Logic-Independent Proof Search in Logical Frameworks (short paper)

An important question is to what extent the latter can include a logic-independent automated theorem prover.

On the one hand, many theorem proving innovations can be generalized to much larger classes of logics than they were originally developed for.

On the other hand, most practically competitive provers critically use logic-specific optimizations.

Indeed, logical framework-induced fully logic-independent proof support is generally limited to proof checking and simple search.

In order to investigate this question more deeply, we build a suite of highly modular definitions of a variety of logics in a logical framework and generate Prolog-based theorem provers for each of them.

We emphasize generality of the method and try to avoid taking any logic-specific knowledge into account.

Our generated provers support natural deduction proof search, including back-chaining, as well as tableau provers and model generators.

Even though these efforts have only just started, we are already able to use the latter in a system for natural language understanding that combines grammatical with semantic processing.

Formalizing functional analysis structures in dependent type theory

combine linear algebra with concepts related to limits, like topology

and norms, in dependent type theory. This hierarchy is the backbone of

a new library of formalized classical analysis, for the Coq proof

assistant. It extends the Mathematical Components library, geared

towards algebra, with topics in analysis. This marriage arouses issues

of a more general nature, related to the inheritance of poorer

structures from richer ones. We present and discuss a solution, coined

forgetful inheritance, based on packed classes and unification

hints.

NP Reasoning in the Monotone mu-Calculus

Deep Generation of Coq Lemma Names Using Elaborated Terms

Solving bit-vectors with MCSAT: explanations from bits and pieces

in the MCSAT framework. MCSAT is an alternative to CDCL(T) for

SMT solving and can be seen as an extension of CDCL to other

domains than the Booleans.

To apply MCSAT to bit-vectors, we use Binary Decision Diagrams

to record and update the set of feasible values for a bit-vector

variable and we develop specialized conflict-explanation mechanisms.

We present two methods based on interpolation that generate word-level

explanations. These methods are applicable when the conflict is

restricted to two fragments of bit-vector arithmetic. We use

aggressive normalization to shoehorn as many conflicts as

possible into these fragments. When that fails, we resort to

bit-blasting to generate explanations.

The approach is implemented in the Yices 2 SMT solver. We present

experimental results.

Monadic Decomposition in Integer Linear Arithmetic

(i.e. input formula is quantifier-free), and found various interesting applications including string analysis. Despite these, checking monadic decomposability is undecidable in

general. Decidability for certain theories is known (e.g. Presburger

Arithmetic, Tarski's Real Closed Field), but there are very few results

regarding their computational complexity.

In this paper, we study monadic decomposability of integer linear arithmetic

in the setting of SMT.

We show that this decision problem is coNP-complete and,

when monadically decomposable, a formula admits a decomposition of

exponential size in the worst case.

We provide a new application of our results to

string constraint solving with length constraints.

We then extend our results to variadic decomposability,

where predicates could admit multiple free variables (in contrast to monadic

decomposability). We provide an

application to quantifier elimination in integer linear arithmetic where

the variables in a block of quantifiers, if independent,

could be eliminated with an exponential (instead of the standard

double exponential) blow-up.