THEO : an interactive proof development system

Joelle Despeyroux 1
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This paper presents the first version of a Typol interactive, tactic-driven, theorem prover called Theo. Theorem prover means here proof development system. Typol is the programming language that implements Natural Semantics -a semantics pioneered by G. Plotkin under the name Structural Operational Semantics- in the Centaur meta-compiler. Centaur provides a pleasant graphic man-machine interface that Theo can use, for the user's advantage. Both the meta and the object levels of our theorem prover are logics presented in Typol. In other words, Theo is written in Typol and proves theorems of an object logic also written in Typol. Other important features of Theo are the form chosen for representing proofs, and the way proofs are performed. The internal form of the proofs is a very compact form, expressed with combinators, that is closely related to the lambda-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 variables. The paper presents an implementation of the Calculus of Constructions of Thierry Coquand and Gérard Huet, as an example of an object logic for Theo. It also presents the -very few- tactics that have been implemented so far. Our representation of proofs is discussed and compared with other existing forms. Differences with other existing systems are discussed at length.
Type de document :
[Research Report] RR-0887, INRIA. 1988, pp.11
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 18:46:23
Dernière modification le : jeudi 11 janvier 2018 - 16:30:45
Document(s) archivé(s) le : vendredi 13 mai 2011 - 14:09:10



  • HAL Id : inria-00075667, version 1



Joelle Despeyroux. THEO : an interactive proof development system. [Research Report] RR-0887, INRIA. 1988, pp.11. 〈inria-00075667〉



Consultations de la notice


Téléchargements de fichiers