Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology

DOI10.1112/S1461157000000759MaRDI QIDQ4827602zbMATH OpenOpenAlexFDO

Authors

Publication date 18 November 2004

Published in LMS Journal of Computation and Mathematics (Search for Journal in Brave)

Full work available at URL http://www.lms.ac.uk/jcm/5/lms1999-032/

Mathematics Subject Classification ID

Logic programming (68N17)

Recommendations

• scientific article; zbMATH DE number 1629953
• scientific article; zbMATH DE number 1104384
• scientific article; zbMATH DE number 1543300
• An examination of the prolog technology theorem-prover
• scientific article; zbMATH DE number 3986671

Cites work

• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1104384 (Why is no real title available?)
• scientific article; zbMATH DE number 867332 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• A tactic calculus. --- Abridged version
• Annotations in formal specifications and proofs
• Formalizing a Hierarchical Structure of Practical Mathematical Reasoning
• Isabelle. A generic theorem prover
• Law and logic
• Logic and Computation
• Natural deduction as higher-order resolution
• The Qu-Prolog unification algorithm: formalisation and correctness
• The foundation of a generic theorem prover

Describes a project that uses

Uses Software

• Ergo 6
• Qu-Prolog
• PVS
• Isabelle

This page was built for publication: Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology

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