Lógica de transações
# Lógica de transações

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 por Anthony Bonner e Michael Kifer e posteriormente descrita em mais detalhes em e. A mais compreensível descrição aparece em.
Anos depois, Lógica de Transações foi ampliada em várias aspectos, incluindo concorrência, raciocínio revogável, ações parcialmente definidas e outras características.
Em 2013, o trabalho original em Lógica de Transações venceu o 20-years Test of Time Award como o mais influente trabalho do processo da ICLP 1993 conference nos últimos 20 anos.

## Exemplo

Coloração de grafos. Aqui tinsert denota a operação elementar de atualização da inserção transacional. O conectivo ⊗ é chamado conjunção serial.
Pirâmide de empilhamento. A operação elementária de atualização tdelete representa a operação de remoção transacional.
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.
Jantar dos filósofos. Aqui | é o conectivo lógico da conjunção paralela da Lógica de Transações Concorrente.

## Implementações

Existe 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.