Lógica de transações
Foram assinalados vários problemas nesta página ou se(c)ção: |
A lógica de transações é uma extensão da Lógica de Predicados que responde de uma forma limpa e declarativa para o fenômeno de mudanças de estado em programas lógicos e bancos de dados. Esta extensão adiciona conectivos projetados especificamente para combinar ações simples em transações complexas e para fornecer controle sobre a sua execução. A lógica tem uma natural Teoria dos modelos e uma sólida e completa Teoria da Prova. A Lógica de Transações tem um subconjunto de cláusulas de Horn, que tem um procedimento, bem como uma semântica declarativa. As características importantes da lógica incluem atualizações hipotéticas e empenhadas, restrições dinâmicas na execução da transação, não-determinismo e atualizações em massa. Desta forma, Lógica de Transações é capaz de capturar declarativamente um número de fenômenos não-lógicos, incluindo conhecimentos procedurais (ou também, conhecimentos imperativos) em inteligência artificial, bancos de dados ativos e métodos com efeitos colaterais em bancos de dados de objetos.
A Lógica de Transações foi originalmente proposta em [1] por Anthony Bonner e Michael Kifer e posteriormente descrita em mais detalhes em [2] e [3]. A mais compreensível descrição aparece em [4].
Anos depois, Lógica de Transações foi ampliada em várias aspectos, incluindo concorrência [5], raciocínio revogável [6], ações parcialmente definidas [7] e outras características [8][9].
Em 2013, o trabalho original em Lógica de Transações [1] venceu o 20-years Test of Time Award como o mais influente trabalho do processo da ICLP 1993 conference nos últimos 20 anos.
Exemplo
editarColoração de grafos. Aqui tinsert denota a operação elementar de atualização da inserção transacional. O conectivo ⊗ é chamado conjunção serial.
colorNode <- // colore um nó corretamente
node(N) ⊗ &neg; colored(N,_) ⊗ color(C)
⊗ ¬(adjacent(N,N2) ∧ colored(N2,C))
⊗ tinsert(colored(N,C)).
colorGraph <- ¬uncoloredNodesLeft.
colorGraph <- colorNode ⊗ colorGraph.
Pirâmide de empilhamento. A operação elementária de atualização tdelete representa a operação de remoção transacional.
stack(N,X) <- N>0 ⊗ move(Y,X) ⊗ stack(N-1,Y).
stack(0,X).
move(X,Y) <- pickup(X) ⊗ putdown(X,Y).
pickup(X) <- clear(X) ⊗ on(X,Y) ⊗
⊗ tdelete(on(X,Y)) ⊗ tinsert(clear(Y)).
putdown(X,Y) <- wider(Y,X) ⊗ clear(Y)
⊗ tinsert(on(X,Y)) ⊗ tdelete(clear(Y)).
Execução hipotética. Aqui <> é o operador modal de possibilidade: Se ambos action1 e action2 são possíveis, execute action1. Caso contrário, se somente action2 é possível, então execute ela.
execute <- <>action1 ⊗ <>action2 ⊗ action1. execute <- ¬<>action1 ⊗ <>action2 ⊗ action2.
Jantar dos filósofos. Aqui | é o conectivo lógico da conjunção paralela da Lógica de Transações Concorrente [5].
diningPhilosophers <- phil(1) | phil(2) | phil(3) | phil(4).
Implementações
editarExiste um número de implementações da Lógica de Transações. A implementação original está disponível aqui. Uma implementação da Lógica de Transações Concorrente está disponível aqui. A Lógica de Transações aperfeiçoada com apresentação pode ser encontrada aqui. Uma implementação da Lógica de Transações teve sido incorporada como parte do Flora-2, sistema de raciocínio e representação do conheciento. Todas estas implementações são de código aberto.
Trabalhos adicionais em Lógica de Transações podem ser encontrados no sítio do Flora-2.
Referências
- ↑ a b A.J. Bonner and M. Kifer (1993), Transaction Logic Programming, International Conference on Logic Programming (ICLP), 1993.
- ↑ A.J. Bonner and M. Kifer (1994), An Overview of Transaction Logic, Theoretical Computer Science, 133:2, 1994.
- ↑ A.J. Bonner and M. Kifer (1998), Logic Programming for Database Transactions in Logics for Databases and Information Systems, J. Chomicki and G. Saake (eds.), Kluwer Academic Publ., 1998.
- ↑ A.J. Bonner and M. Kifer (1995), Transaction Logic Programming (or A Logic of Declarative and Procedural Knowledge). Technical Report CSRI-323, November 1995, Computer Science Research Institute, University of Toronto.
- ↑ a b A.J. Bonner and M. Kifer (1996), Concurrency and communication in Transaction Logic, Joint Intl. Conference and Symposium on Logic Programming, Bonn, Germany, September 1996
- ↑ P. Fodor and M. Kifer (2011), Transaction Logic with Defaults and Argumentation Theories. In Technical communications of the 27th International Conference on Logic Programming (ICLP), July 2011.
- ↑ M. Rezk and M. Kifer (2012), Transaction Logic with Partially Defined Actions. Journal on Data Semantics, August 2012, vol. 1, no. 2, Springer.
- ↑ H. Davulcu, M. Kifer and I.V. Ramakrishnan (2004), CTR-S: A Logic for Specifying Contracts in Semantic Web Services. Proceedings of the 13-th World Wide Web Conference (WWW2004), May 2004.
- ↑ P. Fodor and M. Kifer (2010), Tabling for Transaction Logic. In Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP), July 2010.