THEO : an interactive proof development system
Résumé
Theo is an interactive, tectic-driven, proof development system - a Theorem Prover. Both the meta and the objet levels of our theorem prover are logics presented in Typol. Typol is the programmind language that implements Natural Semantics - a semantics developed at Inria and poineered by G. Plotkin under the name Structural Operational Semantics. So Theo is written in Typol and helps the user to bult proofs in an objetc logic also written in Typol. Other important features od Theo are the form chosen for representing proofs, and the way proofs are performed. The internal form of the proofs is very compact form, expressed with combinators, that can be related to the calculus used in Automath and its descendants. Meanwhile, Theo performs proofs by a pure calculus on proofs, using a resolution rule. Proofs may be incomplete, and may contain logical variables. Theo is developed under the Centaur system, a well as Typol. This system provides a modern graphic man-machine interface that Theo uses, for the user's advantage. This is the reference and user's manual for Theo version 1.0 runing under Centaur version 1. 0
Théo est un système de développement de preuves - ou prouveur de Théorèmes - intéractif, dirigé par des tactiques. Les niveaux de meta et objet de notre prouveur de théorèmes sont tous deux des logiques présentés en Typol. Typol est le langage de programmation implémentant la Sémantique Naturelle - une sémantique développée à l'INRIA à partir de la Sémantique Operationnelle Structurelle de Gordon Plotkin. Donc Theo est écrit en Typol et aide l'utilisateur à construire des preuves dans des logiques objets également écrites en Typol. Les autres principales caractéristiques de Théo sont la forme choisie pour représenter les preuves, et la manière dont les preuves sont construites. La formeinternet des preuves en Théo est une forme très compacte. Elle utilise des combinateurs, et est très proche des lambda-calculs utilisés dans Automath et ses descendants. Théo, pourtant, construit les preuves en utilisant une règle de résolution. Les préuves peuvent être incomplètes, et contenir des variables. Théo, ainsi que Typol, sont développés sous le méta-compilateur Centaur. Centaur forunit une agréable interface homme machine graphique, que Théo utilise, à l'avantage de l'utilisateur. Ceci est le manuel utilisateur ainsi que le manuel de référence de Théo version 1.0 implémenté sous Centaur version 1.0