On Non-clausal Horn-like Satisfiability Problems

Author: Edgar Altamirano
Advisor: Gonzalo E. Imaz
Year: 2005

Many applications in Computer Science require to represent knowledge and reason with non-clausal form formulas. However, most of the advances in tractable reasoning are related only to clausal (CNF) formulas.
This thesis is devoted to prove that several classes of non-clausal formulas are strictly linear in the two-valued paradigm of the logic and almost linear in the case of many-valued regular non-clausal Horn-like formulas.
Our scientic contribution can be viewed from two points of view: theoretical and practical.
On the theoretical side, our results aims at pushing further the frontiers of non clausal tractability. Thus, we firstly have defined several classes of non-clausal formulas in Negation Normal Form having a Horn-like shape. Secondly, we have established a Logical Calculus for each one of these classes, consisting of sets of inference rules which we prove they are sound and refutationally complete. In third place, we have designed several strictly linear algorithms for the cases of bi-valued paradigms and we also have developed several almost linear algorithms for the many-valued regular cases. These algorithms resolve efficiently the satis ability problem in their related classes of formulas.

On the practical side, as the non-clausal formulas keep a Horn-like structure, they are of relevant interest in many and very heterogenous applications as for instance all those based on Rule Based Systems. Indeed, rules and questions of many real applications require to represent and to reason with a richer language than the Horn formulas language. In this sense, our formulas absorb the Horn language as a particular case. Additionally, our formulas represent logically equivalent classical Horn problems but with exponentially less symbols. Hence, as the described algorithms run in linear or an almost linear time on these classes, the gain of execution time could be of an exponential order with respect to the known algorithms running over classical Horn formulas.