Welcome Guest!

Quick Find:  

Advanced Search

Languages: English Español

Valid XHTML 1.0 Transitional ¡CSS Válido! Icono de conformidad con el Nivel Doble-A, 
	de las Directrices de Accesibilidad para el 
	Contenido Web 1.0 del W3C-WAI

On Non-clausal Horn-like Satisfiability Problems

On Non-clausal Horn-like Satisfiability Problems
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


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 Table of Contents (0.14 Mb)

Preview Preview (0.15 Mb)

Bibliographic information

Physical Description : XV, 126 p. : gráf. ; 24 cm

ISBN: 978-84-00-08573-5

Publication: Bellaterra (España) : Consejo Superior de Investigaciones Científicas, 2007

Reference CSIC: 11494

Other data: Thesis

Buy the digital edition at

This eBook is available for free download

Free Downloads

Download eBook Download eBook (1.49 Mb)

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