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
Complete list of metadatas

https://hal.inria.fr/inria-00075667
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 6:46:23 PM
Last modification on : Saturday, January 27, 2018 - 1:31:02 AM
Long-term archiving on : Friday, May 13, 2011 - 2:09:10 PM

Identifiers

  • HAL Id : inria-00075667, version 1

Collections

Citation

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

Share

Metrics

Record views

170

Files downloads

67