Publication
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.
Abstract
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.