\input zb-basic
\input zb-ioport
\iteman{io-port 05662163}
\itemau{Dietrich, Dominik; Schulz, Ewaryst}
\itemti{Crystal: Integrating structured queries into a tactic language.}
\itemso{J. Autom. Reasoning 44, No. 1-2, 79-110 (2010).}
\itemab
Summary: We present the language $\bold {CRStL}$ ($\bold C$ontrol $\bold R$ule $\bold {St}$rategy $\bold L$anguage, pronounce ``crystal'') to formulate mathematical reasoning techniques as proof strategies in the context of the proof assistant $\Omega $mega. 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 $\bold {CRStL}$ and illustrate its use by examples.
\itemrv{~}
\itemcc{}
\itemut{tactic language; query language; proof search; proof planning; mathematical knowledge}
\itemli{doi:10.1007/s10817-009-9138-5}
\end