A Tagged LCF-style Proof Architecture

Abstract

We describe the notion of tagged inference as it arises in LCF-style theorem proving systems. Adding tags considerably widens the applicability of such systems, while costing little. By way of introduction, we give a simple tagged implementation of a propositional logic. We also discuss how tagged inference is currently used in an industrial strength proof system. Some knowledge of ML is assumed.

paper