A programmable interactive automated deduction system for propositional logic
James David Shelley · 1987
A special-purpose language and interpreter for that language were created to facilitate the development of interactive automated propositional logic theorem proving systems. The language was designed so that concentration can be focussed on the definition of inference rules and development of proving strategies without concern for computer programming intricacies. The language syntax includes features for defining and manipulating syntactic structures commonly encountered in standard propositional logic systems. The interpreter provides a proof construction environment that performs the mechanical functions of automated deduction and implements the defined logic system and its associated proving strategies.