CONTENTS 2 Contents 1 Folderol: a simple theorem prover 3 1.1 Representation of rules .......................... 4 1.2 Propositional logic ............................ 5 1.3 Quantifiers and unification ........................ 7 1.4 Parameters in quantifier rules ...................... 7 2 Basic data structures and operations 10 2.1 Terms ................................... 10 2.2 Formulae .................................. 11 2.3 Abstraction and substitution ....................... 11 2.4 Parsing and printing ........................... 13 3 Unification 14 3.1 Examples ................................. 15 3.2 Parameter dependencies in unification .................. 16 3.3 The environment ............................. 17 3.4 The ML code for unification ....................... 17 3.5 Extensions and omissions ......................... 18 3.6 Instantiation by the environment .................... 19 4 Inference in Folderol 20 4.1 Solving a goal ............................... 21 4.