Representation theorems and theorem proving in non-classical logics

摘要

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 a Priestley-style representation 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 ideas by several examples.