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 :
Rapport
[Research Report] RR-0887, INRIA. 1988, pp.11
Liste complète des métadonnées

https://hal.inria.fr/inria-00075667
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 18:46:23
Dernière modification le : samedi 27 janvier 2018 - 01:31:02
Document(s) archivé(s) le : vendredi 13 mai 2011 - 14:09:10

Fichiers

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

162

Téléchargements de fichiers

62