Non-well-founded Deduction for Induction and Coinduction

ABSTRACT. Induction and coinduction are both used extensively within mathematics and computer science. Algebraic formulations of these principles make the duality between them apparent, but do not account well for the way they are commonly used in deduction. Generally, the formalization of these reasoning methods employs inference rules that express a general explicit (co)induction scheme. Non-well-founded proof theory provides an alternative, more robust approach for formalizing implicit (co)inductive reasoning. This approach has been extremely successful in recent years in supporting implicit inductive reasoning, but is not as well-developed in the context of coinductive reasoning. This talk reviews the general method of non-well-founded proofs, and puts forward a concrete natural framework for (co)inductive reasoning, based on (co)closure operators, that offers a concise framework in which inductive and coinductive reasoning are captured as we intuitively understand and use them. Through this framework we demonstrate the enormous potential of non-well-founded deduction, both in the foundational theoretical exploration of (co)inductive reasoning and in the provision of proof support for (co)inductive reasoning within (semi-)automated proof tools.

Politeness and Stable Infiniteness: Stronger Together

ABSTRACT. We make two contributions to the study of polite combination
in satisfiability modulo theories.
The first contribution is a separation between
politeness and strong politeness, by
presenting a polite theory that is not strongly polite.
This result shows that proving strong politeness
(which is often harder than proving politeness) is sometimes necessary.
The second contribution is an optimization to the polite combination method,
obtained by borrowing from the Nelson-Oppen method.
In its non-deterministic form, the Nelson-Oppen method
is based on guessing arrangements over shared variables.
In contrast,
polite combination requires an arrangement over all
variables of the shared sort (not just the shared variables).
We show that when using polite combination, if the other theory is stably infinite with respect to
a shared sort, only
the shared variables of that sort need be considered in arrangements, as in the Nelson-Oppen method.
Reasoning about arrangements of variables is exponential in the worst case,
so reducing the number of variables that are considered
has the potential to improve performance significantly.
We show preliminary evidence for this in practice by demonstrating a speed-up on
a smart contract verification benchmark.

ABSTRACT. Unlike other methods for theorem proving modulo with constrained clauses, equational theorem proving modulo with constrained clauses along with its simplification techniques has not been well studied. We introduce a basic paramodulation calculus modulo equational theories E (satisfying certain properties of E) and present a new framework for equational theorem proving modulo E with constrained clauses. We propose an inference rule called Generalized E-Parallel for constrained clauses, which makes our inference system completely basic, meaning that we do not need to allow any paramodulation in the constraint part of a constrained clause for refutational completeness. We present a saturation procedure for constrained clauses based on relative reducibility and show that our inference system including our contraction rules is refutationally complete.

ABSTRACT. We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed binary--ternary representations of positive integers. Termination of this rewriting system is equivalent to the Collatz conjecture. To show the feasibility of our approach in proving mathematically interesting statements, we implement a minimal termination prover that uses the automated method of matrix/arctic interpretations and we perform experiments where we obtain proofs of nontrivial weakenings of the Collatz conjecture. Finally, we adapt our rewriting system to show that other open problems in mathematics can also be approached as termination problems for relatively small rewriting systems. Although we do not succeed in proving the Collatz conjecture, we believe that the ideas here represent an interesting new approach.

Verified interactive computation of definite integrals

ABSTRACT. Symbolic computation is involved in many areas of mathematics, as well as in analysis of physical systems in science and engineering. Computer algebra systems present an easy-to-use interface for performing these calculations, but do not provide strong guarantees of correctness. In contrast, interactive theorem proving provides much stronger guarantees of correctness, but requires more time and expertise. In this paper, we propose a general framework for combining these two methods, and demonstrate it using computation of definite integrals. It allows the user to carry out step-by-step computations in a familiar user interface, while also verifying the computation by translating it to proofs in higher-order logic. The system consists of an intermediate language for recording computations, proof automation for simplification and inequality checking, and heuristic integration methods. A prototype is implemented in Python based on HolPy, and tested on a large collection of examples at the undergraduate level.

A Normative Supervisor for Reinforcement Learning Agents (System Description)

ABSTRACT. We introduce a modular and transparent approach for augmenting the ability of reinforcement learning agents to comply with a given norm base. The normative supervisor module functions as both an event recorder and real-time compliance checker w.r.t. an external norm base. We have implemented this module with a theorem prover for defeasible deontic logic, in a reinforcement learning agent that we task with playing "vegan" version of the arcade game Pac-Man.

Automatically Building Diagrams for Olympiad Geometry Problems (System Description)

ABSTRACT. We present a method for automatically building diagrams for olympiad-level geometry problems and implement our approach in a new open-source software tool, the Geometry Model Builder (GMB). Central to our method is a new domain-specific language, the Geometry Model-Building Language (GMBL), for specifying geometry problems along with additional metadata useful for building diagrams. A GMBL program specifies (1) how to parameterize geometric objects (or sets of geometric objects) and initialize these parameterized quantities, (2) which quantities to compute directly from other quantities, and (3) additional constraints to accumulate into a (differentiable) loss function. A GMBL program induces a (usually) tractable numerical optimization problem whose solutions correspond to diagrams of the original problem statement, and that we can solve reliably using gradient descent. Of the 39 geometry problems since 2000 appearing in the International Mathematical Olympiad, 36 can be expressed in our logic and our system can produce diagrams for 94% of them on average. To the best of our knowledge, our method is the first in automated geometry diagram construction to generate models for such complex problems.

The Fusemate Logic Programming System (System Description)

ABSTRACT. Fusemate is a logic programming system that implements the
possible model semantics for disjunctive logic programs. Its
input language is centered around a weak notion of stratification
with comprehension and aggregation operators on top of it.
Fusemate is implemented as a shallow embedding in the Scala
programming language. This enables using Scala data types
natively as terms, a tight interface with external systems, and
it makes model computation available as an ordinary container
data structure constructor.

The paper describes the above features and implementation
aspects. It also demonstrates them with a non-trivial use-case,
the embedding of the description logic ALCIF into Fusemate's
input language.

Unification, Combination, Description Logics, and All That

ABSTRACT. One of the earliest approaches for building decision procedures into theorem
provers was based on employing unification modulo an equational theory. While
this was very successful for a few theories, such as associativity and
commutativity (AC), the more general idea of plugging arbitrary new theories
into the provers when needed did never fly. I will point out that this has not
only practical, but also (complexity) theoretic reasons related to the challenge
of combining unification algorithms, which is considerably harder than the
Nelson-Oppen-style combination of decision procedures. For AC, this is less
problematic, which is actually the case for the whole class of commutative
theories, encompassing AC, ACI, theories relevant for verification of
cryptographic protocols, and ones axiomatizing equivalence in certain
description logics. Speaking of description logics, I will, on the one hand, argue that these kinds
of logic-based knowledge-representation approaches are well-suited for achieving
explainable AI. On the other hand, I will also point out that this does not come
for free, and requires a lot more than just designing and implementing efficient
reasoning procedures for these logics. In particular, it is important to provide
the users with tools that support building and maintaining large knowledge
bases. One of the approaches used in this connection is actually again
unification.