| In this dissertation, we exhibit work revolving around the FOLDN metalogic. After going over some of the background material on FOLDN, we discuss work about induction, and give induction principles that are richer than mathematical induction, in that they yield shorter, simpler and more elegant proofs. We then define and study notions of entailment and equivalence between two FOLDN definitions. We make use of these notions by defining a framework, closely related to FOLDN, for performing program transformation on definitions, and proving it correct. Finally, we discuss implementations in LambdaProlog of Iris, a theorem prover based on FOLDN, and of a program transformation tool based on the framework we built. |
