Crystal: Integrating Structured Queries into a Tactic Language |
| |
Authors: | Dominik Dietrich Ewaryst Schulz |
| |
Affiliation: | 1. DFKI-Labor Bremen, Safe and Secure Cognitive Systems, Enrique-Schmidt-Stra?e 5, 28359, Bremen, Germany
|
| |
Abstract: | We present the language CRStL (Control Rule Strategy Language, pronounce “crystal”) to formulate mathematical reasoning techniques as proof strategies in the context of the proof assistant Ωmega. 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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|