On Non-clausal Horn-like Satisfiability Problems

Edgar Altamirano Carmona Affiliation: Consejo Superior de Investigaciones Científicas. Institut d'Investigació en Intel-ligencia Artificial (Bellaterra, España) Biography: Not available Close window

Edgar Altamirano Carmona About the authors  Publication year: 2007 Language: English Subjects: Science and Technology Collection: Monografies de l'Institut d'Investigació en Intel-ligencia Artificial Free eBook

Abstract:

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 scientific 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 eficiently the satisfiability 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.

Table of Contents (0.14 Mb)

Preview (0.15 Mb)

This book was added to our online catalog on Monday 20 April, 2015.