IJCAR 2020 Accepted Papers with Abstracts

Abstract: In text-encoding standards such as Unicode, text strings are sequences of
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.

Abstract: With regard to formalizing mathematics in proof assistants, the hierarchy of mathematical structure that allows for the sharing of notations and theories, and makes subtyping of structures implicit, is a key ingredient of infrastructure to support the users. The packed classes method is a generic design pattern to define and combine mathematical structures in a dependent type theory with records. The Coq proof assistant has mechanisms to enable automated structure inference and subtyping with packed classes; that is, implicit coercions and canonical structures. In this paper, we describe some invariants of hierarchies that ensure the modularity of reasoning and the predictability of inference with packed classes, propose checking tools for those invariants, and show that our tools significantly improve the development process of Mathematical Components, a formalized mathematics library for Coq.

Abstract: PyRes is a complete theorem prover for first-order logic. It is not
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.

Abstract: We consider three graphs, G_{7,3}, G_{7,4}, and G_{7,6}, related to Keller's conjecture in dimension 7. The conjecture is false for this dimension if and only if at least one of the graphs contains a clique of size 2^7 = 128. We present an automated method to solve this conjecture by encoding the existence of such a clique as a propositional formula. We apply satisfiability solving combined with symmetry-breaking techniques to determine that no such clique exists. This result implies that every unit cube tiling of R^7 contains a facesharing pair of cubes. Since a faceshare-free unit cube tiling of R^8$exists (which we also verify), this completely resolves Keller's conjecture.

Abstract: In this paper, we discuss the mechanisation of some fundamental propositional 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.

Abstract: We extend the graceful higher-order basic Knuth-Bendix order (KBO) of Blanchette et al. to an ordering that orients combinator equations left-to-right. The resultant ordering is highly suited to parameterising the first-order superposition calculus when dealing with the theory of higher-order logic, as it prevents inferences between the combinator axioms. We prove a number of desirable properties about the ordering including it having the subterm property for ground terms, being transitive and being well-founded. The ordering fails to be a reduction ordering as it lacks compatibility with certain contexts. We provide an intuition of why this need not be an obstacle when using it to parameterise superposition.

Abstract: SUMOjEdit is a programmer’s text editor for the SUO-KIF language and SUMO theory. Modern procedural programming is done in a text editor with tool support. Development of ontologies and taxonomies has often been done in graphical editors, leading many developers to employ only logics of very limited expressiveness that can be manipulated visually. Developers in the theorem proving community typically work in text editors but without the same degree of tool support that most programmers rely on. Beginners working with SUMO make some very predictable errors in syntax, logical formulation, and use of the library of theories. Many of these errors can be flagged during editing, resulting in reduced time to become a productive developer. An editor designed for working with SUMO has the potential to aid beginners and experienced SUMO developers.

Abstract: The functorial structure of type constructors is the foundation for many definition and proof principles in higher-order logic (HOL).
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.

Abstract: Linear logic and its refinements have been used as a specification language for a number of deductive systems. This has been accomplished by carefully studying the structural restrictions of linear logic modalities. Examples of such refinements include subexponentials, light linear logic, and soft linear logic. We bring together these refinements of linear logic in a non-commutative setting. We introduce a non-commutative substructural system with subexponential modalities controlled by a minimalistic set of rules. Namely, we disallow the contraction and weakening rules for the exponential modality and introduce two primitive subexponentials. One of the subexponentials allows the multiplexing rule in the style of soft linear logic and light linear logic. The second subexponential provides the exchange rule. For this system, we construct a sequent calculus, establish cut elimination, and also provide a complete focused proof system. We illustrate the expressive power of this system by simulating Turing computations and categorial grammar parsing for compound sentences. Using the former, we prove an undecidability result. The new system employs Lambek's non-emptiness restriction, which is incompatible with the standard (sub)exponential setting. Lambek's restriction is crucial for applications in linguistics: without this restriction, categorial grammars incorrectly mark some ungrammatical phrases as being correct.

