The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs

TL;DR

This paper introduces a teaching tool for the sequent calculus that uses automated reasoning to help students understand formal proofs in First-Order Logic, addressing both syntactic and semantic learning challenges.

Contribution

The paper presents a novel educational tool that combines automated reasoning with didactical strategies to improve student understanding of formal proofs in sequent calculus.

Findings

Enhanced student understanding of proof construction

Effective support for syntactic and semantic learning challenges

Improved engagement with formal logic concepts

Abstract

The sequent calculus is a formalism for proving validity of statements formulated in First-Order Logic. It is routinely used in computer science modules on mathematical logic. Formal proofs in the sequent calculus are finite trees obtained by successively applying proof rules to formulas, thus simplifying them step-by-step. Students often struggle with the mathematical formalities and the level of abstraction that topics like formal logic and formal proofs involve. The difficulties can be categorised as syntactic or semantic. On the syntactic level, students need to understand what a correctly formed proof is, how rules can be applied (on paper for instance) without leaving the mathematical framework of the sequent calculus, and so on. Beyond this, on the semantic level, students need to acquire strategies that let them find the right proof. The Sequent Calculus Trainer is a tool that is designed to aid students in learning the techniques of proving given statements formally. In this paper we describe the didactical motivation behind the tool and the techniques used to address issues on the syntactic as well as on the semantic level.