{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T10:32:50Z","timestamp":1648981970184},"reference-count":30,"publisher":"Wiley","license":[{"start":{"date-parts":[[2010,2,1]],"date-time":"2010-02-01T00:00:00Z","timestamp":1264982400000},"content-version":"unspecified","delay-in-days":2953,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["LMS J. Comput. Math."],"published-print":{"date-parts":[[2002]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>To support formal reasoning in mathematical and software engineering applications, it is desirable to have a <jats:italic>generic<\/jats:italic> 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.<\/jats:p>","DOI":"10.1112\/s1461157000000759","type":"journal-article","created":{"date-parts":[[2013,8,6]],"date-time":"2013-08-06T07:42:12Z","timestamp":1375774932000},"page":"194-219","source":"Crossref","is-referenced-by-count":2,"title":["Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology"],"prefix":"10.1112","volume":"5","author":[{"given":"Mark","family":"Utting","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Robinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ray","family":"Nickson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2010,2,1]]},"reference":[{"key":"S1461157000000759_ref030","first-page":"137","article-title":"\u2018Theory structuring in Ergo 4.1\u2019","author":"Utting","year":"1996","journal-title":"Austral. Comput. Sci. Comm"},{"key":"S1461157000000759_ref028","doi-asserted-by":"publisher","DOI":"10.1007\/BF00297245"},{"key":"S1461157000000759_ref025","first-page":"48","volume-title":"The World Congress in Formal Methods, Toulouse, France","author":"Rushby","year":"1999"},{"key":"S1461157000000759_ref024","first-page":"385","article-title":"\u20181983\u20131993: The wonder years of sequential PROLOG implementation\u2019","author":"Roy","journal-title":"J. Logic Programming"},{"key":"S1461157000000759_ref023","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/3.1.47"},{"key":"S1461157000000759_ref020","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541"},{"key":"S1461157000000759_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/BF00248324"},{"key":"S1461157000000759_ref022","unstructured":"22 Robinson Peter , \u2018Qu-Prolog 6.0 user guide\u2019, Tech. Rep. 00-20, Software Verification Research Centre, School of Information Technology, The University of Queensland,Brisbane 4072, Australia, (2000); http:\/\/svrc.it.uq.edu.au\/Bibliography\/svrc-tr.html?00-20."},{"key":"S1461157000000759_ref018","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526602"},{"key":"S1461157000000759_ref016","doi-asserted-by":"publisher","DOI":"10.1109\/32.345827"},{"key":"S1461157000000759_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/BF01213535"},{"key":"S1461157000000759_ref012","unstructured":"12 Kaufmann Matt and Moore J. Strother , \u2018Design goals for ACL2\u2019, CLI Technical Report 101, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, Texas 78703\u20134776, August 1994."},{"key":"S1461157000000759_ref007","first-page":"37","volume-title":"\u2018Interpretation and instantiation of theories for reasoning about formal specifications\u2019","author":"Hamilton"},{"key":"S1461157000000759_ref003","author":"Deransart","journal-title":"Prolog: the standard reference manual"},{"key":"S1461157000000759_ref014","first-page":"186","volume-title":"\u2018A tactic language for Ergo\u2019","author":"Martin","year":"1997"},{"key":"S1461157000000759_ref017","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(86)90015-4"},{"key":"S1461157000000759_ref011","first-page":"89","article-title":"A simplified proof method for elementary logic","author":"Kanger","journal-title":"Computer programming and formal systems"},{"key":"S1461157000000759_ref029","unstructured":"29 Utting Mark and Reeves Steve , \u2018Implementing cc substitutions in Ergo\u2019,\u2018WESTAPP 2000: The Third International Workshop on Explicit Substitutions: The ory and Applications to Programs and Proofs, Norwich, UK\u2019, preprint, 2000, 35\u201349; available from http:\/\/www.cs.waikato.ac.nz\/~marku."},{"key":"S1461157000000759_ref026","first-page":"435","volume-title":"Meta- programming in logic programming","author":"Staples","year":"1989"},{"key":"S1461157000000759_ref006","volume-title":"Introduction to HOL: a theorem-proving environment for higher-order logic","author":"Gordon","year":"1993"},{"key":"S1461157000000759_ref002","volume-title":"A computational logic","author":"Boyer","year":"1979"},{"key":"S1461157000000759_ref004","volume-title":"A discipline of programming","author":"Dijkstra","year":"1976"},{"key":"S1461157000000759_ref015","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00115-6"},{"key":"S1461157000000759_ref001","first-page":"412","volume-title":"\u2018Jape: A calculator for animating proof-on-paper\u2018","author":"Bornat","year":"1997"},{"key":"S1461157000000759_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384236"},{"key":"S1461157000000759_ref008","volume-title":"Constraint satisfaction in logic programming","author":"van Hentenryck","year":"1989"},{"key":"S1461157000000759_ref005","first-page":"68","volume-title":"The collected papers of Gerhard Gentzen","author":"Gentzen"},{"key":"S1461157000000759_ref021","volume-title":"Handbook of automated reasoning","volume":"2","author":"Pfenning","year":"2001"},{"key":"S1461157000000759_ref027","unstructured":"27 Staples Mark , \u2018Window inference in Isabelle\u2019, presented at the Isabelle Users\u2019 Workshop, 18\u201319 April 1995, University of Cambridge; available from http:\/\/www.cl.cam.ac.uk\/users\/lcp\/Workshop\/index.html."},{"key":"S1461157000000759_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3180-9"}],"container-title":["LMS Journal of Computation and Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1461157000000759","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T19:48:52Z","timestamp":1559936932000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1461157000000759\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"references-count":30,"alternative-id":["S1461157000000759"],"URL":"https:\/\/doi.org\/10.1112\/s1461157000000759","relation":{},"ISSN":["1461-1570"],"issn-type":[{"value":"1461-1570","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002]]}}}