| A Two-Level Approach towards Lean Proof-Checking (1996) | |||||||||||||||
Abstract | |||||||||||||||
| . We present a simple and effective methodology for equational reasoning in proof checkers. The method is based on a two-level approach distinguishing between syntax and semantics of mathematical theories. The method is very general and can be carried out in any type system with inductive and oracle types. The potential of our two-level approach is illustrated by some examples developed in Lego. 1 Introduction The main actions in writing mathematics consist of defining, reasoning and computing (symbolically; this is also called `equational reasoning'). Whereas defining and reasoning are reasonably well captured by a interactive proof-developer, the formalisation of computations has caused problems. This paper studies the possibilities of a partial automation of equational reasoning, which is from the authors' experience, one of the most recurrent source of problems in formalising mathematics using a proof-developer [4, 25]. We describe several methods using elementary techniques from ... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||