Representation Theorems and Automated Theorem Proving in Certain Classes of Non-classical Logics
Viorica Sofronie-Stokkermans · Max Planck Digital Library · 1998
The main goal of this paper is to present a method for translation to clause form in finitely-valued logics having as algebras of truth values distributive lattices with certain types of operators. The method uses the Priestley dual of the algebra of truth values. We illustrate these general ideas by several examples, and show that the general complexity can be further improved by using the structure of particular algebras of truth values. We then show that these ideas are actually much more general: we further develop one of our previous ideas where we showed that Priestley duality is useful in better understanding the link between algebraic and Kripke-style models for certain non-classical logics, and give several examples.