Representation Theorems and Automated Theorem Proving in Non-Classical Logics
Viorica Sofronie-Stokkermans · Max Planck Institute for Plasma Physics · 1999
In this paper we present a method for automated theorem proving in non-classical logics having as algebraic models bounded distributive lattices with certain types of operators. The idea is to use results from Priestley duality for distributive lattices with operators in order to define a class of Kripke-style models with respect to which the logic is sound and complete. If this class of Kripke-style models is elementary, it can then be used for a translation to clause form; satisfiability of the resulting clauses can be checked by resolution. We illustrate the general ideas by several examples, one of which is presented in detail.