Crystal: Integrating Structured Queries into a Tactic Language

被引：1
|
作者：
Dietrich, Dominik [1 ]
Schulz, Ewaryst [1 ]
机构：
[1] DFKI Labor Bremen, D-28359 Bremen, Germany
来源：
JOURNAL OF AUTOMATED REASONING | 2010年 / 44卷 / 1-2期
关键词：
Tactic language; Query language; Proof search; Proof planning; Mathematical knowledge;
D O I：
10.1007/s10817-009-9138-5
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
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 Omega 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.
引用
收藏
页码：79 / 110
页数：32
相关论文
共 50 条
  • [1] Crystal: Integrating Structured Queries into a Tactic Language
    Dominik Dietrich
    Ewaryst Schulz
    [J]. Journal of Automated Reasoning, 2010, 44
  • [2] Explaining Structured Queries in Natural Language
    Koutrika, Georgia
    Simitsis, Alkis
    Ioannidis, Yannis E.
    [J]. 26TH INTERNATIONAL CONFERENCE ON DATA ENGINEERING ICDE 2010, 2010, : 333 - 344
  • [3] Translation of natural language queries to structured data sources
    Posevkin, Ruslan
    Bessmertny, Igor
    [J]. 2015 9TH INTERNATIONAL CONFERENCE ON APPLICATION OF INFORMATION AND COMMUNICATION TECHNOLOGIES (AICT), 2015, : 57 - 59
  • [4] SKDQL: A structured language to specify knowledge discovery processes and queries
    Silva, MPD
    Robin, J
    [J]. ADVANCES IN ARTIFICIAL INTELLIGENCE - SBIA 2004, 2004, 3171 : 326 - 335
  • [5] Searching cross-language metadata with automatically structured queries
    Peinado, V
    López-Ostenero, F
    Gonzalo, J
    Verdejo, F
    [J]. RESEARCH AND ADVANCED TECHNOLOGY FOR DIGITAL LIBRARIES, 2005, 3652 : 529 - 530
  • [6] Structured queries, language modeling, and relevance modeling in cross-language information retrieval
    Larkey, LS
    Connell, ME
    [J]. INFORMATION PROCESSING & MANAGEMENT, 2005, 41 (03) : 457 - 473
  • [7] A tactic language for hiproofs
    Aspinall, David
    Denney, Ewen
    Lueth, Christoph
    [J]. INTELLIGENT COMPUTER MATHEMATICS, PROCEEDINGS, 2008, 5144 : 339 - +
  • [8] A tactic language for ergo
    Martin, A
    Nickson, R
    Utting, M
    [J]. FORMAL METHODS PACIFIC '97, 1997, : 186 - 207
  • [9] Learning to generate structured queries from natural language with indirect supervision
    Bai, Ziwei
    Yu, Bo
    Wu, Bowen
    Wang, Zhuoran
    Wang, Baoxun
    [J]. COMPUTER SPEECH AND LANGUAGE, 2021, 67
  • [10] Knowledge Rich Natural Language Queries over Structured Biological Databases
    Jamil, Hasan M.
    [J]. ACM-BCB' 2017: PROCEEDINGS OF THE 8TH ACM INTERNATIONAL CONFERENCE ON BIOINFORMATICS, COMPUTATIONAL BIOLOGY,AND HEALTH INFORMATICS, 2017, : 352 - 361
12345