ABSTRACT. We present an approach for testing student learning outcomes in a course on automated reasoning using the Isabelle proof assistant. The approach allows us to test both general understanding of formal proofs in various logical proof systems and understanding of proofs in the higher-order logic of Isabelle/HOL in particular. The use of Isabelle enables almost automatic grading of large parts of the exam. We explain our approach through a number of example problems, and explain why we believe that each of the kinds of problems we have selected are adequate measures of our intended learning outcomes.

ABSTRACT. Satisfiability Modulo Theories (SMT) solvers are widely used in various applications, most prominently verification of hardware and software. They are focused on the task of checking the satisfiability of first-order formulas over a wide range of background theories. Currently, mainstream SMT-solvers offer easy to use APIs and textual interfaces, and are accessible even to users with little logical background. Nevertheless, their algorithms are based on interesting and varied theoretical subjects.

For these reasons, SMT as a field is a good candidate for introducing automated reasoning and logic to students with little or no background in logic: its wide applicability provides a great motivation to study them, the solvers’ accessibility offers hands-on exercises and the logical foundations contain a wide variety of topics of different levels and depth.

In this talk I will describe my experience in teaching an automated reasoning class focused on SMT. I will describe my original hypotheses and plans before the class, what happened during the class, and some reflections that occurred in the process.

ABSTRACT. We have developed a web-based graphical proof assistant, the Proof Tree Builder, that lets you apply rules upwards from the initial goal in sequent calculus and Hoare logic for a simple imperative language. We equipped our tool with a basic proof automation feature and Z3 integration. Students in the automated reasoning course at Princeton University used our tool and found it intuitive. The Proof Tree Builder is available online at https://proof-tree-builder.github.io.

ABSTRACT. Geometry Automated Theorem Provers have now what may be considered a long story. Since the early attempts, linked to Artificial Intelligence, synthetic provers based on inference rules and using forward chaining reasoning are considered the more suited for education. Using an appropriated set of rules and using forward chaining they can more easily mimic the expected behaviour of a student when developing a proof. We describe an implementation of the geometry deductive database method, discussing its merits, and demerits when an application in education is concerned.

ABSTRACT. After a short survey of the developments of CAS, DGS and other useful technologies, such as internet, we show their implication in Mathematics Education, and in the broader frame of STEAM Education. In particular we discuss the transformation of Mathematics Education into exploration-discovery-conjecture-proof scheme. This scheme fits well into the so-called 4 C’s of 21st Century Education.

ABSTRACT. The introduction of automated deduction systems in secondary schools face several bottlenecks, apart the problems related with the curricula and the teachers, the dissonance between the outcomes of the Geometry Automated Theorem Provers and the normal practice of conjecturing and proving in schools is a major barrier to a wider use of such tools in an educational environment. Since the early implementations of Geometry Automated Theorem Provers, applications of Artificial Intelligence methods, synthetic provers based on inference rules and using forward chaining reasoning are considered to be more suited for education proposes. Choosing an appropriate set of rules and a automated method that can use those rules is a major challenge. We discuss one such rule set and its implementation using the geometry deductive databases method. The approach is tested using a set of geometric conjectures that can be the goal of a 7th year class.