Experiments on supporting interactive proof using resolution

被引：0
|
作者：
Meng, J [1 ]
Paulson, LC [1 ]
机构：
[1] Univ Cambridge, Comp Lab, Cambridge CB3 0FD, England
来源：
AUTOMATED REASONING, PROCEEDINGS | 2004年 / 3097卷
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Interactive theorem provers can model complex systems, but require much effort to prove theorems. Resolution theorem provers are automatic and powerful, but they are designed to be used for very different applications. This paper reports a series of experiments designed to determine whether resolution can support interactive proof as it is currently done. In particular, we present a sound and. practical encoding in first-order logic of Isabelle's type classes.
引用
收藏
页码：372 / 384
页数：13
相关论文
共 50 条
  • [31] Proof Mate: An Interactive Proof Helper for PVS (Tool Paper)
    Masci, Paolo
    Dutle, Aaron
    NASA FORMAL METHODS (NFM 2022), 2022, 13260 : 809 - 815
  • [32] High-resolution neutron radiography with microchannel plates: Proof-of-principle experiments at PSI
    Tremsin, A. S.
    McPhate, J. B.
    Vallerga, J. V.
    Siegmund, O. H. W.
    Hull, J. S.
    Feller, W. B.
    Lehmann, E.
    NUCLEAR INSTRUMENTS & METHODS IN PHYSICS RESEARCH SECTION A-ACCELERATORS SPECTROMETERS DETECTORS AND ASSOCIATED EQUIPMENT, 2009, 605 (1-2): : 103 - 106
  • [33] An 'economics proof' of the supporting hyperplane theorem
    Weitzman, ML
    ECONOMICS LETTERS, 2000, 68 (01) : 1 - 6
  • [34] Supporting proof in a reactive development environment
    Mehta, Farhad
    SEFM 2007: FIFTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2007, : 103 - 112
  • [35] The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts
    Hentschel, Martin
    Haehnle, Reiner
    Bubel, Richard
    2016 31ST IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE), 2016, : 846 - 851
  • [36] Proof assistance for real-time systems using an interactive theorem prover
    Kolano, PZ
    THEORETICAL COMPUTER SCIENCE, 2002, 282 (01) : 53 - 99
  • [37] IFA PROOF OF PRINCIPLE EXPERIMENTS
    OLSON, CL
    IEEE TRANSACTIONS ON NUCLEAR SCIENCE, 1979, 26 (03) : 4231 - 4233
  • [38] ProofViz: An Interactive Visual Proof Explorer
    Melcer, Daniel
    Chang, Stephen
    TRENDS IN FUNCTIONAL PROGRAMMING (TFP 2021), 2021, 12834 : 116 - 135
  • [39] IMPS - AN INTERACTIVE MATHEMATICAL PROOF SYSTEM
    FARMER, WM
    GUTTMAN, JD
    THAYER, FJ
    JOURNAL OF AUTOMATED REASONING, 1993, 11 (02) : 213 - 248
  • [40] The Theorema environment for interactive proof development
    Piroi, F
    Kutsia, T
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 : 261 - 275
12345