SMV-algebras and Kripke models: comparing the semantics

Tommaso Flaminio, Franco Montagna.

In this paper we compare the variety of SMV-algebras with the class of Kripke models introduced in [8, 6, 5] as semantics for the logics FP(Ln, L) and FP(L, L). The main result of this paper tells us that a formula φ written in the language of SMValgebras is satisfiable in a Kripke model iff there exists a non-trivial SMV-algebra satisfying φ. This result is used also to provide results about the decidability and complexity for SMV-algebras.

PDF full paper