Paper Info
Title
The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs.
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.
Year
DOI
Venue
2018
10.4204/EPTCS.267.2
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
DocType
Volume
Issue
Journal
abs/1803.01467
267
ISSN
Citations 
PageRank 
2075-2180
0
0.34
References 
Authors
7
3
Name
Order
Citations
PageRank
Arno Ehle100.34
Norbert Hundeshagen231.50
Martin Lange344722.83