Dialogues for proof search
Logic
2014-05-09 v1 Artificial Intelligence
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.
Cite
@article{arxiv.1405.1864,
title = {Dialogues for proof search},
author = {Jesse Alama},
journal= {arXiv preprint arXiv:1405.1864},
year = {2014}
}
Comments
Submitted to ARQNL (Automated Reasoning in Quantified Non-Classical Logics)