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