Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
type: Item
instance of: scholarly article
title: Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
zbMATH Open document ID: 1043.03013
DOI: 10.1016/S0747-7171(03)00069-5
author: Viorica Sofronie-Stokkermans
published in: Journal of Symbolic Computation
publication date: 2004-06-22T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 06D20
zbMATH DE Number: 2076999
zbMATH Keywords: satisfiability of universal sentences
zbMATH Keywords: distributive lattices with operators
zbMATH Keywords: relational structures
zbMATH Keywords: decision procedures
zbMATH Keywords: universal clause theory
zbMATH Keywords: Heyting algebras
describes a project that uses: SPASS
describes a project that uses: FLOTTER
MaRDI profile type: Publication
cites work: Q4085699
cites work: Modal languages and bounded fragments of predicate logic
cites work: Ordered chaining calculi for first-order theories of transitive relations
cites work: Resolution theorem proving
cites work: Q4308745
cites work: Q3934450
cites work: Q3696560
cites work: Q4692885
cites work: Q4503908
cites work: Q4940724
cites work: Resolution methods for the decision problem
cites work: Q4329239
cites work: Q4313857
cites work: Monotone bounded distributive lattice expansions
cites work: On the Restraining Power of Guards
cites work: On the Computational Complexity of Algebra on Lattices
cites work: Boolean Algebras with Operators. Part I
cites work: Boolean Algebras with Operators
cites work: The decision problem for some classes of sentences without quantifiers
cites work: Q4218134
cites work: Translation Methods for Non-Classical Logics: An Overview
cites work: Encoding two-valued nonclassical logics in classical logic
cites work: Representation of Distributive Lattices by means of ordered Stone Spaces
cites work: Q3222242
cites work: Q4263162
cites work: Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics. I
cites work: Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics. II
cites work: Q4544342
cites work: Q4450440
cites work: SPASS & FLOTTER version 0.42
description: scientific article; zbMATH DE number 2076999