Table of Contents

1. Introduction

About this document

2. How to Run Tutch

2.1 Explicitely Specification of Path
2.2 Setting Your Global Path
2.3 Creating Intermediate Scripts

3. Proofs in Propositional Logic

3.1 Propositional Logic I
3.2 Propositional Logic II
3.3 Propositional Logic III
3.4 Propositional Logic IV
3.5 Requirements and Submission

3.5.1 Getting the requirements
3.5.2 Completing the proofs
3.5.3 Checking against the requirements
3.5.4 Submitting
3.5.5 Checking status of submission

4. Proof Terms for Propositional Logic
5. Types and Programs
6. First-Order Logic
7. Arithmetic

7.1 Proof terms

8. Structural Induction

8.1 Proof terms

A. Reference

A.1 Command Line Syntax
A.2 Tutch File Syntax

A.2.1 Proof Terms
A.2.2 Types and Programs
A.2.3 First-Order Logic
A.2.4 Arithmetic

A.2.4.1 Proof Terms

A.2.5 Structural Induction
A.2.6 Summary

A.3 Requirements File Syntax
A.4 Proof Checking

A.4.1 Proof Terms

B. Emacs Quickstart

B.1 Starting Emacs, File Commands
B.2 Editing Commands

B.2.1 Find and Replace
B.2.2 Indentation

B.3 Editing Several Files
B.4 Modes and Customization
B.5 More Editing Commands