ABSTRACT. In this paper we present a procedure used to translate the GeoCoq library, a Rocq formalization of proofs in geometry, into a First-Order Logic encoding in the logical framework \Dedukti. We describe the modifications made to the tool to permit this translation and the process that lead to the first-order simplification. As a result, this translation enables us to share the proofs to other proofs assistants.

ABSTRACT. In this work, we aim at the verification in Coq/Rocq of Beeson's main result in A constructive version of Tarski's geometry, namely that the arithmetization of geometry can be obtain without assuming any decidability property. Our first goal is to deal with the lemmas that do not assert the existence of some geometrical objects. This is what Beeson calls the "wholesale importation of proofs of negative theorems from classical to constructive geometry". Instead of relying on the Gödel double-negation interpretation, we work at the level of tactics, the language that allows to build proofs interactively. Reasoning steps that are not intuitionistically acceptable can still be performed under the assumption that they are used to prove a negative theorem, thus constructivizing the proofs. Thus, we rely on coq-ditto to automate the constructivization process. We report on the current progress towards this goal.

ABSTRACT. When Beeson started his project of computer-checking Euclid's Elements he used a set of $36$ axioms. They can we split into two kinds. 20 of them are Tarski-style axioms and the remaining $16$ are about the notion of equal figures. Then, at the Logic Colloquium 2019, he presented his approach of defining the concept of equal figures and how to prove that it verifies the axioms needed for computer-checking Euclid's Elements. This work was completed with "On the Notion of Equal Figures in Euclid". Our work aims at the formal verification in the Coq/Rocq proof assistant of the proofs from "On the Notion of Equal Figures in Euclid". This would not only guarantee that there is no hole in the proofs, but it would also allow to establish the mutual interpretability between the axioms used in "Proof-Checking Euclid" and the one used by Tarski and his co-authors in "Metamathematische Methoden in der Geometrie". We use the GeoCoq library as a basis for this work. Up to our knowledge, there is no formal verification of the results from "On the Notion of Equal Figures in Euclid".

ABSTRACT. Proof certificates can be used to validate the correctness of algebraic derivations. However, in practice, we frequently observed that the exact same proof steps are repeated for different sets of variables, which leads to unnecessarily large proofs. To overcome this issue we extend the existing Practical Algebraic Calculus with linear combinations (LPAC) with two new proof rules that allow us to capture and reuse parts of the proof to derive a more condensed proof certificate. We integrate these rules into the proof checker Pacheck 2.0. Our experimental results demonstrate that the proposed extension helps to reduce both proof size and verification time.

ABSTRACT. Determining the satisfiability of formulas involving nonlinear real arithmetic and transcendental functions %, such as exponential and sine, is necessary in many applications, such as formally verifying dynamic systems, digital signal processing and motion planning.

Doing this automatically generally requires costly and intricate methods, which limits their applicability.

In the context of SMT solving, Incremental Linearization was introduced recently to facilitate reasoning on this domain, via an incomplete but easy to implement and highly effective approach.

The approach, based on abstraction-refinement via an incremental axiomatization of the nonlinear and transcendental operators, is currently implemented in the SMT solvers MathSAT and cvc5.

The cvc5 implementation is also proof-producing.

In this paper, we present a formalization in the Lean proof assistant of the proof calculus employed by cvc5.

This formalization ensures the soundness of the proof calculus, not only making the underlying algorithm more trustworthy but also enabling the possibility of reconstructing in Lean proofs emitted by cvc5 for this logic fragment.

We discuss how we modeled the rules in the proof assistant and the challenges encountered while formalizing them.

As far as we know, this is the first formalization of a proof calculus for incremental linearization for satisfiability modulo nonlinear arithmetic and transcendental functions.

ABSTRACT. In this talk, I will present Integer linear-exponential programming (ILEP), an extension of integer linear programming (ILP) in which linear systems of inequalities are generalized to also feature two additional functions: the exponential function x → 2^x and the remainder function (x, y) → (x mod 2^y). We will focus on interesting aspects of ILEP, and on the symbolic techniques used to design the current best-known algorithm for solving this problem.

ABSTRACT. Waterproof is educational software, based on a proof assistant, that is intended to help students with acquiring the skill of writing mathematical proofs. This extended abstract compares the proof structure of students who interacted with the software versus that of students who did not, by means of a coding scheme that combines the concepts of proof framework and natural deduction. The results suggest that students become skilled in the type of behavior that gets trained in Waterproof.

ABSTRACT. The use of Large Language Models is on the rise in educational settings such as creating teaching material, helping with assignments or solving exercises. At the same time these new possibilities bring new challenges in regards to the understanding of the capabilities of LLMs. To offer a glimpse into the current capabilities of LLMs in regards to solving coursework, we developed a set of questions from our Bachelor's course Formal Models, which allows us to rate and compare the generated answers of LLMs. We developed an evaluation template to rate the responses, which allows us to not only compare the end result of given answers, but also intermediate steps and understanding of given tasks. The evaluations are presented on an interactive website, which allows us to offer new insights and enables a faster response to newly released models.

ABSTRACT. This note briefly presents the ADG-Lib initiative. Our goal is to provide rigorous descriptions of the axiom systems used by the different geometry automatic and interactive theorem provers, propose common input and output languages for geometry theorem provers, and establish and make available to the research community a large library of geometric problems.

ABSTRACT. The Geometry Automated-Theorem-Provers (GATP) based on the deductive database method, use a data-based search strategy to improve the efficiency of forward chaining. An implementation of such a method is expected tobe able to efficiently prove a large set of geometric conjectures, producing readable proofs. The number of conjectures a given implementation can prove will depend on the set of inference rules chosen. Natural language and visual renderings of the proofs are made possible by the use of a synthetic forward-chaining method. In the original approach, the method and the corresponding implementation had the axioms and rules of inference hard-coded. In our implementation, the OGP-GDDM Prover, we used an approach based in an SQL database library and an in-memory database to allow a more flexible approach to re-implementations of the provers whenever a different set of axioms and rules of inference is needed. The Provers-Generator for the Geometric Deductive Databases Method (PG for short) is the next natural step. The PG is a program that, given a set of rules, generates a prover, an OGP-GDDM-prover, for that specific set of rules. The applications in areas such as education are very important given the possibility, opened by the PG, of having a prover, capable of producing readable proofs, adapted to a specific audience.

ABSTRACT. The Model Constructing Satisfiability (MCSat) approach to Satisfiability Modulo Theories (SMT) has demonstrated strong performance when handling complex theories such as nonlinear arithmetic. Despite being in development for over a decade, there has been limited research on the heuristics utilized by MCSat solvers as in Yices2.

In this paper, we discuss the decision heuristics employed in the MCSat approach of Yices2 and empirically show their significance on QF_NRA and QF_NIA benchmarks. Additionally, we propose new ideas to enhance these heuristics by leveraging theory-specific reasoning and drawing inspiration from recent advancements in SAT solvers.

Our new version of the MCSat Yices2 solver not only solves more nonlinear arithmetic benchmarks than before but is also more efficient compared to other leading SMT solvers.

ABSTRACT. This paper presents a pedagogical experience integrating the Maude language into a master's-level course on automated software verification. The course aims to provide students with both theoretical foundations and practical skills in formal methods, particularly through model checking and equational reasoning. Maude, a high-performance logical framework based on rewriting logic, was selected due to its strong formal semantics and versatility. Over the semester, students engaged in hands-on assignments using Maude to specify and verify system properties, culminating in a mini-project. The outcomes indicate that Maude facilitated a deeper understanding of formal verification techniques and allowed students to model complex systems concisely and rigorously. Reflections on student feedback and course design are discussed to inform future integration of formal tools in software verification curricula.

