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

DOI10.1112/S1461157000000759zbMath1068.68683OpenAlexW2025919633MaRDI QIDQ4827602

No author found.

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

Uses Software

• Isabelle
• PVS
• Qu-Prolog
• Ergo 6

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Isabelle. A generic theorem prover
• Annotations in formal specifications and proofs
• The Qu-Prolog unification algorithm: formalisation and correctness
• A tactic calculus. --- Abridged version
• The foundation of a generic theorem prover
• Logic and Computation
• Formalizing a Hierarchical Structure of Practical Mathematical Reasoning
• Natural deduction as higher-order resolution
• Law and logic

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