Crystal: Integrating Structured Queries into a Tactic Language
We present the language CRStL (Control Rule Strategy Language, 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 CRStL and illustrate its use by examples.
tactic language query language mathematical knowledge proof search proof planning