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

DOI10.1016/S0747-7171(03)00069-5zbMath1043.03013MaRDI QIDQ1432885

Viorica Sofronie-Stokkermans

Publication date: 22 June 2004

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

Heyting algebrasrelational structuresdecision proceduresdistributive lattices with operatorssatisfiability of universal sentencesuniversal clause theory

Mathematics Subject Classification ID

Heyting algebras (lattice-theoretic aspects) (06D20) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items (5)

Modules with fusion and implication based over distributive lattices: representation and duality ⋮ Automated theorem proving by resolution in non-classical logics ⋮ Binary resolution over Boolean lattices ⋮ Priestley dualities for some lattice-ordered algebraic structures, including MTL, IMTL and MV-algebras ⋮ On the refutational completeness of signed binary resolution and hyperresolution

Uses Software

• SPASS
• FLOTTER

Cites Work

• Modal languages and bounded fragments of predicate logic
• Resolution methods for the decision problem
• Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics. I
• Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics. II
• Ordered chaining calculi for first-order theories of transitive relations
• On the Computational Complexity of Algebra on Lattices
• Translation Methods for Non-Classical Logics: An Overview
• SPASS & FLOTTER version 0.42
• On the Restraining Power of Guards
• Representation of Distributive Lattices by means of ordered Stone Spaces
• Boolean Algebras with Operators. Part I
• Boolean Algebras with Operators
• The decision problem for some classes of sentences without quantifiers
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators