Theo: An interactive proof development system

DOI10.1007/BF01995105zbMath0784.68074OpenAlexW1970894287MaRDI QIDQ688727

Joëlle Despeyroux

Publication date: 28 November 1993

Published in: BIT (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01995105

zbMATH Keywords

symbolic computationtheorem provingproof theorylogics and meaning of programstactic driven theorem prover

Mathematics Subject Classification ID

Theory of languages and software systems (knowledge-based systems, expert systems, etc.) for artificial intelligence (68T35) Mechanization of proofs and logical operations (03B35)

Related Items

Encoding natural semantics in Coq

Uses Software

• Nuprl
• Cambridge LCF

Cites Work

• Using typed lambda calculus to implement formal systems on a machine
• Simple consequence relations
• The foundation of a generic theorem prover
• Logic and Computation
• A framework for defining logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item