CRStL: A Declarative Language for the Encoding of Proof Techniques

Dominik Dietrich, Ewaryst Schulz

In: Workshop on Programming Languages for Mechanized Mathematics Systems. Conferences on Intelligent Computer Mathematics (CICM-08) July 29 Birmingham United Kingdom Seiten 16-28 2008.


We propose 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 very declarative way. We give examples to illustrate the use and semantics of CRStL.


paper.pdf (pdf, 99 KB )

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