Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned

Jørgen Villadsen

TL;DR

MiniCalc introduces a minimal sequent calculus for first-order logic with function symbols, implemented as a web tool with optional Isabelle verification. The paper outlines a three-step development: (1) naming and organizing the rule set, (2) enriching the syntax with datatypes and de Bruijn indices while establishing an environment-based semantics, and (3) embedding the construction in Isabelle with inductive definitions and derived rules such as Ext and NegNeg. It provides concrete example proofs (trivial, default, and advanced like the drinker paradox) to illustrate proof layout, notation, and interoperability with Isabelle. Finally, it reports teaching experience from a 5 ECTS MSc course on automated reasoning, including student engagement, assessment structure (MiniCalc-based proofs and Isabelle/Isar work), and the role of formal verification in education.

Abstract

MiniCalc is a web app for teaching first-order logic based on a minimal sequent calculus. As an option the proofs can be verified in the Isabelle proof assistant. We present the lessons learned using the tool in recent years at our university.

Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned

TL;DR

MiniCalc introduces a minimal sequent calculus for first-order logic with function symbols, implemented as a web tool with optional Isabelle verification. The paper outlines a three-step development: (1) naming and organizing the rule set, (2) enriching the syntax with datatypes and de Bruijn indices while establishing an environment-based semantics, and (3) embedding the construction in Isabelle with inductive definitions and derived rules such as Ext and NegNeg. It provides concrete example proofs (trivial, default, and advanced like the drinker paradox) to illustrate proof layout, notation, and interoperability with Isabelle. Finally, it reports teaching experience from a 5 ECTS MSc course on automated reasoning, including student engagement, assessment structure (MiniCalc-based proofs and Isabelle/Isar work), and the role of formal verification in education.

Abstract

MiniCalc is a web app for teaching first-order logic based on a minimal sequent calculus. As an option the proofs can be verified in the Isabelle proof assistant. We present the lessons learned using the tool in recent years at our university.
Paper Structure (11 sections)

This paper contains 11 sections.

Table of Contents

  1. Introduction
  2. Minimal Sequent Calculus
  3. Step 1: Naming of Rules
  4. Step 2: Adding Datatypes and Functions
  5. Step 3: Adding Isabelle Notions and Notations
  6. Example Proofs
  7. A Trivial Example Proof in First-Order Logic
  8. The Default Example Proof in First-Order Logic
  9. Advanced Example Proofs in First-Order Logic
  10. Related Work
  11. Our Approach to Teaching and Lessons Learned