2008 | OriginalPaper | Chapter
Towards Ludics Programming: Interactive Proof Search
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Girard [1] introduced Ludics as an interactive theory aiming at overcoming the distinction between syntax and semantics in logic.
In this paper, we investigate how ludics could serve as a foundation for logic programming, providing a mechanism for interactive proof search, that is proof search by interaction (or proof search by cut-elimination).