非表示:
キーワード:
-
要旨:
In this paper we give a method for automated theorem proving in the universal
theory of certain varieties of distributive lattices with well-behaved
operators. For this purpose, we use extensions of Priestley's representation
theorem for distributive lattices. We first establish a link between
satisfiability of universal sentences with respect to varieties of distributive
lattices with operators and satisfiability with respect to certain classes of
relational structures. We then use these results for giving a method for
translation to clause form of universal sentences in such varieties, and obtain
decidability and complexity results for the universal theory of some such
varieties. The advantage is that we avoid the explicit use of the full
algebraic structure of such lattices, instead using sets endowed with a
reflexive and transitive relation and with additional functions and relations.
We first studied this type of relationships in the context of finitely-valued
logics and then extended the ideas to more
general non-classical logics. This paper shows that the idea is much more
general. In particular, the method presented here subsumes both existing
methods for translating modal logics to classical logic and methods for
automated theorem proving in finitely-valued logics based on distributive
lattices with operators.
