Theo: An interactive proof development system (Q688727)

The paper presents the main features of THEO, the first Typol version of a new tactic driven theorem prover which aims to help the user in building appropriate proofs in an object logic by proving theorems or derived rules in a backward way using resolution rule. The whole formalism used here, is essentially based on Gentzen sequent system. The resolution rule is expressed as a pair of Typol rules which describe the proof step when an inference rule is applied to the currently processed sequent. The basic implemented tactics, all of them being valid tactics, allow the user to add any number of previous derived rules and to ask for application of a particular instantiation of an object inference rule. Some editing manipulations as cut and paste transform can be applied to the derived proofs. The execution of the program can be controlled using the debugging facilities offered by Typol. Some examples of object logics which are already implemented under the described system are presented in the final part of the paper. A series of comments about some related work and conclusion remarks are formulated here too.