ABSTRACT. For more than five years we have used the Isabelle proof assistant to teach metatheory of propositional and first-order logic, not only for natural deduction and sequent calculus, but also for simple axiomatic systems. Languages of any cardinality are supported. We present the tools and the lessons learned. The focus is on the formal soundness and completeness theorems for classical propositional logic.

ABSTRACT. IsaGeoCoq is a port of GeoCoq 2.4.0, library written for Rocq, to Isabelle/HOL. A brief description of all the translated files is presented, as well as the difficulties encountered during the manual translation and useful resources such as the sledgehammer tool. Par- ticular emphasis is placed on the evolution of the work: initially the translation contained some implications at the level of the postulates of parallels. Currently, many equivalences between postulates have been formalized thanks to the translation of the results obtained in GeoCoq, but also the construction of many notions included in the first part of the book "Metamathematische methode in des geometrie", allowing to demonstrate the Pythagorean theorem, secondary school level exercises, but also interpretations between different axiom systems such as those of Tarski and Hilbert.

ABSTRACT. We use elementary geometry and elimination to prove some non-trivial theorems on regular polygons, including regular 5-, 7- and 9-gons. The required knowledge to follow the proofs does not go beyond high school knowledge.

ABSTRACT. The Cylindrical Algebraic Decomposition (CAD) method is currently the only complete algorithm used in practice for solving real-algebraic problems. To ameliorate its doubly-exponential complexity, different exploration-guided adaptations try to avoid some of the computations. The first such adaptation named NLSAT was followed by Non-uniform CAD (NuCAD) and the Cylindrical Algebraic Covering (CAlC). Both NLSAT and CAlC have been developed and implemented in SMT solvers for satisfiability checking, and CAlC was recently also adapted for quantifier elimination. However, NuCAD was designed for quantifier elimination only, and no complete implementation existed before this work.

In this paper, we present a novel variant of NuCAD for both real quantifier elimination and SMT solving, provide an implementation, and evaluate the method by experimentally comparing it to CAlC.

ABSTRACT. The cylindrical algebraic decomposition (CAD) is the only complete method used in practice for solving problems like quantifier elimination or SMT solving related to real algebra, despite its doubly exponential complexity. Recent exploration-guided algorithms like NLSAT, NuCAD, and CAlC rely on CAD technology but reduce the computational effort heuristically. Single cell construction is a paradigm that is used in each of these algorithms.

The central property on which the CAD algorithm is based is called delineability. Recently, we introduced a weaker notion called projective delineability which can require fewer computations to guarantee, but needs to be applied carefully. This paper adapts the single cell construction for exploiting projective delineability and reports on experimental results.

ABSTRACT. Given a linear equation ℰ of the form ax + by = cz where a, b, c are positive integers, the k-colour Rado number R_k(ℰ) is the smallest positive integer n, if it exists, such that every k-colouring of the positive integers {1, 2, ..., n} contains a monochromatic solution to ℰ. In this paper, we consider k = 3 and the linear equations ax + by = bz and ax + ay = bz. Using SAT solvers, we compute a number of previously unknown Rado numbers corresponding to these equations. We prove new general bounds on Rado numbers inspired by the satisfying assignments discovered by the SAT solver. Our proofs require extensive case-based analyses that are difficult to check for correctness by hand, so we automate checking the correctness of our proofs via an approach which makes use of a new tool we developed with support for operations on symbolically-defined sets—e.g., unions or intersections of sets of the form {f(1), f(2), ..., f(a)} where a is a symbolic variable and f is a function possibly dependent on a. No computer algebra system that we are aware of currently has sufficiently capable support for symbolic sets, leading us to develop a tool supporting symbolic sets using the Python symbolic computation library SymPy coupled with the Satisfiability Modulo Theories solver Z3.

ABSTRACT. How to handle division in systems that compute with logical formulas involving what would otherwise be polynomial constraints over the real numbers is a surprisingly difficult question. This presentation reports recently published work that surveys existing solutions, describes their issues, and proposes a novel solution for the problem that is specifically tailored to tools from symbolic computing and real algebraic geometry.