Non-clausal refinement of Boolean Constraint Propagation inference procedure for classical logic, called P-BCP, is introduced within a new knowledge representational formalism of polarized formulas. P-BCP is sound, incomplete, and linear time inference procedure. It is shown that P-BCP can be adopted for tractable reasoning in a number of non-classical logics (including some modal and finitely-valued logical systems).
Registration: ISBN 978-0-262-51106-3
Copyright: July 18-22, 1999, Orlando, Florida. Published by The AAAI Press, Menlo Park, California.