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 sometimesleads 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-theoreticsemantics 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-purposeknowledge representation systems.
展开▼
