ABSTRACT. We describe the implementation of the alternating path method for premise selection in the theorem prover PyRes.

ABSTRACT. Simple Clause Learning (SCL) is an automated theorem proving technique for first-order logic that Christoph Weidenbach and his team have designed and studied in recent years. In this extended abstract, I adapt a method for model construction presented by Bromberger, Krasnopol, Möhle and Weidenbach in 2024 at IJCAR to make it more directly useful to SCL.

ABSTRACT. In this contribution, we compare three different options to define geometric difficulty of geometry problems. By computing correlation between the achieved values and the algebraic complexity, and, alternatively, ad-hoc human intuition, we confirm that our former definition seems acceptable.

ABSTRACT. This article compares different proving methods for projective incidence theorems. In particular, a technique using quadrilateral tilings recently introduced by Sergey Fomin and Pavlo Pylyavskyy is shown to be at most as strong as proofs using bi-quadratic final polynomials and thus, also proofs using Ceva-Menelaus-tilings. Furthermore, the equivalence between quadrilateral-tiling-proofs and proofs using exclusively Menelaus configurations is shown as well as additional results for Ceva-Menelaus-proofs.

ABSTRACT. Gelernter's Geometry Machine is significant not only as the very first automated prover for geometry but also as one of the earliest artificial intelligence systems. Developed almost seventy years ago, it remains a seminal work, in some aspects still fresh and inspiring. In this paper, we provide historical reflections on the Geometry Machine, interpret its results in modern terms, and attempt to reproduce its outputs.

ABSTRACT. We discuss some possible characterizations of regular polygons that can be directly used in algebraic provers in automated reasoning in geometry.

ABSTRACT. Metamath is an established computer language for archiving, verifying, and studying mathematical proofs. Its basis is condensed detachment, with unification and a view on proofs as terms. Grammar-based tree compression applied to such proof terms factorizes repeated patterns, which provide proofs of definite clauses, pattern variables corresponding to body atoms. A Metamath database is then just a grammar that compresses a set of giant proof trees. We provide a formal account of this view and have implemented a practical toolkit. In experiments we compare the proof structuring of Metamath by human experts with machine-generated structurings, and address possibilities of the interplay of both.

ABSTRACT. Techniques for synthesizing inductive invariants of distributed algorithms are becoming useful. This presentation reports on recent work for generating an inductive invariant for the Raft consensus algorithm, and it points out the importance of designing decidable and expressive fragments of first-order logic.

ABSTRACT. The SCAN algorithm aims to solve the problem of eliminating second-order quantifiers from an existentially second-order quantified first-order formula and equivalently expressing it in first-order logic. This problem has applications in many subfields of computer science, from modal correspondence theory, knowledge representation, and automated reasoning to verification. In this paper we consider the application of the SCAN algorithm to basic path logic and the ordered fragment of first-order logic. We extend the clausal class of basic path logic to accommodate inequalities, which characterizes the search space of SCAN for basic path logic. By introducing constant Skolemization, we show that sentences of the ordered fragment can be transformed into basic path clauses and the generalized class, and this transformation preserves logical consequences in the ordered fragment. We prove that SCAN terminates on clauses of basic path logic, and therefore it decides second-order quantifier elimination and semantic forgetting for basic path logic. We show a general result that inequalities between constants can be eliminated without cost to consequences in basic path logic or the ordered fragment. The result also shows that SCAN can compute uniform interpolants expressed in basic path logic of ordered sentences.

ABSTRACT. An approach to planning in which states are represented as first-order terms is presented. Fluents can be computed from the term structure, and actions on the states correspond to rewrite rules on the terms. Actions that only depend on or influence a subset of the fluents can often be described as rewrite rules that operate on subterms of the terms. If actions are bidirectional, then efficient completion methods can be used to solve planning problems. Such completion methods first show that a plan exists and then can construct it explicitly. This approach is guaranteed to find a solution to a planning problem if one exists, but not necessarily an optimal one. Some ideas for optimizing plans found in this way are sketched. An implementation shows that this approach can sometimes show quickly that a very long plan exists. The time to find a plan is important as well as the cost of the plan. The time to construct the plan will be proportional to the length of the plan. Some examples are given, and an argument is given that this approach can be more efficient than other common approaches to planning. If this approach quickly show that a plan exists, then the plan has a succinct representation even though the plan may be very long. Also, even before constructing the entire plan, a term representing a state somewhere in the middle of the plan can be computed efficiently.

