A tactic language for ergo

被引：0
|
作者：
Martin, A [1 ]
Nickson, R [1 ]
Utting, M [1 ]
机构：
[1] Univ Queensland, Sch Informat Technol, Software Verificat Res Ctr, Brisbane, Qld 4072, Australia
来源：
FORMAL METHODS PACIFIC '97 | 1997年
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
A new version of the Ergo theorem prover is under development. It uses a single tactic language, based on Angel, for tactic programming, user interface, and proof representation. This paper describes the language as it is used in each of these cases, and explains the details of its implementation in Qu-Prolog. An example from classical propositional calculus is included.
引用
收藏
页码：186 / 207
页数：22
相关论文
共 50 条
  • [1] A tactic language for hiproofs
    Aspinall, David
    Denney, Ewen
    Lueth, Christoph
    [J]. INTELLIGENT COMPUTER MATHEMATICS, PROCEEDINGS, 2008, 5144 : 339 - +
  • [2] ArcAngel: A tactic language for refinement
    Oliveira, Marcel
    Cavalcanti, Ana
    Woodcock, Jim
    [J]. Formal Aspects of Computing, 2003, 15 (01) : 28 - 47
  • [3] A Tactic Language for Declarative Proofs
    Autexier, Serge
    Dietrich, Dominik
    [J]. INTERACTIVE THEOREM PROVING, PROCEEDINGS, 2010, 6172 : 99 - 114
  • [4] A tactic language for the system Coq
    Delahaye, D
    [J]. LOGIC FOR PROGRAMMING AND AUTOMATED REASONING, PROCEEDINGS, 2000, 1955 : 85 - 95
  • [5] Incognito ergo sum - Language, memory and the subject
    Sayer, D
    [J]. THEORY CULTURE & SOCIETY, 2004, 21 (06) : 67 - +
  • [6] ArcAngelC: a Refinement Tactic Language for Circus
    Oliveira, M. V. M.
    Cavalcanti, A. L. C.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 214 (0C) : 203 - 229
  • [7] Crystal: Integrating Structured Queries into a Tactic Language
    Dominik Dietrich
    Ewaryst Schulz
    [J]. Journal of Automated Reasoning, 2010, 44
  • [8] Crystal: Integrating Structured Queries into a Tactic Language
    Dietrich, Dominik
    Schulz, Ewaryst
    [J]. JOURNAL OF AUTOMATED REASONING, 2010, 44 (1-2) : 79 - 110
  • [9] A tactic language for refinement of state-rich concurrent specifications
    Oliveira, Marcel
    Zeyda, Frank
    Cavalcanti, Ana
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2011, 76 (09) : 792 - 833
  • [10] ERGO IF NOT INERTIA
    Polaschegg, Nina
    [J]. NEUE ZEITSCHRIFT FUR MUSIK, 2012, (05): : 87 - 87
12345