Model-Theoretic Semantics and Tractable Algorithm for CNF-BCP

CNF-BCP is a well-known propositional reasoner that extends clausal Boolean Constraint Propagation (BCP) to non-clausal theories. Although BCP has efficient linear-time implementations, CNF-BCP requires clausal form transformation that sometimes leads to an exponential increase in the size of a theory. We present a new quadratic-time reasoner, RFP, that infers exactly the same literals as CNF-BCP. Although CNF-BCP has been specified only syntactically, we present a simple model-theoretic semantics for RFP. We also present a convergent term-rewriting system for RFP that is suitable for reasoning with knowledge bases that are built incrementally. Potential applications of RFP include logical truth-maintenance systems and general-purpose knowledge representation systems.

Authors

• Rahul Roy-Chowdhury Mukesh Dalal

Keywords

No keywords are indexed for this paper.