Registro de datos Z

DatalogZ (estilizado como Datalog _ℤ ) es una extensión de Datalog con aritmética de números enteros y comparaciones. El problema de decisión de si un átomo fundamental dado (hecho) está implicado o no por un programa DatalogZ es RE-completo (por lo tanto, indecidible ), lo que se puede demostrar mediante una reducción a ecuaciones diofánticas . ^[1]

La sintaxis de DatalogZ extiende la de Datalog con términos numéricos , que son constantes enteras, variables enteras o términos formados a partir de estas mediante la adición, la resta y la multiplicación. Además, DatalogZ permite la comparación de átomos , que son átomos de la forma t < so t <= spara términos numéricos t, s. ^[2]

La semántica de DatalogZ se basa en la semántica de teoría de modelos (Herbrand) de Datalog . ^[2]

La indecidibilidad de la implicación de DatalogZ motiva la definición de límite DatalogZ . El límite DatalogZ restringe los predicados a una única posición numérica, que se marca como máxima o mínima. La semántica se basa en la semántica de teoría de modelos (Herbrand) de Datalog. La semántica requiere que las interpretaciones de Herbrand sean cerradas al límite para calificar como modelos, en el siguiente sentido: Dado un átomo fundamental de un predicado límite donde la última posición es una posición máxima (resp. mín), si está en una interpretación de Herbrand , entonces los átomos fundamentales para (resp. ) también deben estar en para para ser cerrados al límite. ^[3]${\displaystyle a=r(c_{1},\ldots ,c_{n})}$${\estilo de visualización r}$${\estilo de visualización a}$${\displaystyle I}$${\displaystyle r(c_{1},\ldots ,k)}$$estilo de visualización k>c_{n}}$$estilo de visualización k<c_{n}}$${\displaystyle I}$${\displaystyle I}$

Dada una constante w, una relación binaria edgeque representa los bordes de un gráfico y una relación binaria spcon la última posición de spmínimo, el siguiente programa DatalogZ de límite calcula la relación sp, que representa la longitud de la ruta más corta desde wa cualquier otro nodo en el gráfico:

sp ( w ,  0 )  :-  . 
sp ( y ,  m  +  1 )  :-  sp ( x ,  m ),  borde ( x ,  y ).

• Programación lógica de restricciones

• Grau, Bernardo Cuenca; Horrocks, Ian; Kaminski, Mark; Kostylev, Egor V.; Motik, Boris (2020-02-25). "Limit Datalog: un lenguaje de consulta declarativo para el análisis de datos". ACM SIGMOD Record . 48 (4): 6– 17. doi :10.1145/3385658.3385660. ISSN  0163-5808. S2CID  211520719.
• Kaminski, Mark; Grau, Bernardo Cuenca; Kostylev, Egor V.; Motik, Boris; Horrocks, Ian (12 de noviembre de 2017). "Fundamentos del análisis de datos declarativos utilizando programas de registro de datos límite". arXiv : 1705.06927 [cs.AI].
• Kaminski, Mark; Kostylev, Egor V.; Grau, Bernardo Cuenca; Motik, Boris; Horrocks, Ian (2021-12-22). "La complejidad y el poder expresivo de los registros de datos de límites". Revista de la ACM . 69 (1): 6:1–6:83. doi :10.1145/3495009. ISSN  0004-5411. S2CID  246702614.