Proof General in Eclipse

David Aspinall, Christoph Lüth, Daniel Winterstein, Ahsan Fayyaz

In: Eclipse Technology eXchange ETX'06. Eclipse Technology Exchange Workshop (ETX-06) ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications befindet sich OOPSLA 2006 October 22-26 Portland OR United States ACM Press 2006.


Interactive theorem proving is the art of constructing electronic proofs. Proof development, based around a proof script, has much in common with program development, based around a program text. Proof developers use rather primitive tools for developing and manipulating proof scripts at present. The Proof General project aims at to change this, by providing powerful generic tools and interfaces. The flagship tool is our Eclipse plugin, which brings the features of a industrial-strength IDE to theorem proving for the first time. In this paper we give an overview of the Eclipse plugin and its underlying architecture.

etx06.pdf (pdf, 611 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence