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. 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. 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.