Dialogues for proof search

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.