05662163

j

05662163 Dietrich, Dominik Schulz, Ewaryst Crystal: Integrating structured queries into a tactic language. J. Autom. Reasoning 44, No. 1-2, 79-110 (2010). 2010 Springer, Dordrecht EN tactic language query language proof search proof planning mathematical knowledge

doi:10.1007/s10817-009-9138-5

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.