Publikation
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.
Zusammenfassung
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.