Theo: An interactive proof development system
type: Item
instance of: scholarly article
title: Theo: An interactive proof development system
zbMATH Open document ID: 0784.68074
DOI: 10.1007/BF01995105
author: J. Despeyroux
published in: BIT
publication date: 1993-11-28T00:00:00Z
review text: The paper presents the main features of THEO, the first Typol version of a new tactic driven theorem prover which aims to help the user in building appropriate proofs in an object logic by proving theorems or derived rules in a backward way using resolution rule. The whole formalism used here, is essentially based on Gentzen sequent system. The resolution rule is expressed as a pair of Typol rules which describe the proof step when an inference rule is applied to the currently processed sequent. The basic implemented tactics, all of them being valid tactics, allow the user to add any number of previous derived rules and to ask for application of a particular instantiation of an object inference rule. Some editing manipulations as cut and paste transform can be applied to the derived proofs. The execution of the program can be controlled using the debugging facilities offered by Typol. Some examples of object logics which are already implemented under the described system are presented in the final part of the paper. A series of comments about some related work and conclusion remarks are formulated here too.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T35
zbMATH DE Number: 438465
zbMATH Keywords: logics and meaning of programs
zbMATH Keywords: symbolic computation
zbMATH Keywords: theorem proving
zbMATH Keywords: proof theory
zbMATH Keywords: tactic driven theorem prover
reviewed by: Luminita State
describes a project that uses: Nuprl
describes a project that uses: Cambridge LCF
MaRDI profile type: Publication
cites work: Simple consequence relations
cites work: Using typed lambda calculus to implement formal systems on a machine
cites work: Q3789101
cites work: Q5610986
cites work: A framework for defining logics
cites work: Q3774923
cites work: Logic and Computation
cites work: The foundation of a generic theorem prover
cites work: Q5559220
cites work: Q5632554
full work available at URL: https://doi.org/10.1007/bf01995105
OpenAlex ID: W1970894287
description: scientific article; zbMATH DE number 438465