martes, 27 de septiembre de 2011

Forma clausal y cláusulas de Horn

Una fórmula del cálculo relacional es una condición que contiene predicados llamados átomos (basados en nombres de relaciones). Ademas, una fórmula puede tener cuantificadores: el cuantificador universal ("para todo") y el cuantificador existencial ("existe"). En la forma clausal, una fórmula se debe convertir en otra fórmula con las siguientes características:

-Todas las variables de la fórmila están cuantificadas universalmente. Por tanto, no es necesario incluir los cuantificadores universales explícitamente; los cuantificadores se eliminan y todas las variables de la fórmula quedan cuantificadas implícitamente por el cuantidicador universal.
-En forma clausal, la fórmila se compone de varias cláusulas, y cada cláusula se compone de varias literales conectadas exclusivamente por conectores lógicos OR. Así pues, toda cláusula es una disyunción de literales..
-Las cláusulas mismas se conectan exclusivamente mediante conectores lógicos AND, para constituir una fórmula. Así pues, la forma clausal de una fórmula es una conjunción de cláusulas.

Es posible demostrar que cualquier fórmula puede convertirse a la forma clausal. Para nuestros fines, nos interesa, principalmente, la forma de las cláusulas individuales, cada una de las cuales es una disyunción de literales.
En Datalog, las reglas se expresan como una forma restringida de cláusulas llamadas "cláusulas de Horn", en las que una cláusula puede contener cuando más una literal positiva.

No hay comentarios:

Publicar un comentario