首页>
外文会议>Automated deduction-CADE-16
>On the universal theory of varieties of distributive lattices with operators: some decidability and complexity results
【24h】
On the universal theory of varieties of distributive lattices with operators: some decidability and complexity results
In this paper we 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 use these results for giving a method for translation to clause form of universal sentences in such varieties, and then use results from automated theorem proving to obtain decidability and complexity results for the universal theory of some such varieties.
展开▼
