Embedding Boolean expressions into logic programming

DOI10.1016/S0747-7171(87)80065-2zbMath0641.68148MaRDI QIDQ1100935

Helmut Simonis, Wolfram Buettner

Publication date: 1987

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

zbMATH Keywords

PROLOGBoolean expressionslogic programmingmost general unifierunification theory

Mathematics Subject Classification ID

Logical aspects of Boolean algebras (03G05)

Related Items (22)

On the complexity of Boolean unification ⋮ Unification in varieties of idempotent semigroups ⋮ Negative Boolean constraints ⋮ Running time experiments on some algorithms for solving propositional satisfiability problems ⋮ Unification in commutative idempotent monoids ⋮ Unification in Boolean rings ⋮ Controlling the complexity in model-based diagnosis ⋮ Propositional calculus problems in CHIP ⋮ Ordered Binary Decision Diagrams and the Davis-Putnam procedure ⋮ Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages ⋮ Complexity assessments for decidable fragments of set theory. II: A taxonomy for `small' languages involving membership ⋮ Discriminator varieties and symbolic computation ⋮ Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case* ⋮ Solving a cutting-stock problem with the constraint logic programming language CHIP ⋮ IMPLEMENTING COMPLEX DOMAINS OF APPLICATION IN AN EXTENDED PROLOG SYSTEM ⋮ Goals and benchmarks for automated map reasoning ⋮ Constraint satisfaction using constraint logic programming ⋮ The Evaluation and the Computational Complexity of Datalog Queries of Boolean Constraint Databases ⋮ Symbolic constraint handling through unification in finite algebras ⋮ Boolean unification - the story so far ⋮ Unification problem in equational theories ⋮ On equational theories, unification, and (un)decidability

Cites Work

• Refutational theorem proving using term-rewriting systems
• Unification in abelian semigroups
• A Unification Algorithm for Associative-Commutative Functions
• A Machine-Oriented Logic Based on the Resolution Principle
• DIOPHANTINE REPRESENTATION OF ENUMERABLE PREDICATES
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Embedding Boolean expressions into logic programming