[Top] | [Contents] | [Index] | [ ? ] |

1. Introduction

2. How to Run TutchAbout this document

2.1 Explicitely Specification of Path3. Proofs in Propositional Logic

2.2 Setting Your Global Path

2.3 Creating Intermediate Scripts

3.1 Propositional Logic I4. Proof Terms for Propositional Logic

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

5. Types and Programs

6. First-Order Logic

7. Arithmetic

7.1 Proof terms8. Structural Induction

8.1 Proof termsA. Reference

A.1 Command Line SyntaxB. Emacs Quickstart

A.2 Tutch File Syntax

A.2.1 Proof TermsA.3 Requirements File Syntax

A.2.2 Types and Programs

A.2.3 First-Order Logic

A.2.4 Arithmetic

A.2.4.1 Proof TermsA.2.5 Structural Induction

A.2.6 Summary

A.4 Proof Checking

A.4.1 Proof Terms

B.1 Starting Emacs, File Commands

B.2 Editing Commands

B.2.1 Find and ReplaceB.3 Editing Several Files

B.2.2 Indentation

B.4 Modes and Customization

B.5 More Editing Commands

This document was generated by