| ||||
| ||||
![]() Title:SAT-Based Proof Search in Intermediate Propositional Logics Conference:IJCAR 2022 Tags:countermodel construction, proof-search and propositional intermediate logics Abstract: We present a decision procedure for intermediate logics relying on a modular extension of the SAT-based proof search-engine intuitR for intuitionistic propositional logic. Given the module for the intermediate logic L, our procedure iteratively searches for a Kripke countermodel for a formula A, exploiting the search engine of intuitR: whenever a countermodel for A is built, the module checks whether it is a model of the logic L. If this is the case A is not valid in L. Otherwise, the module provides an instance of an axiom of L falsified in the countermodel that is fed to the SAT-solver for a new try. We prove the partial correctness of our procedure and its termination for some well-known intermediate logics. SAT-Based Proof Search in Intermediate Propositional Logics ![]() SAT-Based Proof Search in Intermediate Propositional Logics | ||||
Copyright © 2002 – 2025 EasyChair |