An ASP Approach to Generate Minimal Countermodels in Intuitionistic Propositional Logic

Camillo Fiorentini

An ASP Approach to Generate Minimal Countermodels in Intuitionistic Propositional Logic

Camillo Fiorentini

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence

Main track. Pages 1675-1681. https://doi.org/10.24963/ijcai.2019/232

PDF BibTeX

Intuitionistic Propositional Logic is complete w.r.t. Kripke semantics: if a formula is not intuitionistically valid, then there exists a finite Kripke model falsifying it. The problem of obtaining concise models has been scarcely investigated in the literature. We present a procedure to generate minimal models in the number of worlds relying on Answer Set Programming (ASP).

Keywords:

Knowledge Representation and Reasoning: Automated Reasoning and Theorem Proving

Heuristic Search and Game Playing: Modeling