ABSTRACT. We describe our work in progress on extending our automated triangle construction solver ArgoTriCS with the possibility of checking correctness of partial constructions given by the student and suggesting the next construction step when the student gets stuck.

ABSTRACT. The introduction of automated deduction systems in secondary schools face several bottlenecks, the absence of the subject rigorous mathematical demonstrations in the curricula, the lack of knowledge by the teachers about the subject and the difficulty of tackling the task by automatic means.

We are proposing that we can, nevertheless, introduce the subject of automated deduction in secondary problems by addressing it in particular cases. Particular cases, simple to manipulate by students and teachers, and reasonably easy to be dealt by automatic means. In such a way that friendly, with a natural language and geometric renderings, geometry automated theorem prover can be built.

The subject is discussed addressing four problems secondary schools geometry problems. Its rigourous proofs, visual proofs, numeric proofs, algebraic formal proofs, synthetic formal proofs, or the lack of them. Four this problems we discuss a classroom plan to address them with the help of Information and Communications Technology (ICT), more specifically, automated deduction tools.

ABSTRACT. Comparison of geometric quantities usually means obtaining generally true equalities of different algebraic expressions of a given geometric figure. Today's technical possibilities already support symbolic proofs of a conjectured theorem, by exploiting computer algebra capabilities of some dynamic geometry systems as well. We introduce GeoGebra's new feature, the Compare command, that helps the users in experiments in planar geometry. We focus on automatically obtaining conjectures and their proofs at the same time, including not just equalities but inequalities too.

ABSTRACT. Prooftoys is a web-based visual proof assistant with a modern user interface, written in JavaScript to run in modern Web browsers.

Its purpose is to support non-experts in exploration and self-education in logic and axiomatic mathematical reasoning, using the real numbers as a starting point. The design is driven by an overriding concern for simplicity and a less difficult learning process.

This demonstration walks through several scenarios of use of Prooftoys, showing how to work with it, what to expect from it, and hopefully revealing a little about the principles it is based on.

ABSTRACT. In various provers and deductive verification tools, logical transformations are used extensively in order to reduce a proof task into a number of simpler tasks. Logical transformations are often part of the trusted base of such tools. In this paper, we develop a framework to improve confidence in their results. We follow a modular and skeptical approach: transformations are instrumented independently of each other and produce certificates that are checked by a third-party tool. Logical transformations are considered in a higher-order logic, with type polymorphism and built-in theories such as equality and integer arithmetic. We develop a language of proof certificates for them and use it to implement the full chain of certificate generation and certificate verification.

ABSTRACT. Whereas proof assistants based on Higher-Order Logic benefit of automation from external solvers, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter is a more expressive logic which is further from first-order logic, the logic of most automatic theorem provers. In this article, we develop a methodology to transform a subset of Coq goals into first-order statements that can be automatically discharged by automatic provers. The general idea is to write modular, pairwise independent transformations and combine them. Each of these eliminates a specific aspect of Coq logic towards first-order logic. As a proof of concept, we apply this methodology to a set of simple but crucial transformations which extend the local context with proven first-order assertions that make Coq definitions and algebraic types explicit. They allow users of Coq to solve non-trivial goals automatically. This methodology paves the way towards the definition and combination of more complex transformations, making Coq more accessible.

ABSTRACT. We describe a prototype of a new experimental GeoGebra command and tool Discover that analyzes geometric figures for salient patterns, properties, and theorems. This tool is a basic implementation of automated discovery in elementary planar geometry.

ABSTRACT. We describe a formalization of intuitionistic propositional logic in the Isabelle/Pure framework. In contrast to earlier work (where we explored the pedagogical benefits of using a deep embedding approach to logical modelling) here we employ a simpler axiomatic instance modelling. This gives rise to simple and natural teaching examples and we report on the role it played in teaching our Automated Reasoning course in 2020 and 2021.

ABSTRACT. Isabelle and other advanced proof assistants are reaching maturity for engineering of security-critical software and for clarifying abstract mathematics; they implement a vast amount of mechanised mathematics knowledge. Isabelle provides several front-ends, and an experimental one is VSCode.

At Johannes Kepler University the “Institut Integriert Studieren (IIS)” is involved in supporting students with special needs and in research to make software “accessible” for those students. Since one member of IIS and co-author of this paper is a mathematician and and personally affected by special needs in vision, accessibility in mathematics software is an important field of research of IIS.

The recent discovery, that Isabelle/VSCode is greatly accessible, now comes into relation with long-lasting cooperation in the ISAC -project: presently the ISAC -prototype is being integrated into Isabelle such, that it can re-use all of it’s front-ends (and eventually inheriting accessibility).

ISAC had been designed to re-use Isabelle’s mathematics knowledge, but it reduces the complexity of proof to “structured derivations”, that means to calculations as taught in academic engineering courses and at high-school. So this paper envisages new prospects to continuous tool support for mathematics at the interface between high-school and university for all students, including visually impaired ones.

ABSTRACT. Recently, we developed an automated theorem prover for projective incidence geometry. This prover, based on a combinatorial approach using matroids, proceeds by saturation using the matroid rules. It is designed as an independent tool, implemented in C, which takes a geometric configuration as input and produces as output some Coq proof scripts: the statement of the expected theorem, a proof script proving the theorem and possibly some auxiliary lemmas. In this document, we show how to embed such an external tool as a plugin in Coq so that it can be used as a simple tactic.

ABSTRACT. The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the conjunctive normal form (CNF) format used for SAT proof logging means that it is hard to extend the method to other, stronger, solving paradigms for combinatorial problems. We show how to instead leverage the cutting planes proof system to provide proof logging for pseudo-Boolean solvers that translate pseudo-Boolean problems (a.k.a 0-1 integer linear programs) to CNF and run CDCL. We are hopeful that this is just a first step towards providing a unified proof logging approach that will also extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.

ABSTRACT. The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are used within multiple applications, and other solvers generate proofs in the same format. Now we would like to gather feedback from the community to guide future developments. Towards this, we review the history of the format, present our pragmatic approach to develop the format, and also discuss problems that may arise when other solvers use the format.

ABSTRACT. Did PyRes [15] achieve its goal of being a sufficient model for learning about how to implement a first-order ATP system? JavaRes is a demonstration prover patterned after PyRes. In this paper we discuss the architecture and data structures of this prover and the experience of one of us implementing the prover, without prior expertise in writing an au- tomated theorem prover prover. We present performance measurements relative to PyRes and other systems. To illustrate the value of JavaRes for learning about theorem proving we also mention the implementation of several features beyond the original PyRes concept.

ABSTRACT. SASyLF was released in 2008 and used as a proof assistant in courses at several universities. It proved itself useful and has continued to be used, and each iteration of use has encouraged further development: fixing bugs and adding enhancements. This paper describes how SASyLF was developed while keeping true to its purpose. Most notable are making substitutions explicit, support of and/or, support for mutual and lexicographic induction. and IDE support.

ABSTRACT. Resuming the effort initiated by the proof-by-pointing project, in which formal proofs are constructed through mouse actions, we present a first version of a drag-and-drop proof tactic. We argue that such a tactic provides quick and intuitive proof construction steps and could be a step towards more accessible proof-systems, for instance in education. The precise description of the tactic and its implementation involve theoretical tools coming from focused proofs and deep inference.

ABSTRACT. Almost all Computer Science programs require students to take a course on the Theory of Computation which covers various models of computation such as finite automata, push-down automata and Turing machines. Theory of Computation courses tend to emphasize paper-and-pencil mathematics over programming. As a consequence, students typically receive feedback on their work only after it has been graded, which can take several weeks. We present tools that provide automatic feedback for constructing finite automata, push-down automata and Turing machines. These tools are based on the ACL2s interactive theorem prover, which provides advanced methods for stating as well as proving and disproving conjectures. Since feedback is automatic, our tools can be deployed at scale and integrated into massively open online courses.

ABSTRACT. One of the first steps in learning how to program is reading and tracing existing code. In order to avoid the error-prone task of generating variations of a tracing exercise, our tool TATSU generates instances of a given code skeleton automatically. This is achieved by a finite unfolding of the program in the style of bounded model checking and using the SMT solver Z3 to find models for this unfolded program.