×

zbMATH — the first resource for mathematics

Ergo 6: a generic proof engine that uses Prolog proof technology. (English) Zbl 1068.68683
Summary: To support formal reasoning in mathematical and software engineering applications, it is desirable to have a generic prover that can be instantiated with a range of logics. This allows the prover to be applied to a wider variety of reasoning tasks than a fixed-logic prover. This paper describes the design principles and the architecture of the latest version of the Ergo proof engine, Ergo 6. Ergo 6 is a generic interactive theorem prover, similar to Isabelle, but with better support for proving schematic theorems with user-defined constraints, and with a different approach to handling variable scoping. A major theme of the paper is that Prolog implementation technology can be generalized to obtain efficient implementations of generic proof engines. This is demonstrated via a Qu-Prolog implementation of Ergo 6.
MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68N17 Logic programming
PDF BibTeX XML Cite
Full Text: DOI Link
References:
[1] DOI: 10.1016/B978-044450813-3/50019-9 · doi:10.1016/B978-044450813-3/50019-9
[2] DOI: 10.1093/logcom/3.1.47 · Zbl 0779.68078 · doi:10.1093/logcom/3.1.47
[3] Jones, a formal development support system (1991) · doi:10.1007/978-1-4471-3180-9
[4] van Hentenryck, Constraint satisfaction in logic programming (1989)
[5] Hamilton, ’Interpretation and instantiation of theories for reasoning about formal specifications’ pp 37–
[6] Gordon, Introduction to HOL: a theorem-proving environment for higher-order logic (1993) · Zbl 0779.68007
[7] Gentzen, The collected papers of Gerhard Gentzen pp 68– · Zbl 0209.30001
[8] Dijkstra, A discipline of programming (1976) · Zbl 0368.68005
[9] Deransart, Prolog: the standard reference manual · Zbl 0844.68017
[10] Boyer, A computational logic (1979)
[11] Bornat, ’Jape: A calculator for animating proof-on-paper’ pp 412– (1997)
[12] Utting, Austral. Comput. Sci. Comm pp 137– (1996)
[13] DOI: 10.1007/BF00248324 · Zbl 0679.68173 · doi:10.1007/BF00248324
[14] DOI: 10.1017/CBO9780511526602 · Zbl 0645.68041 · doi:10.1017/CBO9780511526602
[15] DOI: 10.1016/0743-1066(86)90015-4 · Zbl 0613.68035 · doi:10.1016/0743-1066(86)90015-4
[16] DOI: 10.1109/32.345827 · Zbl 05113371 · doi:10.1109/32.345827
[17] DOI: 10.1016/S0304-3975(96)00115-6 · Zbl 0874.68134 · doi:10.1016/S0304-3975(96)00115-6
[18] Martin, ’A tactic language for Ergo’ pp 186– (1997) · Zbl 0886.68124
[19] DOI: 10.1007/BF01213535 · Zbl 0857.68094 · doi:10.1007/BF01213535
[20] Kanger, Computer programming and formal systems pp 89– · Zbl 0265.02020
[21] DOI: 10.1007/BF01384236 · Zbl 0814.68088 · doi:10.1007/BF01384236
[22] DOI: 10.1007/BF00297245 · Zbl 0662.68104 · doi:10.1007/BF00297245
[23] Staples, Meta- programming in logic programming pp 435– (1989)
[24] Rushby, The World Congress in Formal Methods, Toulouse, France pp 48– (1999)
[25] Roy, J. Logic Programming pp 385–
[26] Paulson, Isabelle: a generic theorem prover 828 (1994) · Zbl 0825.68059 · doi:10.1007/BFb0030541
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.