Publication
Crystal: Integrating Structured Queries into a Tactic Language
Dominik Dietrich; Ewaryst Schulz
In: Journal of Automated Reasoning (JAR), Vol. 43, No. 3, Pages 1-32, Springer, 2009.
Abstract
We present the language CRStL to formulate mathematical reasoning techniques as proof strategies
in the context of the proof assistant Omega. The language is arranged in two
levels, a query language to access mathematical knowledge maintained in development
graphs, and a strategy language to annotate the results of these queries with
further control information. The two-leveled structure of the language allows the
specification of proof techniques in a declarative way. We present the syntax and
semantics of CRStL and illustrate its use by examples.