Polarity Guided Tractable Reasoning

Zbigniew Stachniak, York University

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


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.