Theo: An interactive proof development system

DOI10.1007/BF01995105MaRDI QIDQ688727zbMATH OpenOpenAlexFDO

Authors J. 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

proof theorytheorem provingsymbolic computationlogics 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)

Recommendations

• SETHEO: A high-performance theorem prover
• TPS: A hybrid automatic-interactive system for developing proofs
• The Theorema Environment for Interactive Proof Development
• scientific article; zbMATH DE number 4072441
• Tactic theorem proving with refinement-tree proofs and metavariables

Cites work

• scientific article; zbMATH DE number 4035108 (Why is no real title available?)
• scientific article; zbMATH DE number 4053062 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• A framework for defining logics
• Logic and Computation
• Simple consequence relations
• The foundation of a generic theorem prover
• Using typed lambda calculus to implement formal systems on a machine

Cited in

(7)

• Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
• The Theorema Environment for Interactive Proof Development
• Encoding natural semantics in Coq
• The Abella Interactive Theorem Prover (System Description)
• Theorema 2.0: A System for Mathematical Theory Exploration
• \textit{Mollusc}: a general proof-development shell for sequent-based logics
• Collaborative Interactive Theorem Proving with Clide

Describes a project that uses

Uses Software

• Nuprl
• Cambridge LCF

This page was built for publication: Theo: An interactive proof development system

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q688727)