Abstract:

Many applications in Computer Science require to represent knowledge and reason with non-clausal form formulas. However, most of the advances obtained in tractable reasoning are applied only to CNF formulas. In this paper, we extend tractability (even linearity) to certain non-clausal formulas which are of high practical interest. For instance, the real applications of the Knowledge Rule-based Systems can increase allowing a richer language and preserving a high efficiency level for performing reasoning. Our non-clausal formulas codify the same problems that the Horn formulas but with significantly, even exponentially, less propositional symbols. After defining these formulas, we establish a sound and refutation complete logical calculus. Finally, a correct and strictly linear running time SAT algorithm is designed. As a result, the time required by our linear algorithms running on the defined Horn-like non-clausal formulas, can be exponentially less than that required by the existing linear HORN-SAT algorithms, running on the logically equivalent HORN formulas.

• Tagged
• XML
• BibTex