Theo: An interactive proof development system

DOI10.1007/BF01995105zbMATH Open0784.68074OpenAlexW1970894287MaRDI QIDQ688727FDOQ688727

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

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

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)

Cites Work

• Logic and Computation
• A framework for defining logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Simple consequence relations
• Title not available (Why is that?)
• The foundation of a generic theorem prover
• Using typed lambda calculus to implement formal systems on a machine
• Title not available (Why is that?)

Cited In (7)

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

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)