Intuitionistic modal logics IS4 and IK4 shown decidable with new proof method
A decision procedure for intuitionistic modal logic IS4 (and IK4)
Logic in Computer Science
Summary
Some logical systems used to reason about possibilities and necessity can be hard to decide if statements are true or not. The authors found a way to always answer this question for two such systems, IS4 and IK4, by either proving the statement or giving a small counter-example. They use a special way to detect repeating patterns in proofs to make the process work. This also confirms that any false statement can be shown false with a finite example, which helps with checking these logics.
What this means in practice
- •For formal verification engineers: Use decidability of IS4 and IK4 to automate proving system properties expressible in these logics.
- •For automated reasoning developers: Integrate the loop rule method for efficient proof search in tools handling intuitionistic modal logics.
A theory result. No direct application yet.
Authors
Marianna Girlando, Roman Kuznets, Sonia Marin, Lutz Straßburger
Abstract
In this paper, we show that the two intuitionistic modal logics IS4 and IK4 are decidable. We provide a constructive decision procedure, that, given a formula, produces either a proof showing the formula to be valid or a finite countermodel falsifying the formula, thus also proving the finite model property for both logics. The main ingredient of our strategy is the introduction of (possibly unsound) loop rules, which encode repeating behaviour in proof search. This paper fixes a previous mistake in our LICS'23 contribution.