Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








Author, Editor(s)
Author(s):
Sofronie-Stokkermans, Vioricadblp

BibTeX cite key*:

Sofronie-Stokkermans-jsc-2003

Title

Title*:

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

Journal

Journal Title*:

Journal of Symbolic Computation
Journal's URL:

http://www.academicpress.com/jsc

Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:

Elsevier
Publisher's URL:

http://www.academicpress.com/

Publisher's
Address:

Amsterdam, The Netherlands
ISSN:

0747-7171

Vol, No, pp, Date

Volume*:

36
Number:

6

Publishing Date:

2003

Pages*:

891-924
Number of
VG Pages:


Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) Abstract:

We establish a link between the satisfiability of universal
sentences with respect to classes of distributive lattices
with operators and their satisfiability with respect to
certain classes of relational structures.
This justifies a method for structure-preserving translation
to clause form of universal sentences in such classes of
algebras.

We show that refinements of resolution yield decision procedures
for the universal theory of some such classes. In particular, we
obtain exponential space and time decision procedures
for the universal clause theory of
(i) the class of all bounded distributive lattices with
operators satisfying a set of (generalized) residuation
conditions,
(ii) the class of all bounded distributive lattices with
operators,
and a doubly-exponential time decision procedure for the
universal clause theory of the class of all Heyting algebras.

URL for the Abstract:


Categories,
Keywords:


HyperLinks / References / URLs:


Copyright Message:

Copyright Elsevier Publishers

Personal Comments:


Download
Access Level:

Intranet

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:
@ARTICLE{Sofronie-Stokkermans-jsc-2003,
AUTHOR = {Sofronie-Stokkermans, Viorica},
 TITLE = {Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators},
 JOURNAL = {Journal of Symbolic Computation},
 PUBLISHER = {Elsevier},
 YEAR = {2003},
 NUMBER = {6},
 VOLUME = {36},
 PAGES = {891--924},
 ADDRESS = {Amsterdam, The Netherlands},
 ISBN = {0747-7171},
}

Entry last modified by Christine Kiesel, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Viorica Sofronie-Stokkermans		Created
01/21/2003 03:42:01 PM
Revisions
8.
7.
6.
5.
4.		Editor(s)
Christine Kiesel
Christine Kiesel
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans		Edit Dates
17.06.2004 16:03:48
17.06.2004 14:34:17
11/21/2003 01:53:33 PM
10/07/2003 04:28:12 PM
06/26/2003 04:23:26 PM