Publikation

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.

Abstrakt

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.

Projekte

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