Resolution-based decision procedures for the universal theory of some classes 
of distributive lattices with operators

Sofronie-Stokkermans, Viorica

アイテム詳細

登録内容を編集ファイル形式で保存

一時保存へ追加

タグ情報を表示リリース履歴を表示詳細要約

公開

報告書

Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators

MPS-Authors

/persons/resource/persons45516

Sofronie-Stokkermans, Viorica
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource

There are no locators available

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

フルテキスト (公開)

2001-2-005
(全文テキスト（全般）), 11KB

付随資料 (公開)

There is no public supplementary material available

引用

Sofronie-Stokkermans, V.(2001). Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators (MPI-I-2001-2-005). Saarbrücken: Max-Planck-Institut für Informatik.

引用: https://hdl.handle.net/11858/00-001M-0000-0014-6CB3-4

要旨

In this paper we establish a link between satisfiability of universal sentences with respect to classes of distributive lattices with operators and satisfiability with respect to certain classes of relational structures. This justifies a method for structure-preserving translation to clause form of universal (Horn) sentences in such classes of algebras. We show that refinements of resolution yield decision procedures for the universal (Horn) theory of some such classes. In particular, we obtain exponential decision procedures for the universal Horn theory of (i) the class of all bounded distributive lattices with operators, (ii) for the class of all bounded distributive lattices with operators satisfying a set of (generalized) residuation conditions, and a doubly-exponential decision procedure for the universal Horn theory of the class of all Heyting algebras.