×

Proof General

swMATH ID: 4901
Software Authors: Aspinall, David
Description: Proof General: A generic tool for proof development. 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 uniform appearance for diverse proof assistants. par 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.
Homepage: http://proofgeneral.inf.ed.ac.uk/
Related Software: Coq; Isabelle; Isabelle/HOL; Mizar; Isar; Isabelle/jEdit; Isabelle/Isar; Matita; HOL; Metis_; PVS; CtCoq; HOL Light; ACL2; Isabelle/PIDE; Haskell; Proof General Kit; VAMPIRE; Flyspeck; PIDE
Cited in: 52 Publications
Further Publications: http://proofgeneral.inf.ed.ac.uk/pubs

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Proof General: A generic tool for proof development. Zbl 0971.68627
Aspinall, David
2000
all top 5

Cited by 84 Authors

8 Wenzel, Makarius
5 Sacerdoti Coen, Claudio
5 Tassi, Enrico
4 Lüth, Christoph
4 Paulson, Lawrence Charles
3 Asperti, Andrea
3 Aspinall, David
3 Kaliszyk, Cezary
3 Nipkow, Tobias
3 Zacchiroli, Stefano
2 Benzmüller, Christoph Ewald
2 Ring, Martin
1 Abrial, Jean-Raymond
1 Armstrong, Alasdair
1 Autexier, Serge
1 Ballarin, Clemens
1 Barras, Bruno
1 Berardi, Stefano
1 Brady, Edwin C.
1 Brown, Chad Edward
1 Butterfield, Andrew
1 Calude, Cristian S.
1 Cansell, Dominique
1 Chlipala, Adam J.
1 Christiansen, David R.
1 Coppo, Mario
1 Czajka, Łukasz
1 Damanik, David
1 Damiani, Ferruccio
1 David, Rene
1 Delaware, Benjamin
1 Denney, Ewen
1 Dennis, Louise Abigail
1 Dietrich, Dominik
1 Dillinger, Peter C.
1 Dixon, Lucas
1 Ferreira, João Filipe
1 Fleuriot, Jacques D.
1 Foster, Simon
1 Gast, Holger
1 Gauthier, Thibault
1 Gesztesy, Fritz
1 Gross, Jason
1 Hansen, Helle Hvid
1 Heras, Jónathan
1 Hupel, Lars
1 Jucovschi, Constantin
1 Komendantskaya, Ekaterina
1 Kupke, Clemens
1 Kutsia, Temur
1 Manolios, Panagiotis
1 Mendes, Alexandra
1 Meng, Jia
1 Moore, J Strother
1 Müller, Christine
1 Owens, Scott
1 Pease, Adam
1 Peskine, Gilles
1 Piroi, Florina
1 Pit-Claudel, Clément
1 Quigley, Claire
1 Raffalli, Christophe
1 Ricciotti, Wilmer
1 Ridge, Thomas
1 Roe, Kenneth
1 Rutten, Jan J. M. M.
1 Sarkar, Susmit
1 Sewell, Peter
1 Strniša, Rok
1 Struth, Georg
1 Sutcliffe, Geoff
1 Tankink, Carst
1 Tews, Hendrik
1 Theiss, Frank
1 Urban, Josef
1 Vroon, Daron
1 Wagner, Marc Oliver
1 Wang, Peng
1 Wenzel, Markus
1 Wiedijk, Freek
1 Winterstein, Daniel
1 Yuditskii, Peter Meerovich
1 Zappa Nardelli, Francesco
1 Zinn, Claus
all top 5

Cited in 9 Serials

3 Journal of Applied Logic
3 Mathematics in Computer Science
2 Journal of Automated Reasoning
2 Lecture Notes in Computer Science
2 Logical Methods in Computer Science
1 Information and Computation
1 Formal Aspects of Computing
1 Journal of Functional Programming
1 Oberwolfach Reports
all top 5

Cited in 7 Fields

51 Computer science (68-XX)
10 Mathematical logic and foundations (03-XX)
2 General and overarching topics; collections (00-XX)
1 Partial differential equations (35-XX)
1 Dynamical systems and ergodic theory (37-XX)
1 Operator theory (47-XX)
1 Mathematics education (97-XX)

Citations by Year