Transaction Logic es una extensión de la lógica de predicados que explica de forma limpia y declarativa el fenómeno de los cambios de estado en los programas lógicos y las bases de datos . Esta extensión agrega conectores diseñados específicamente para combinar acciones simples en transacciones complejas y para proporcionar control sobre su ejecución. La lógica tiene una teoría de modelo natural y una teoría de prueba sólida y completa . Transaction Logic tiene una cláusula Hornsubconjunto, que tiene una semántica tanto procedimental como declarativa. Las características importantes de la lógica incluyen actualizaciones hipotéticas y comprometidas, restricciones dinámicas en la ejecución de transacciones, no determinismo y actualizaciones masivas. De esta manera, Transaction Logic es capaz de capturar de forma declarativa una serie de fenómenos no lógicos, incluido el conocimiento procedimental en inteligencia artificial , bases de datos activas y métodos con efectos secundarios en bases de datos de objetos .
La lógica de transacción fue propuesta originalmente en [1] por Anthony Bonner y Michael Kifer y luego descrita con más detalle en [2] y. [3] La descripción más completa aparece en. [4]
En años posteriores, Transaction Logic se extendió de varias maneras, incluida la concurrencia , [5] razonamiento anulable , [6] acciones parcialmente definidas, [7] y otras características. [8] [9]
En 2013, el documento original en la lógica de transacción [1] ha ganado la prueba de 20 años de la concesión de Tiempo de la Asociación para la programación lógica como el papel más influyente de las actas de la conferencia ICLP 1993 en los 20 años anteriores.
Ejemplos de
Coloración gráfica
Aquí tinsert denota la operación de actualización elemental de la inserción transaccional . El conectivo ⊗ se llama conjunción serial .
colorNode <- // colorear un nodo correctamente nodo (N) ⊗ ¬ coloreado (N, _) ⊗ color (C) ⊗ ¬ (adyacente (N, N2) ∧ coloreado (N2, C)) ⊗ tinsert (coloreado (N, C)).colorGraph <- ¬uncoloredNodesLeft.colorGraph <- colorNode ⊗ colorGraph.
Apilamiento piramidal
La actualización elemental tdelete representa la operación de eliminación transaccional .
apilar (N, X) <- N> 0 ⊗ mover (Y, X) ⊗ apilar (N-1, Y).apilar (0, X).mover (X, Y) <- recoger (X) ⊗ dejar (X, Y).recoger (X) <- borrar (X) ⊗ en (X, Y) ⊗ ⊗ tdelete (en (X, Y)) ⊗ tinsert (borrar (Y)).menospreciar (X, Y) <- más ancho (Y, X) ⊗ claro (Y) ⊗ tinsert (en (X, Y)) ⊗ tdelete (borrar (Y)).
Ejecución hipotética
Aquí <> es el operador modal de posibilidad: si ambos action1 y action2 son posibles, ejecutar acción1 . De lo contrario, si solo action2 es posible, luego ejecútelo.
ejecutar <- <> acción1 ⊗ <> acción2 ⊗ acción1.ejecutar <- ¬ <> action1 ⊗ <> action2 ⊗ action2.
Filósofos gastronómicos
Aquí | es el conectivo lógico de la conjunción paralela de la lógica de transacción concurrente. [5]
comedorFilosofos <- phil (1) | phil (2) | phil (3) | phil (4).
Implementaciones
Existen varias implementaciones de Transaction Logic:
- La implementación original. [10]
- Una implementación de la lógica de transacciones concurrentes. [11]
- Lógica de transacciones mejorada con tabulación . También se ha incorporado una implementación de Transaction Logic como parte del sistema de razonamiento y representación del conocimiento de Flora-2 . [12]
Todas estas implementaciones son de código abierto .
Referencias
- ^ a b A.J. Bonner y M. Kifer (1993), Transaction Logic Programming , International Conference on Logic Programming (ICLP), 1993.
- ^ AJ Bonner y M. Kifer (1994), Una descripción general de la lógica de transacciones , Informática teórica, 133: 2, 1994.
- ^ AJ Bonner y M. Kifer (1998), Programación lógica para transacciones de bases de datos en lógicas para bases de datos y sistemas de información, J. Chomicki y G. Saake (eds.), Kluwer Academic Publ., 1998.
- ^ AJ Bonner y M. Kifer (1995), Programación lógica de transacciones (o una lógica del conocimiento declarativo y procedimental) . Informe técnico CSRI-323, noviembre de 1995, Instituto de Investigación en Ciencias de la Computación, Universidad de Toronto.
- ^ a b A.J. Bonner y M. Kifer (1996), Concurrencia y comunicación en la lógica de transacciones , Joint Intl. Conferencia y simposio sobre programación lógica, Bonn, Alemania, septiembre de 1996
- ^ P. Fodor y M. Kifer (2011), Lógica de transacciones con valores predeterminados y teorías de la argumentación . En Comunicaciones técnicas de la 27a Conferencia Internacional de Programación Lógica (ICLP), julio de 2011.
- ^ M. Rezk y M. Kifer (2012), Lógica de transacción con acciones parcialmente definidas . Journal on Data Semantics, agosto de 2012, vol. 1, no. 2, Springer.
- ^ H. Davulcu, M. Kifer y IV Ramakrishnan (2004), CTR-S: Una lógica para especificar contratos en servicios web semánticos. Actas de la 13a Conferencia World Wide Web (WWW2004), mayo de 2004.
- ^ P. Fodor y M. Kifer (2010), Presentación de lógica de transacciones . En Actas del 12 ° simposio internacional ACM SIGPLAN sobre Principios y práctica de la programación declarativa (PPDP), julio de 2010.
- ^ Hung, Samuel (1996). "Prototipo de lógica de transacciones" . Universidad de Toronto, Departamento de Ciencias de la Computación . Consultado el 10 de mayo de 2021 .
- ^ Sleghel, Amalia F. (2000). "Prototipo de lógica de transacciones concurrentes" . Universidad de Toronto, Departamento de Ciencias de la Computación . Consultado el 10 de mayo de 2021 .
- ^ "Representación y razonamiento del conocimiento con Flora-2" . Sourceforge.net . Consultado el 10 de mayo de 2021 .
enlaces externos
- Sitio web Flora-2 , que contiene artículos adicionales sobre la lógica de transacciones