El sistema DLV ( D ata L og with Disyunction, donde se usa el símbolo de disyunción lógica V ) es un sistema de programación lógica disyuntiva , que implementa la semántica del modelo estable bajo el paradigma de programación de conjuntos de respuestas . Extiende el lenguaje del registro de datos para permitir el uso de OR en las reglas.
Brevemente, Datalog disyuntivo es una variante de Datalog donde pueden aparecer disyunciones en los encabezados de las reglas; Las versiones avanzadas también permiten la negación en los cuerpos, que se puede manejar de acuerdo con una semántica para la negación en la programación lógica disyuntiva.
Una regla de registro de datos disyuntiva es una cláusula de la forma:
Una restricción de registro de datos disyuntiva es una cláusula de la forma:
Una de las lógicas no monótonas más populares es la lógica predeterminada de Reiter [1980]. Esta lógica se desarrolló como un formalismo de representación del conocimiento y originalmente no se concibió como un lenguaje de consulta de bases de datos. Sin embargo, se definió una configuración adecuada en la que la lógica predeterminada se puede utilizar como lenguaje de consulta para bases de datos relacionales (lenguaje de consulta predeterminado, DQL).
Desde un punto de vista práctico, en el contexto de las bases de datos deductivas, Datalog disyuntivo parece ser la extensión más adecuada de DATALOG ~ que DQL. Debido a su sintaxis simple, DATALOGv, ~ es susceptible de análisis y optimización automáticos de programas.
Estos resultados no son solo de interés teórico; Los problemas relevantes en la práctica, como el cálculo del valor de recorrido óptimo en el Problema del vendedor ambulante y los cálculos de vectores propios, se pueden manejar en Datalog disyuntivo, pero no Datalog con negación (a menos que la Jerarquía polinomial colapse). [1]
Entrada de ejemplo: registro de datos con negación como falla
fumador ( john ). fumador ( jack ).corredor ( jill ). corredor ( john ).saludable ( X ) : - corredor ( X ), \ + fumador ( X ).
Traducción a DLV: Take Clark Completion and Clausal Form
fumador (X) <- X = john.fumador (X) <- X = jack.X = john v X = jack <- fumador (X).corredor (X) <- X = jill.corredor (X) <- X = john.X = jill v X = john <- corredor (X).saludable (X) v fumador (X) <- corredor (X).corredor (X) <- saludable (X)<- saludable (X) y fumador (X).
Ejecución de ejemplo: modelo estable único
? - saludable (X).X = jill;No