Abstract: We describe an implementation of gradient boosted and neural guidance of saturation-style automated theorem provers that does not depend on consistent symbol names across problems. For the gradient-boosted guidance, we manually create abstracted features by considering arity-based encodings of formulas. For the neural guidance, we use symbol-independent graph neural networks and their embedding of the terms and clauses. The two methods are efficiently implemented in the E prover and its ENIGMA learning-guided framework and evaluated on the MPTP large-theory benchmark. Both methods are shown to achieve comparable real-time performance to state-of-the-art symbol-based methods.

Abstract: Hybrid logic is modal logic enriched with names for worlds. We formalize soundness and completeness proofs for a Seligman-style tableau system for hybrid logic in the proof assistant Isabelle/HOL. The formalization shows how to lift certain rule restrictions, thereby simplifying the original un-formalized proof. Moreover, the completeness proof we formalize is synthetic which suggests we can extend this work to prove a wider range of results about hybrid logic.

Abstract: We verify two related divide-and-conquer algorithms solving one of the fundamental problems in Computational Geometry, the Closest Pair of Points problem. Using the interactive theorem prover Isabelle/HOL, we prove functional correctness and the optimal running time of O(n log n) of the algorithms. We generate executable code which is empirically competitive with handwritten reference implementations.

Abstract: Uniform interpolants were largely studied in non-classical propositional logics since the nineties, and their connection to model completeness was pointed out in the literature. A successive parallel research line inside the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. In this paper, we investigate cover transfer to theory combinations in the disjoint signatures case. We prove that, for convex theories, cover algorithms can be transferred to theory combinations under the same hypothesis needed to transfer quantifier-free interpolation (i.e., the equality interpolating property, aka strong amalgamation property). The key feature of our algorithm relies on the extensive usage of the Beth definability property for primitive fragments to convert implicitly defined variables into their explicitly defining terms. In the non-convex case, we show by a counterexample that cover may not exist in the combined theories.

Abstract: We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, load balancing, and bin packing. In the process we uncover incompletenesses in existing proofs and improve the approximation ratio in one case.

Abstract: Fixed-point arithmetic is a popular alternative to floating-point arithmetic on
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.

Abstract: In interactive theorem provers (ITPs), extensible syntax is
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.

Abstract: The word problem for a finite set of ground identities is known to be decidable in polynomial time using congruence closure, and this is also the case if some of the function symbols are assumed to be commutative. We show that decidability in P is preserved if we add the assumption that certain function symbols f are extensional in the sense that f(s1,...,sn) = f(t1,...,t) implies s1 = t1,...,sn = tn. In addition, we investigate a variant of extensionality that is more appropriate for commutative function symbols, but which raises the complexity of the word problem to coNP.

Abstract: We present a refutationally complete superposition calculus for a version of higher-order logic (HOL) based on the combinatory calculus. We also introduce a novel method of dealing with extensionality. The calculus was implemented in the Vampire theorem prover and we test its performance against other leading higher-order provers. The results suggests that the method is competitive.

Abstract: We have modified the Vampire theorem prover to support rank-1 polymorphism. In this paper we discuss the changes required to enable this and compare the performance of polymorphic Vampire against other polymorphic provers. We also compare its performance on monomorphic problems against standard Vampire. Finally, we discuss how polymorphism can be used to support theory reasoning and present results related to this.

Abstract: We present a practical proof search procedure for Coq based on a direct search for type inhabitants in an appropriate normal form. An implementation in a Coq plugin is available. It significantly outperforms the automation natively available in Coq, proving in 30s, with no ATP input, 40.9% of 4494 theorems from a collection of Coq libraries and 17.1% of CompCert. As a reconstruction backend for CoqHammer, the procedure achieves reconstruction success rates in the range 87-97%.

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.

Abstract: That every field admits an algebraically closed extension is a fundamental mathematical theorem. Despite its central importance, this result has never before been formalised in a proof assistant. We fill this gap by documenting its formalisation in Isabelle/HOL, describing the difficulties that impeded this development and their solutions.

Abstract: This paper describes the design of the normalising tactic ring_exp for the Lean prover. This tactic improves on existing tactics by extending commutative rings with a binary exponent operator. An inductive family of types represents the normal form, enforcing various invariants. The design can also be extended with more operators.