ABSTRACT. In our contribution, we discuss the current performance of the GeoGebra Discovery LocusEquation command, which automatically outputs where to place some point in a construction so that a given property is satisfied. We will show some examples of unexpected output of this command, regarding different computational or interpretative issues (number of conditions, non-principal locus ideals, nondegeneracy conditions, etc.). Then we focus on the proposal of some theoretical and algorithmic recommendations to improve the performance of this LocusEquation command.

ABSTRACT. We present an exploration of inferring orientations for point configurations. We can compute the orientation of every triple of points by a combination of direct calculation and inference from prior computations. This ``parsimonious'' approach was suggested by Knuth in 1992, and aims to minimize calculation by maximizing inference. We wish to investigate the efficacy of this approach by investigating the minimum and maximum number of inferences that are possible for a point set configuration. To find the configurations which yield maximum inferences, there is no direct formula and hence two constructive approaches are suggested. A basic analysis of sequences that achieve those maximum inferences is also presented and some properties have been proved regarding their existence.

ABSTRACT. The diversity of output encodings of different reasoning systems hinders proof verification and interoperability. The Dedukti framework addresses this issue by implementing the λΠ-calculus modulo, enabling proofs from different frameworks to be expressed, combined, and checked automatically. We identify common challenges and requirements for verifying proofs of automated theorem provers for higher-order logic, and develop general strategies for systematically deriving encodings of calculus rules and proof steps. Building on these strategies, we propose a modular encoding approach, which we demonstrate and evaluate using the higher-order logic prover Leo-III. This effort has already led to the discovery and resolution of minor bugs in the original prover.

ABSTRACT. The cylindrical algebraic covering method is an approach for deciding the satisfiability of non-linear real arithmetic formulas. We extend that method for optimization modulo theories (OMT), allowing to find solutions that are optimal w.r.t. a given polynomial objective function. Our approach is complete and detects unbounded objective functions as well as infima/suprema, which the objective function can approach, but never reach. We show how to construct meaningful models even in those special cases and provide an experimental evaluation demonstrating the advantages of our method compared to approaches based on quantifier elimination or incremental linearization.

ABSTRACT. Satisfiability modulo theories (SMT), if summarized into a single sentence, studies algorithms to test whether a formula is satisfied in a given theory. Theory combination is a branch of SMT where we combine these algorithms in order to obtain one that works for the combined theory: methods include Nelson-Oppen ([NO79]), and those involving shininess ([RRZ05a]) and gentleness ([Fon09]).

One method that, although extremely useful and used in cvc5 ([BBB+22]), had a complicated history is the one involving strong politeness ([JB10]). It started as only politeness in [RRZ05b], meaning smooth and finitely witnessable. A theory is smooth when we can increase one of its models as we please while keeping a fixed formula ϕ satisfied. Finite witnessability, on the other hand, is far more difficult to intuit. It involves a computable function wit, called a witness, that takes a quantifier-free formula ϕ and returns another quantifier-free formula wit(ϕ) such that: first, ϕ and wit(ϕ) are essentially equivalent (more precisely, ϕ is T-equivalent to the existential closure of wit(ϕ) with respect to those variables not in ϕ); and, if ϕ is actually satisfiable in T, then there is a T-interpretation that satisfies ϕ where every element is the interpretation of a variable in wit(ϕ). In a sense, wit(ϕ) ”witnesses” all elements of some T-interpretation that satisfies ϕ, so we can say that this interpretation is ”witnessed”.

But the proof that this method worked was flawed. A correction was found in [JB10], the corresponding property being later on named strong politeness. The underlying algorithm is the same as the one for politeness, but in the earlier case the algorithm was not sound. The combination method then guarantees, essentially, that if two theories are decidable, and one of them is strongly polite, then their combination is also decidable, strong politeness being the conjunction of smoothness and strong finite witnessability. The latter is almost the same as finite witnessability, except that now wit is required to maintain, in the witnessed model, the relationship between variables found in the starting model, where ϕ is known to be satisfied. Notice, however, that [JB10] did not prove that theory combination assuming only politeness is not possible, only that the provided proof did not work.

Later on, in [CR13,CR18], strong politeness plus decidability was proven to be equivalent to shininess, property involved in another theory combination method; a theory is shiny when it is smooth; stably finite, a property guaranteeing that if a quantifier-free formula has a T-interpretation where it is satisfied, then it has another T-interpretation where it is satisfied and whose domains are finite and of cardinality equal to or lesser than the cardinality of the corresponding domains in the starting interpretation; and one can computably find the minimal (tuples of) cardinalities of a T-interpretation that satisfies a given quantifier-free formula. Were strong politeness to imply decidability, we would have that not only strong politeness itself is equivalent to shininess, but the theory combination method involving strong politeness could be simplified: if a theory is strongly polite and another is decidable, then their combination is decidable.

