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 条
  • [41] Towards a computational proof of Vizing's conjecture using semidefinite programming and sums-of-squares *,**
    Gaar, Elisabeth
    Krenn, Daniel
    Margulies, Susan
    Wiegele, Angelika
    JOURNAL OF SYMBOLIC COMPUTATION, 2021, 107 : 67 - 105
  • [42] Memorizable interactive proof and zero-knowledge proof systems
    Chen, N
    Rong, JW
    JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2004, 19 (06) : 936 - 941
  • [43] Memorizable interactive proof and zero-knowledge proof systems
    Ning Chen
    Jia-Wei Rong
    Journal of Computer Science and Technology, 2004, 19 : 936 - 941
  • [44] Proof Mate: An Interactive Proof Helper for PVS (Tool Paper)
    Masci, Paolo
    Dutle, Aaron
    NASA FORMAL METHODS (NFM 2022), 2022, 13260 : 809 - 815
  • [45] Interactive Graph Search
    Tao, Yufei
    Li, Yuanbing
    Li, Guoliang
    SIGMOD '19: PROCEEDINGS OF THE 2019 INTERNATIONAL CONFERENCE ON MANAGEMENT OF DATA, 2019, : 1393 - 1410
  • [46] 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
  • [47] Interactive Video Search
    Schoeffmann, Klaus
    Hopfgartner, Frank
    MM'15: PROCEEDINGS OF THE 2015 ACM MULTIMEDIA CONFERENCE, 2015, : 1321 - 1322
  • [48] Proof search and proof check for equational and inductive theorems
    Deplagne, E
    Kirchner, C
    Kirchner, H
    Nguyen, QH
    AUTOMATED DEDUCTION - CADE-19, PROCEEDINGS, 2003, 2741 : 297 - 316
  • [49] ProofViz: An Interactive Visual Proof Explorer
    Melcer, Daniel
    Chang, Stephen
    TRENDS IN FUNCTIONAL PROGRAMMING (TFP 2021), 2021, 12834 : 116 - 135
  • [50] IMPS - AN INTERACTIVE MATHEMATICAL PROOF SYSTEM
    FARMER, WM
    GUTTMAN, JD
    THAYER, FJ
    JOURNAL OF AUTOMATED REASONING, 1993, 11 (02) : 213 - 248
12345