Article

Proof General: A Generic Tool for Proof Development

Author:

TACAS '00: Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000

Pages 38 - 42

Published: 25 March 2000 Publication History

Abstract

This note describes Proof General, a tool for developing machine proofs with an interactive proof assistant. Interaction is based around a proof script, which is the target of a proof development. Proof General provides a powerful user-interface with relatively little effort, alleviating the need for a proof assistant to provide its own GUI, and providing a uniformap pearance for diverse proof assistants.

Proof General has a growing user base and is currently used for several interactive proof systems, including Coq, LEGO, and Isabelle. Support for others is on the way. Here we give a brief overview of what Proof General does and the philosophy behind it; technical details are available elsewhere. The program and user documentation are available on the web at http://www.dcs.ed.ac.uk/home/proofgen.

References

[1]

D. Aspinall, H. Goguen, T. Kleymann, and D. Sequira. Proof General. System documentation, see http://www.dcs.ed.ac.uk/home/proofgen, 1999.

Google Scholar

[2]

Yves Bertot, Thomas Kleymann, and Dilip Sequeira. Implementing proof by pointing without a structure editor. Technical Report ECS-LFCS-97-368, University of Edinburgh, 1997.

Google Scholar

[3]

Yves Bertot and Laurent ThÉry. A generic approach to building user interfaces for theoremp rovers. Journal of Symbolic Computation, 25(7):161-194, February 1998.

Crossref

Google Scholar

[4]

Markus Wenzel. Isar -- a generic interpretative approach to readable formal proof documents. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Lecture Notes in Computer Science 1690. Springer-Verlag, 1999.

Crossref

Google Scholar

Cited By

View all

Palmskog KCelik AGligoric MTip FBodden E(2018)piCoq: parallel regression proving for large-scale verification projectsProceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3213846.3213877(344-355)Online publication date: 12-Jul-2018
https://dl.acm.org/doi/10.1145/3213846.3213877
Czajka źKaliszyk C(2018)Hammer for CoqJournal of Automated Reasoning10.1007/s10817-018-9458-461:1-4(423-453)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10817-018-9458-4
Mateescu R(2018)Recent advances in interactive and automated analysisInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-017-0477-y20:2(119-123)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10009-017-0477-y
Show More Cited By

Index Terms

Proof General: A Generic Tool for Proof Development

Index terms have been assigned to the content through auto-classification.

Recommendations

Proof Pearl: a Formal Proof of Higman's Lemma in ACL2

Higman's lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. In this paper we present a formalization and proof of Higman's Lemma in the ACL2 theorem prover. Our formalization is based on a ...
Proof-checking metamathematics (theorem-proving)
Proving Isomorphism of First-Order Logic Proof Systems in HOL

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

March 2000

549 pages

ISBN:3540672826

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 25 March 2000

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

38
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Palmskog KCelik AGligoric MTip FBodden E(2018)piCoq: parallel regression proving for large-scale verification projectsProceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3213846.3213877(344-355)Online publication date: 12-Jul-2018
https://dl.acm.org/doi/10.1145/3213846.3213877
Czajka źKaliszyk C(2018)Hammer for CoqJournal of Automated Reasoning10.1007/s10817-018-9458-461:1-4(423-453)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10817-018-9458-4
Mateescu R(2018)Recent advances in interactive and automated analysisInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-017-0477-y20:2(119-123)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10009-017-0477-y
Faithfull ABengtson JTassi ETankink C(2018)CoqoonInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-017-0457-220:2(125-137)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10009-017-0457-2
Celik APalmskog KGligoric MRosu GDi Penta MNguyen T(2017)iCoq: regression proof selection for large-scale verification projectsProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering10.5555/3155562.3155588(171-182)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.5555/3155562.3155588
Christiansen DBrady E(2016)Elaborator reflection: extending Idris in IdrisACM SIGPLAN Notices10.1145/3022670.295193251:9(284-297)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/3022670.2951932
Christiansen DBrady EGarrigue JKeller GSumii E(2016)Elaborator reflection: extending Idris in IdrisProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming10.1145/2951913.2951932(284-297)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/2951913.2951932
Faithfull ABengtson JTassi ETankink C(2016)CoqoonProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 963610.1007/978-3-662-49674-9_18(316-331)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.1007/978-3-662-49674-9_18
Matichuk DMurray TAndronick JJeffery RKlein GStaples MBertolino ACanfora GElbaum S(2015)Empirical study towards a leading indicator for cost of formal software verificationProceedings of the 37th International Conference on Software Engineering - Volume 110.5555/2818754.2818842(722-732)Online publication date: 16-May-2015
https://dl.acm.org/doi/10.5555/2818754.2818842
Lüth CRing M(2013)A web interface for isabelleProceedings of the 2013 international conference on Intelligent Computer Mathematics10.1007/978-3-642-39320-4_22(326-329)Online publication date: 8-Jul-2013
https://dl.acm.org/doi/10.1007/978-3-642-39320-4_22
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations

Proof Pearl: a Formal Proof of Higman's Lemma in ACL2

Proof-checking metamathematics (theorem-proving)

Proving Isomorphism of First-Order Logic Proof Systems in HOL

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations