| Sumario: | Esta tesis está dedicada a probar que existen varias clases de fórmulas en formas no clausales que son estrictamente lineales en el caso de la lógica proposicional y casi-lineales en el caso de la lógica multivaluada. Nuestra contribución científica puede ser considerada desde dos puntos de vista: teórico y práctico. En cuanto al aspecto teórico, nuestros resultados amplían el campo de la tratabilidad no clausal. Así, en primer lugar hemos definido varias clases de fórmulas no-clausales en forma normal negada con una estructura de Horn. En segundo lugar, hemos establecido un cálculo lógico para cada una de estas clases, consistente en un conjunto de reglas de inferencia que probamos que forman un cálculo sólido y refutacionalmente completo. En tercer lugar, hemos diseñado algoritmos estrictamente lineales para el caso de la lógica proposicional y hemos desarrollado algoritmos casi-lineales para el caso de la lógica multivaluada. Estos algoritmos resuelven eficientemente el problema de la satisfactibilidad en cada clase correspondiente. En cuanto al aspecto práctico, como las fórmulas mantienen una estructura de Horn, son de relevante interés en varias aplicaciones como por ejemplo las provenientes de los sistemas basados en reglas. De hecho, las reglas y preguntas en muchas aplicaciones reales requieren representar y razonar con un lenguaje más rico que el ofrecido por el lenguaje de fórmulas de Horn. En este sentido, nuestras fórmulas absorben las fórmulas de Horn como un caso particular. Además, nuestras fórmulas son lógicamente equivalentes a fórmulas de Horn pero utilizan un número exponencialmente inferior de símbolos. Por lo tanto, como los algoritmos descritos corren en tiempo lineal o casi lineal sobre estas clases de problemas, la ganancia experimentada puede ser de un orden exponencial con respecto a los algoritmos conocidos ejecutándose sobre las clásicas fórmulas de Horn.
|
|---|
