Proof General

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.


References in zbMATH (referenced in 36 articles , 1 standard article )

Showing results 1 to 20 of 36.
Sorted by year (citations)

1 2 next

  1. Barras, Bruno; Tankink, Carst; Tassi, Enrico: Asynchronous processing of Coq documents: from the kernel up to the user interface (2015)
  2. Heras, Jónathan; Komendantskaya, Ekaterina: Recycling proof patterns in Coq: case studies (2014)
  3. Lüth, Christoph; Ring, Martin: A web interface for Isabelle: the next generation (2013)
  4. Armstrong, Alasdair; Foster, Simon; Struth, Georg: Dependently typed programming based on automated theorem proving (2012)
  5. Gast, Holger: Engineering the prover interface (2012)
  6. Jucovschi, Constantin: Cost-effective integration of MKM semantic services into editing environments (2012)
  7. Wenzel, Makarius: Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit (2012)
  8. Wenzel, Makarius: Isabelle/jEdit -- a prover IDE within the PIDE framework (2012)
  9. Wiedijk, Freek: A synthesis of the procedural and declarative styles of interactive theorem proving (2012)
  10. Wenzel, Makarius: Isabelle as document-oriented proof assistant (2011)
  11. Aspinall, David; Denney, Ewen; Lüth, Christoph: Tactics for hierarchical proof (2010)
  12. Butterfield, Andrew: Saoithín: a theorem prover for UTP (2010)
  13. Sewell, Peter; Nardelli, Francesco Zappa; Owens, Scott; Peskine, Gilles; Ridge, Thomas; Sarkar, Susmit; Strniša, Rok: Ott: effective tool support for the working semanticist (2010)
  14. Aspinall, David; Autexier, Serge; Lüth, Christoph; Wagner, Marc: Towards merging platomega and PGIP. (2009)
  15. Aspinall, David; Autexier, Serge; Lüth, Christoph; Wagner, Marc: Towards merging Plat$\Omega$ and PGIP (2009)
  16. Calude, Cristian S.; Müller, Christine: Formal proof: reconciling correctness and understanding (2009)
  17. Coen, Claudio Sacerdoti: A user interface for a mathematical system that allows ambiguous formulae. (2009)
  18. Gast, Holger: Managing proof documents for asynchronous processing. (2009)
  19. Gast, Holger: Managing proof documents for asynchronous processing (2009)
  20. Sacerdoti Coen, Claudio: A user interface for a mathematical system that allows ambiguous formulae (2009)

1 2 next


Further publications can be found at: http://proofgeneral.inf.ed.ac.uk/pubs