A tactic language for Ergo

MaRDI QIDQ4370265zbMATH OpenFDO

Authors A. Martin, Ray Nickson, Mark Utting

Publication date 2 February 1998

zbMATH Keywords

AngelErgo theorem prover

Mathematics Subject Classification ID

Recommendations

• A tactic calculus. --- Abridged version
• A tactic language for the system Coq
• A Proof-Theoretic Approach to Tactics
• Mechanised support for sound refinement tactics
• scientific article; zbMATH DE number 2177623

Cited in

(8)

• A tactic calculus. --- Abridged version
• Crystal: Integrating structured queries into a tactic language
• A tactic language for the system Coq
• scientific article; zbMATH DE number 549074 (Why is no real title available?)
• Mechanised support for sound refinement tactics
• Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
• A tactic language for refinement of state-rich concurrent specifications
• A tactic language for declarative proofs

Describes a project that uses

Uses Software

• Qu-Prolog
• Ergo 6

This page was built for publication: A tactic language for Ergo

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