MINLOG REFERENCE MANUAL
Date
: January 17, 2007.
Contents
Acknowledgements
1.
Introduction
1.1.
Simultaneous free algebras
1.2.
Partial continuous functionals
1.3.
Primitive recursion, computable functionals
1.4.
Decidable predicates, axioms for predicates
1.5.
Minimal logic, proof transformation
1.6.
Comparison with Coq and Isabelle
2.
Types, with simultaneous free algebras as base types
2.1.
Generalitites for substitutions, type substitutions
2.2.
Simultaneous free algebras as base types
3.
Variables
4.
Constants
4.1.
Rewrite and computation rules for program constants
4.2.
Recursion over simultaneous free algebras
4.3.
Internal representation of constants
5.
Predicate variables and constants
5.1.
Predicate variables
5.2.
Predicate constants
5.3.
Inductively defined predicate constants
6.
Terms and objects
6.1.
Normalization
6.2.
Substitution
7.
Formulas and comprehension terms
8.
Assumption variables and constants
8.1.
Assumption variables
8.2.
Axiom constants
8.3.
Theorems
8.4.
Global assumptions
9.
Proofs
9.1.
Constructors and accessors
9.2.
Normalization
9.3.
Substitution
9.4.
Display
9.5.
Classical logic
10.
Interactive theorem proving with partial proofs
10.1.
Partial proofs
10.2.
Interactive theorem proving
11.
Search
12.
Computational content of classical proofs
13.
Extracted terms
14.
Reading formulas in external form
14.1.
Lexical analysis
14.2.
Parsing
References
Index