Dialogues for proof search
arXiv:1405.1864
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.
Submitted to ARQNL (Automated Reasoning in Quantified Non-Classical Logics)