Skip to main content Skip to main navigation

Publikation

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, Pages 16-28, 2008.

Zusammenfassung

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.

Projekte