Abstract: Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library providing the basic constructions and operations over polyhedra, including projections, convex hulls and images under linear maps. Moreover, we design a special mechanism which automatically introduces an appropriate representation of a polyhedron or a face, depending on the context of the proof. We demonstrate the usability of this approach by establishing some of the most important combinatorial properties of faces, namely that they constitute a family of graded atomistic and coatomistic lattices closed under sublattices.

Abstract: Modern logic engines widely fail to decide axiom sets that are only satisfiable in an infinite domain. This paper specifies a method to decide an infinite number of infinity axiom sets by strong infinity axiom sets (superpostulates). Any formula that is derivable from satisfiable superpostulates is also satisfiable. Starting from known infinity axioms, a complete infinity axiom set for pure first-order logic with only one binary relation (FOL$_{R}$) is specified. Based on complete theories, rules are defined to generate a system of infinity superpostulates based on a complete infinity axiom set. We generated a database with 1040 infinity superpostulates by running our algorithm. The paper ends with a discussion of the possibility of extending the method of specifying infinity superpostulates for FOL$_{R}$.

Abstract: This article gives an elementary computational proof of the group
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.

Abstract: Concrete domains have been introduced in the area of Description Logic to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts. Unfortunately, in the presence of general concept inclusions (GCIs), which are supported by all modern DL systems, adding concrete domains may easily lead to undecidability. One contribution of this paper is to strengthen the existing undecidability results further by showing that concrete domains even weaker than the ones considered in the previous proofs may cause undecidability. To regain decidability in the presence of GCIs, quite strong restrictions, in sum called omega-admissiblity, need to be imposed on the concrete domain. On the one hand, we generalize the notion of omega-admissiblity from concrete domains with only binary predicates to concrete domains with predicates of arbitrary arity. On the other hand, we relate omega-admissiblity to well-known notions from model theory. In particular, we show that finitely bounded, homogeneous structures yield omega-admissible concrete domains. This allows us to show omega-admissibility of concrete domains using existing results from model theory.

Abstract: Sequent calculus is a pervasive technique for studying logics and their
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.

Abstract: We prove Chen and Grätzer's construction theorem for Stone algebras in Isabelle/HOL. The development requires extensive reasoning about algebraic structures in addition to reasoning in algebraic structures. We present an approach for this using classes and locales with implicit carriers. This involves using function liftings to implement some aspects of dependent types and using embeddings of algebras to inherit theorems. We also formalise a theory of filters based on partial orders.

Abstract: Hybrid games are models which combine discrete, continuous, and
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.

Abstract: Many applications require generating catalogues of combinatorial
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).

Abstract: We describe Imandra, a modern computational logic theorem prover designed to
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.

Abstract: Motivated by applications of first-order theorem proving to software analysis,
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.

Abstract: We present an original approach to sound program extraction in a proof assistant, using syntax-driven automation to derive correct-by-construction imperative programs from nondeterministic functional source code. Our approach does not require committing to a single inflexible compilation strategy and instead makes it straightforward to create domain-specific code translators. In addition to a small set of core definitions, our framework is a large, user-extensible collection of compilation rules each phrased to handle specific language constructs, code patterns, or data manipulations. By mixing and matching these pieces of logic, users can easily tailor extraction to their own domains and programs, getting maximum performance and ensuring correctness of the resulting assembly code.

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.

Abstract: N-PAT is a new model-checking tool that supports the verification of nested-models -- i.e. models whose behavior depends on the results of verification tasks. In this paper, we describe its operation and discuss mechanisms that are tailored to the efficient verification of nested-models. Further, we motivate the advantages of N-PAT over traditional model-checking tools through a network security case study.

Abstract: We study finite first-order satisfiability (FSAT)
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.

Abstract: This paper is concerned with logic-based modeling and automated
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.

Abstract: We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC. In doing so, we remodularized Paulson's ZF-Constructibility library.

Abstract: We present HYPNO (HYpersequent Prover for NOn-normal modal logics), a Prolog-based theorem prover and countermodel generator for non-normal modal logics. HYPNO implements some hypersequent calculi recently introduced for the basic system E and its extensions with axioms M, N, and C. It is inspired by the methodology of LeanTAP, so that it does not make use of any ad-hoc control mechanism. Given a formula, HYPNO provides either a proof in the calculus or a countermodel, directly built from an open saturated branch. Preliminary experimental results show that the performances of HYPNO are very promising with respect to other theorem provers for the same class of logics.

Abstract: In this paper we show that the QBF proof checking format QRAT (Quantified Resolution Asymmetric Tautologies) by Heule, Biere and Seidl cannot have polynomial time strategy extraction unless P=PSPACE. In our proof, the crucial property that makes strategy extraction PSPACE-hard for this proof format is universal expansion, even expansion on a single variable.

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.

Abstract: We present a simple Prolog prover for intuitionistic modal logics based on nested sequent proof systems. We have implemented single-conclusion (Genzten-style) nested sequent systems and multi-conclusion nested sequent systems (Maehara-style) for all logics in the intuitionistic modal IS5-cube. While the single-conclusion system are better investigated and have an internal cut-elimination, the multi-conclusion systems can provide a counter model in case the proof search fails. To our knowledge this is the first automated theorem prover for intuitionistic modal logics. For wider usability of our system, we also implemented all classical normal modal logics in the S5-cube.

Abstract: In this work in progress we demonstrate a new use-case for the ENIGMA system. The ENIGMA system using the XGBoost implementation of gradient boosted decision trees has shown high capability to learn to guide the E theorem prover's inferences in real time.

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.

Abstract: Given a Conditional Term Rewriting System (CTRS) R and terms s and t, the reachability condition s ->* t is called feasible if there is a substitution σ such that σ(s) ->*_R σ(t) holds; otherwise, it is infeasible. Checking infeasibility of (sequences of) reachability conditions is important in the analysis of computational properties of CTRSs like confluence or operational termination. In this paper, we generalize this notion of feasibility to enable the use of other relations (e.g., subterm |>, context-sensitive rewriting \->, etc.) defined by first-order theories, so that more general properties can be investigated. We introduce a framework for proving feasibility/infeasibility, and a new tool, infChecker, which implements it.

Abstract: We report on the new version of mu-term, a tool for proving termination properties of variants of rewrite systems, including conditional, context-sensitive, equational, and order-sorted rewrite systems.

Abstract: We address the problem of proving the satisfiability of
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.

Abstract: We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte Carlo Tree Search as done in the rlCoP system. Other components include a Python interface between plCoP and machine learners, and an external proof checker that verifies the validity of the plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) the learned guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We show that the code size compares favorably to rlCoP and argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released.

Abstract: SGGS (Semantically-Guided Goal-Sensitive reasoning) is a conflict-driven first-order theorem-proving method which is refutationally complete and model complete in the limit. These features make it attractive as a basis for decision procedures. In this paper we show that SGGS decides the stratified fragment which generalizes EPR, the PVD fragment, and a new fragment that we dub restrained. The new class has the small model property, as the size of SGGS-generated models can be upper-bounded, and is also decided by hyperresolution and ordered resolution. We report on experiments with a termination tool implementing a restrainedness test, and with an SGGS prototype named Koala.

Abstract: We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It permits us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of, e.g., an Otter or DISCOUNT loop prover implementing the calculus. Our framework is mechanized in Isabelle/HOL.

Abstract: Liveness analysis is a standard compiler analysis, enabling several
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.

Abstract: Sorting algorithms are an important part of most standard libraries, and
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.

Abstract: Runtime monitors for rich specification languages are sophisticated algorithms, especially when they are heavily optimized. To gain trust in them and safely explore the space of possible optimizations, it is important to verify the monitors themselves. We describe the development and correctness proof in Isabelle/HOL of a monitor for metric first-order dynamic logic. This monitor significantly extends previous work on formally verified monitors by supporting aggregations, regular expressions (the dynamic part), and optimizations including multi-way joins adopted from databases and a new sliding window algorithm.

Abstract: Propositional proof systems based on recently-developed redundancy properties admit short refutations for many formulas traditionally considered hard. Redundancy properties are also used by procedures which simplify formulas in conjunctive normal form by removing redundant clauses. Revisiting the covered clause elimination procedure, we prove the correctness of an explicit algorithm for identifying covered clauses, as it has previously only been implicitly described. While other elimination procedures produce redundancy witnesses for compactly reconstructing solutions to the original formula, we prove that witnesses for covered clauses are hard to compute. Further, we show that not all covered clauses are propagation redundant, the most general, polynomially-verifiable standard redundancy property. Finally, we close a gap in the literature by demonstrating the complexity of clause redundancy itself.

Abstract: Coinductive reasoning about infinitary data structures has many applications in computer science. Nonetheless developing natural proof systems (especially ones amenable to automation) for reasoning about coinductive data remains a challenge. This paper presents a minimal, generic formal framework that uniformly captures applicable (i.e. finitary) forms of inductive and coinductive reasoning in an intuitive manner. The logic extends transitive closure logic, a general purpose logic for inductive reasoning based on the transitive closure operator, with a dual 'co-closure' operator that similarly captures applicable coinductive reasoning in a natural, effective manner. We develop a sound and complete non-well-founded proof system for the extended logic, whose cyclic subsystem provides the basis for an effective system for automated inductive and coinductive reasoning. To demonstrate the adequacy of the framework we show that it captures the canonical coinductive datatype: streams.

Abstract: Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in
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.

Abstract: iProver is a saturation theorem prover for first-order logic with equality, which is originally based on an instantiation calculus, Inst-Gen. In this paper we describe an extension of iProver with the superposition calculus.
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.

Abstract: Explicit theory axioms are added by a saturation-based theorem prover as one of the techniques for supporting theory reasoning. While simple and effective, adding theory axioms can also pollute the search space with many irrelevant consequences. As a result, the prover often gets lost in parts of the search space where the chance to find a proof is low. In this paper we describe a new strategy for controlling the amount of reasoning with explicit theory axioms. The strategy refines a recently proposed two-layer-queue clause selection and combines it with a heuristical measure of the amount of theory reasoning in the derivation of a clause. We implemented the new strategy in the automatic theorem prover Vampire and present an evaluation showing that our work dramatically improves the state-of-the-art clause-selection strategy in the presence of theory axioms.

Abstract: The abduction problem asks whether there exists a predicate that is consistent
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.

Abstract: Logical frameworks enable prototyping and analyzing logical systems as well as developing logic-independent implementations.
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.

Abstract: This paper discusses the design of a hierarchy of structures which
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.

Abstract: Satisfiability checking for monotone modal logic is known to be (only) NP-complete. We show that this remains true when the logic is extended with aconjunctive and alternation-free fixpoint operators as well as the universal modality; the resulting logic -- the aconjunctive alternation-free fragment of the monotone mu-calculus with the universal modality -- contains both concurrent propositional dynamic logic (CPDL) and the alternation-free fragment of game logic as fragments. We obtain our result from a characterization of satisfiability by means of Büchi games with polynomially many Eloise nodes.

Abstract: Coding conventions for naming, spacing, and other essentially stylistic properties are necessary for developers to effectively understand, review, and modify source code in large software projects. Consistent conventions in verification projects based on proof assistants, such as Coq, increase in importance as projects grow in size and scope. While conventions can be documented and enforced manually at high cost, emerging approaches automatically learn and suggest idiomatic names in Java-like languages by applying statistical language models on large code corpora. However, due to its powerful language extension facilities and fusion of type checking and computation, Coq is a challenging target for automated learning techniques. We present novel generation models for learning and suggesting lemma names for Coq projects. Our models, based on multi-input neural networks, are the first to leverage syntactic and semantic information from Coq’s lexer (tokens in lemma statements), parser (syntax trees), and kernel (elaborated terms); the key insight is that learning from elaborated terms can substantially boost model performance. We implemented our models in a toolchain, dubbed Roosterize, and applied it to learn from a large corpus of code derived from the Mathematical Components family of projects, known for its stringent coding conventions. Our results show that Roosterize substantially outperforms baselines for suggesting lemma names, highlighting the importance of using multi-input models and elaborated terms.

Abstract: We develop a treatment of the theory of fixed-sized bit-vectors
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.

Abstract: Monadic decomposability is a notion of variable independence, which asks whether a given formula in a first-order theory is expressible as a boolean combination of monadic predicates in the theory. Recently, Veanes et al. showed the usefulness of monadic decomposability in the context of SMT
(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.