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 条
  • [1] A Resolution-Based Interactive Proof System for UNSAT
    Czerner, Philipp
    Esparza, Javier
    Krasotin, Valentin
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PT II, FOSSACS 2024, 2024, 14575 : 116 - 136
  • [2] Interactive Analysis using PROOF in a GRID Infrastructure
    Rodriguez Marrero, Ana Yaiza
    Gonzalez Caballero, Isidro
    Cuesta Noriega, Alberto
    Matorras Weinig, Francisco
    INTERNATIONAL CONFERENCE ON COMPUTING IN HIGH ENERGY AND NUCLEAR PHYSICS (CHEP 2010), 2011, 331
  • [3] Interactive Proof Assistant Based on Resolution Method in First Order Logic
    Bekiaris, Benjamin
    Perhac, Jan
    28TH INTERNATIONAL CONFERENCE ON INTELLIGENT ENGINEERING SYSTEMS, INES 2024, 2024, : 167 - 174
  • [4] A human interactive proof algorithm using handwriting recognition
    Rusu, A
    Govindaraju, V
    EIGHTH INTERNATIONAL CONFERENCE ON DOCUMENT ANALYSIS AND RECOGNITION, VOLS 1 AND 2, PROCEEDINGS, 2005, : 967 - 971
  • [5] Supporting interactive graph exploration using edge plucking
    Wong, Nelson
    Carpendale, Sheelagh
    VISUALIZATION AND DATA ANALYSIS 2007, 2007, 6495
  • [6] Interactive Proof Systems
    Goldreich, Oded
    FOUNDATIONS AND TRENDS IN THEORETICAL COMPUTER SCIENCE, 2007, 3 (01): : 1 - +
  • [7] Interactive Proof Critics
    Dept. of Comp. and Elec. Engineering, Heriot-Watt University, Edinburgh, United Kingdom
    不详
    不详
    不详
    Formal Aspects Comput, 3 (302-325):
  • [8] A framework for interactive proof
    Aspinall, David
    Lueth, Christoph
    Wintersteini, Daniel
    TOWARDS MECHANIZED MATHEMATICAL ASSISTANTS, 2007, 4573 : 161 - +
  • [9] An interactive approach for illustrating a proof of the sampling theorem using MATHEMATICA
    Guerrero, Fabio G.
    COMPUTER APPLICATIONS IN ENGINEERING EDUCATION, 2018, 26 (06) : 2282 - 2293
  • [10] Distributed parallel interactive data analysis using the proof system
    Brun, R
    Rademakers, F
    PROCEEDINGS OF CHEP 2001, 2001, : 704 - 707
12345