Polarity Guided Tractable Reasoning

Proceedings of the AAAI Conference on Artificial Intelligence, 16

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 16

Tractable Reasoning

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).