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 条
  • [21] A framework for interactive proof
    Aspinall, David
    Lueth, Christoph
    Wintersteini, Daniel
    TOWARDS MECHANIZED MATHEMATICAL ASSISTANTS, 2007, 4573 : 161 - +
  • [22] Towards Automatic Configuration of Interactive Known-Item Search Systems
    Peska, Ladislav
    Kovalcik, Gregor
    Lokoc, Jakub
    SIMILARITY SEARCH AND APPLICATIONS (SISAP 2019), 2019, 11807 : 340 - 347
  • [23] Towards Classification of Interactive Non-programming Tasks Promoting Computational Thinking
    Siaulys, Tomas
    Dagiene, Valentina
    INFORMATICS IN SCHOOLS: RETHINKING COMPUTING EDUCATION, ISSEP 2021, 2021, 13057 : 16 - 28
  • [24] A semantics for proof plans with applications to interactive proof planning
    Richardson, J
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, 2002, 2514 : 337 - 351
  • [25] Proof General/Eclipse: A Generic Interface for Interactive Proof
    Winterstein, Daniel
    Aspinall, David
    Lueth, Christoph
    19TH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-05), 2005, : 1587 - 1588
  • [26] QUBLE: towards blending interactive visual subgraph search queries on large networks
    Ho Hoang Hung
    Sourav S Bhowmick
    Ba Quan Truong
    Byron Choi
    Shuigeng Zhou
    The VLDB Journal, 2014, 23 : 401 - 426
  • [27] QUBLE: towards blending interactive visual subgraph search queries on large networks
    Hung, Ho Hoang
    Bhowmick, Sourav S.
    Ba Quan Truong
    Choi, Byron
    Zhou, Shuigeng
    VLDB JOURNAL, 2014, 23 (03): : 401 - 426
  • [28] Towards Reducing Latency Using Beam Search in an Interactive Conversational Speech Agent
    Ott, Nikolas
    Horst, Robin
    Doerner, Ralf
    2024 IEEE GAMING, ENTERTAINMENT, AND MEDIA CONFERENCE, GEM 2024, 2024, : 215 - 220
  • [29] A tag-frame system of resource management for proof search in linear-logic programming
    Hodas, JS
    López, P
    Polakow, J
    Stoilova, L
    Pimentel, E
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2002, 2471 : 167 - 182
  • [30] INTERACTIVE GOAL PROGRAMMING
    DYER, JS
    MANAGEMENT SCIENCE SERIES A-THEORY, 1972, 19 (01): : 62 - 70
12345