id: 05662163
dt: j
an: 05662163
au: Dietrich, Dominik; Schulz, Ewaryst
ti: Crystal: Integrating structured queries into a tactic language.
so: J. Autom. Reasoning 44, No. 1-2, 79-110 (2010).
py: 2010
pu: Springer, Dordrecht
la: EN
cc: 
ut: tactic language; query language; proof search; proof planning; mathematical
    knowledge
ci: 
li: doi:10.1007/s10817-009-9138-5
ab: 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 $Ω$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.
rv: