Dialogues for proof search
This work addresses the challenge of automated theorem proving in intuitionistic logic, which is incremental as it applies an existing semantic framework (dialogue games) to a new computational context.
The authors tackled the problem of using dialogue games as a foundation for proof search in intuitionistic logic, both first-order and propositional, and announced Kuno, an automated theorem prover for this logic based on dialogue games.
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.