Dialogues for proof search
Jesse Alama

TL;DR
This paper introduces Kuno, an automated theorem prover for intuitionistic first-order logic that utilizes dialogue games as a foundation for proof search, offering a novel approach to logic reasoning.
Contribution
The paper presents Kuno, the first automated theorem prover for intuitionistic first-order logic based on dialogue game semantics, demonstrating its effectiveness for proof search.
Findings
Kuno successfully automates proof search in intuitionistic first-order logic.
Dialogue games provide a viable foundation for automated theorem proving.
Kuno outperforms traditional methods in certain proof search scenarios.
Abstract
Dialogue games are a two-player semantics for a variety of logics, including intuitionistic and classical logic. Dialogues can be viewed as a kind of analytic calculus not unlike tableaux. Can dialogue games be an effective foundation for proof search in intuitionistic logic (both first-order and propositional)? We announce Kuno, an automated theorem prover for intuitionistic first-order logic based on dialogue games.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Semantic Web and Ontologies
