A Tactic Language for Declarative Proofs

Serge Autexier; Dominik Dietrich

In: Matt Kaufmann; Lawrence C. Paulson (Hrsg.). Proceedings International Conference on Interactive Theorem Proving. International Conference on Interactive Theorem Proving (ITP-2010), July 11-14, Edinburgh, United Kingdom, Pages 99-114, Lecture Notes in Computer Sciences (LNCS), Vol. 6172, Springer, 7/2010.


Influenced by the success of the MIZAR system many declarative proof languages have been developed in the theorem prover community, as declarative proofs are more readable, easier to modify and to maintain than their procedural counterparts. However, despite their advantages, many users still prefer the procedural style of proof, because procedural proofs are faster to write. In this paper we show how to define a declarative tactic language on top of a declarative proof language. The language comes along with a rich facility to declaratively specify conditions on proof states in the form of sequent patterns, as well as ellipses (dot notation) to provide a limited form of iteration. As declarative tactics are specified using the declarative proof language, they offer the same advantages as declarative proof languages. At the same time, they also produce declarative justifications in the form of a declarative proof script and can thus be seen as an attempt to reduce the gap between procedural and declarative proofs.


Weitere Links

paper.pdf (pdf, 179 KB )

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