A natural follow-up question was whether there are actually theories that were polite without being strongly polite: if they don’t exist, then the proof that theory combination with strong politeness is possible also proves that theory combination with only politeness is possible. A simple counterexample was eventually found in [SZR+21], but it was not stably finite. This is important as strong finite witnessability is deeply related to stable finiteness: it seemed like politeness and stable finiteness could imply strong politeness.

In summary, many open questions were left in the study of polite and strongly polite theories: 1. Can we simplify strong politeness (to, for example, politeness)? 2. Does strong politeness imply decidability? 3. Are polite and stably finite theories also strongly polite? Notice that a positive answer to the third question could possibly imply a positive one for the first as well, were we to find a combination method assuming only politeness and stable finiteness. We have recently found a partial simplification of strong politeness, giving a somewhat positive answer to the first question, but proved that the others have negative answers. We here present some of these results.

In [TZB23] we started an analysis of the interplay between several combination methods, showing that strong politeness could be replaced by strong finite witnessability and stable infiniteness, a property already well-known given its use in the Nelson and Oppen combination method and weaker than smoothness. Later on, in [PdTZB24], this result was strengthened, at the cost of a significantly more challenging proof, to show that actually stable infiniteness and strong finite witnessability imply strong politeness, thus offering a positive answer to the first question.

In addition, [TZB23] presented a theory that is polite and stably finite with- out being strongly polite, answering the third question in the negative. This theory achieves this by, in a way, having a predictable (read computable) behavior for its models of cardinality a power of 2, while its other models are somewhat unpredictable. Finally, in a paper under peer-review, we construct a theory that is strongly polite yet not decidable, settling the last of these open problems, again in the negative. There is, however, a silver lining to this submitted paper, which also shows that a ”decidability-free” definition of shininess still implies decidability.

All of these results follow, as well as complement, the history of politeness in theory combination so far, enhancing our understanding of this sometimes difficult technique. And they herald the use of new instruments, from areas such as model theory, complexity theory or order theory, in theory combination, that in turn lead to new, sharper results.

ABSTRACT. In his \emph{Automated Reasoning Building Blocks}, Weidenbach presented a version of the CDCL calculus (and a proof of non-redundancy). This calculus is the base for IsaSAT, the only verified SAT solver to take part in the SAT Competition.

In this abstract presentation, we discuss the differences between the abstract calculus and the concrete implementations found in SAT solvers.

Recently, Briefs and he have rediscovered chronological backtracking with a different aim: generalizing the non-redundancy to SMT solving. We discuss the difference between his presentation and the other existing ones.

ABSTRACT. Over the centuries, geometric construction problems have received significant attention. Although many of these problems can be solved using only a ruler and a compass, there are some that cannot. Relatively little effort has been devoted to identifying construction problems that have an obstruction to their solution. This paper focuses on locus-dependent problems – problems where the required figure exists only under specific constraints on the given elements. We explore various types of locus dependencies encountered in geometric constructions and propose automated procedures to solve these types of problem.

ABSTRACT. The concept of what makes a geometric theorem “interesting” is deeply rooted in human intuition, pedagogy, and aesthetic perception. Despite its centrality in the mathematical experience, “interestingness” remains elusive to formal characterisation. Larry Wos highlighted this profound challenge in his 31st problem [8], calling for methods not only to automate theorem proving but to enable the generation and recognition of new and interesting theorems. Building upon Wos’ foundational insight, Quaresma, Graziani, and Nicoletti [6] formalised a related and precise computational question: whether it is algorithmically decidable if a Turing Machine can produce interesting theorems. By reduction to Rice’s theorem [7], they demonstrated that this problem is undecidable, establishing significant theoretical limits. However, this does not mean we cannot attempt to address Wos’ problem (specifically its aspect concerning interestingness) in a heuristic way. In our project, we aim to present a methodology capable of exploring the structural properties of geometric theorems that may underlie their perceived interestingness. Our approach systematically integrates human-based survey data, automated theorem proving, and Geometrographic analysis. First, we will show how it is possible to build upon the results of a comprehensive survey conducted among mathematicians, educators, and students. Participants were asked to list geometric theorems they considered interesting and to provide qualitative explanations for their choices. This phase allowed us to capture the human dimension of mathematical interest, revealing subjective factors such as simplicity, elegance, surprise, utility, and conceptual depth. Second, we will show how to construct formal proofs for each identified theorem using automated theorem proving tools, specifically employing the Area Method [2] (and similar methods that can be characterised geometrographically) as implemented in the GCLC prover [1,3]. These proofs will be synthetically generated, ensuring uniformity and enabling precise structural analysis. Third, we will show how the given formal proof can be analysed using a set of quantitative metrics, known as Geometrographic coefficients A precondition to this project is the need to have a rigorous characterisation of the human perception of interestingness. For that matter, we designed a survey. Answers have been collected about the subject of interesting geometric theorems.

ABSTRACT. We explore envelopes and osets, using automated commands for envelopes and geometric loci. The topology of envelopes and osets is generally more complicated than that of the progenitor, whence the importance to study the singularities. The work involves both analytic and algebraic methods (Gröbner bases, elimination), and networking between dierent kinds of software. Accurate plotting is a central issue, for which the new command Plot2D provided by GeoGebra-Discovery is ef- cient. Finally we discuss briey how some pitfalls of AI can and should be used to develop critical thinking and other skills. The activities presented here have been proposed to in-service teachers learning towards an advanced degree.

ABSTRACT. We present novel semiring semantics for abstract reduction systems (ARSs), i.e., a set A together with a binary relation → denoting reductions. More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a semiring S = (S, ⊕, ⊙, 0, 1), which consists of a set S associated with two operations ⊕ and ⊙ with identity elements 0 and 1, respectively. Inspired by provenance analysis in database theory and logic, we obtain a formalism that can be used for provenance analysis of arbitrary ARSs. Our semantics handle (possibly unbounded) non-determinism and possibly infinite reductions. For that reason, we consider semirings where the natural order (that is induced by addition of the semiring) forms a complete lattice. In most applications of semiring semantics in logic, a higher “truth value” w.r.t. the natural order is more desirable, e.g., for the confidence semiring Sconf = ([0, 1], max, ·, 0, 1) that can be used to assign confidence values to facts, one would like to obtain a value close to the most desirable confidence 1. However, in the application of software verification, it is often the reverse, e.g., for computing the runtime of a reduction via the arctic semiring Sarc = (N±∞, max, +, −∞, 0). While every runtime t < ∞ may still be acceptable, the aim is to prove boundedness, i.e., that the maximum ∞ (an infinite runtime) cannot occur. Our semiring semantics capture and generalize numerous formalisms that have been studied in the literature. For example, boundedness w.r.t. different semirings can imply termination of the underlying ARS, it can ensure that certain bad states cannot be reached (safety), etc. By considering tuples over different semirings, we can combine multiple analyses into a single combined framework analyzing combinations of properties, where simply performing each analysis separately fails. Due to our generalization of existing formalisms via our semiring semantics, we can now use techniques and ideas from, e.g., termination analysis, to prove boundedness or other properties (or combinations of properties) of reduction systems using a completely different semiring. We present sufficient conditions for boundedness and show that the interpretation method, a well-known method to, e.g., prove termination of ARSs, can be generalized to a sound (and sometimes complete) technique to prove boundedness. On the other hand, we also try to find worst-case lower bounds on weights in order to detect bugs and possible denial of service attacks.

ABSTRACT. n/a (the submission itself is a one-page abstract)

ABSTRACT. This paper describes the (new) TPTP format for recording clausal tableau proofs. The format builds on the existing infrastructure of the TPTP World, in particular the TPTP format for recording derivations. An ATP system that outputs tableaux in this format is described. Existing TPTP World tools for verifying and viewing derivations can be directly extended to verify and view tableaux recorded in this new format.

ABSTRACT. We introduce jeha, an Isabelle/HOL tactic and automated theorem prover based on the λ-superposition calculus. An alternative to Isabelle’s metis tactic, jeha targets higher-order logic directly, avoiding the overhead introduced by metis’ translations to first-order logic. Like metis, jeha can be used as a reconstruction backend for Sledgehammer to improve the reconstruction rate of proofs produced by external higher-order automated theorem provers such as E, Vampire, and Zipperposition.

ABSTRACT. We formalize classical first-order logic with functions in the proof assistant Isabelle/HOL. The standalone formalization is based on entries in the Isabelle Archive of Formal Proofs. The soundness and completeness theorems hold for languages of arbitrary cardinalities. The 3 axioms and 3 rules together cover implication, negation and universal quantification. The unique approach has been used to teach formal methods and automated reasoning.