Towards Ludics Programming: Interactive Proof Search

被引：4
|
作者：
Saurin, Alexis [1 ]
机构：
[1] INRIA Saclay Ile de France, Saclay, France
来源：
LOGIC PROGRAMMING, PROCEEDINGS | 2008年 / 5366卷
关键词：
Ludics; Game Semantics; Logic Programming; Proof Search; Interaction; Proof Normalization;
D O I：
10.1007/978-3-540-89982-2_27
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Girard [1] introduced Ludics, as all interactive theory aiming at overcoming the distinction between syntax bind semantics in logic. In this paper, we investigate how ludics could serve as a foundation for logic programming, providing it mechanism for interactive proof search, that is proof search by interaction (or proof search by cut-elimination).
引用
收藏
页码：253 / 268
页数：16
相关论文
共 50 条
  • [31] Improved Assistance for Interactive Proof
    Kaliszyk, Cezary
    PROCEEDINGS OF THE 12TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2023, 2023, : 2 - 2
  • [32] STRATEGIES AND TECHNIQUES FOR INTERACTIVE PROOF
    HONDA, M
    NAKAJIMA, R
    LECTURE NOTES IN COMPUTER SCIENCE, 1983, 160 : 48 - 60
  • [33] A THEORY OF INTERACTIVE PROGRAMMING
    GERGELY, T
    URY, L
    ACTA INFORMATICA, 1982, 17 (01) : 1 - 20
  • [34] Interactive Proof Presentations with Cobra
    Ring, Martin
    Lueth, Christoph
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (239): : 43 - 52
  • [35] BaffleText: a human interactive proof
    Chew, M
    Baird, HS
    DOCUMENT RECOGNITION AND RETRIEVAL X, 2003, 5010 : 305 - 316
  • [36] INTERACTIVE COMPROMISE PROGRAMMING
    EVREN, R
    JOURNAL OF THE OPERATIONAL RESEARCH SOCIETY, 1987, 38 (02) : 163 - 172
  • [37] Expressiveness plus automation plus soundness: Towards combining SMT solvers and interactive proof assistants
    Fontaine, Pascal
    Marion, Jean-Yves
    Merz, Stephan
    Nieto, Leonor Prensa
    Tiu, Alwen
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2006, 3920 : 167 - 181
  • [38] Proof checking and logic programming
    Miller, Dale
    PROCEEDINGS OF THE 17TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING (PPDP 2015), 2015, : 18 - 18
  • [39] Proof Checking and Logic Programming
    Miller, Dale
    LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2015), 2015, 9527 : 3 - 17
  • [40] Proof checking and logic programming
    Miller, Dale
    FORMAL ASPECTS OF COMPUTING, 2017, 29 (03) : 383 - 399
12345