Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 6:46:23 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:33 AM
Long-term archiving on: : Friday, May 13, 2011 - 2:09:10 PM


  • HAL Id : inria-00075667, version 1



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



Record views


Files downloads