Towards Ludics Programming: Interactive Proof Search

被引:4
|
作者
Saurin, Alexis [1 ]
机构
[1] INRIA Saclay Ile de France, Saclay, France
来源
关键词
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 条
  • [1] Interactive observability in Ludics
    Faggian, C
    AUTOMATA , LANGUAGES AND PROGRAMMING, PROCEEDINGS, 2004, 3142 : 506 - 518
  • [2] Interactive observability in Ludics: The geometry of tests
    Faggian, C
    THEORETICAL COMPUTER SCIENCE, 2006, 350 (2-3) : 213 - 233
  • [3] Interactive proof-search for equational reasoning
    Miranda-Perea, Favio E.
    Gonzalez Huesca, Lourdes del Carmen
    Selene Linares-Arevalo, P.
    LOGIC JOURNAL OF THE IGPL, 2020, 28 (06) : 1155 - 1181
  • [4] LUDICS WITH REPETITIONS (EXPONENTIALS, INTERACTIVE TYPES AND COMPLETENESS)
    Basaldella, Michele
    Faggian, Claudia
    LOGICAL METHODS IN COMPUTER SCIENCE, 2011, 7 (02)
  • [5] Ludics with repetitions (Exponentials, Interactive types and Completeness)
    Basaldella, Michele
    Faggian, Claudia
    24TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2009, : 375 - +
  • [6] Genetic Programming Proof Search Automatic Improvement
    Kocsis, Zoltan A.
    Swan, Jerry
    JOURNAL OF AUTOMATED REASONING, 2018, 60 (02) : 157 - 176
  • [7] On Interactive Proof-Search for Constructive Modal Necessity
    Miranda-Perea, Favio E.
    Gonzalez Huesca, Lourdes del Carmen
    Selene Linares-Arevalo, P.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2020, 354 (354) : 107 - 127
  • [8] Implementation of proof search in the imperative programming language pizza
    Urban, C
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 1998, 1397 : 313 - 319
  • [9] Auto in Agda Programming Proof Search Using Reflection
    Kokke, Pepijn
    Swierstra, Wouter
    MATHEMATICS OF PROGRAM CONSTRUCTION, MPC 2015, 2015, 9129 : 276 - 301
  • [10] Towards Interactive Object-Oriented Programming
    Kwon, Keehang
    Park, Kyunghwan
    Park, Mi-Young
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2015, E98D (02): : 437 - 438