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.

• Type: Conference
• Year: 1997
• Where: AAAI
• Authors: Rahul Roy-Chowdhury, Mukesh Dalal
• Keywords: AAAI 1997, Boolean Constraint Propagation, Efficient Linear-time Implementations, Intelligent Agents, Well-known Propositional Reasoner