View: session overviewtalk overview

08:00 | Proof Generation in CDSAT |

08:00 | Towards Next Step Guidance in Triangle Construction Problems PRESENTER: Vesna Marinković 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. |

08:30 | Four Geometry Problems to Introduce Automated Deduction in Secondary Schools PRESENTER: Pedro Quaresma 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. |

09:00 | Symbolic Comparison of Geometric Quantities in GeoGebra PRESENTER: Zoltán Kovács 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. |

09:30 | Prooftoys: a Proof Assistant for Beginners 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. |

10:30 | Parallel Probabilistic Inference |

11:00 | Parallel Tricks for Speedy Learned Guidance |

11:30 | Constraint Solving in the Serverless Cloud |

10:30 | Reasoning in Many Logics with Vampire: Everything's CNF in the End |

10:30 | Automated Discovery of Geometrical Theorems in GeoGebra PRESENTER: Zoltán Kovács 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. |

11:00 | Teaching Intuitionistic Propositional Logic Using Isabelle PRESENTER: Jørgen Villadsen 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. |

11:30 | Make Isabelle Accessible! PRESENTER: Walther Neuper 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. |

This will be a structured discussion session arranged around submitted discussion points. The structure will depend on the number of participants. A list of discussion points will be posted on the PDAR website before the session. If you have a discussion point you would like to raise then please contact the chairs.

12:30 | Learning Theorem Proving by Example - Implementing JavaRes PRESENTER: Adam Pease 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. |

13:00 | Evolution of SASyLF 2008-2021 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. |

13:30 | A Drag-and-Drop Proof Tactic PRESENTER: Pablo Donato 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. |

14:30 | How can we make Formal Proof Teachable? |

15:20 | Automated Grading of Automata with ACL2s PRESENTER: Ankit Kumar 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. |

15:50 | Automated Instantiation of Control Flow Tracing Exercises PRESENTER: Clemens Eisenhofer 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. |