Crystal: Integrating Structured Queries into a Tactic Language

Dominik Dietrich, Ewaryst Schulz

In: Journal of Automated Reasoning (JAR) 43 3 Seiten 1-32 Springer 2009.


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.


Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence