Аннотация:В статье мы анализируем логику атомарных транзакций AtL (atomic transactions
logic), недавно предложенную Матеушем Радзким. В данной табличной трехзначной
логике атомарные транзакции выполняются по принципу “все или ничего”:
либо транзакция выполняется от начала до конца, либо не выполняется вообще,
не останавливаясь на каком-то ее промежуточном этапе. Свойство атомарности является
одним из базовых свойств транзакций в системах баз данных, обеспечивая защиту от сбоев
при передаче данных. С точки зрения логики, AtL состоит из отрицания и импликации
трехзначной логики, предложенной Яном Лукасевичем, а также из введенной Стивеном
Блейми интеръюнкции – специфической связки, обладающей свойствами и конъюнкции,
и дизъюнкции. Задавая AtL семантически и не предлагая аксиоматизирующего
ее логического исчисления, М. Радзкий тем не менее формализует ее работу в случае
атомарных транзакций. В статье мы обсудим возможность аксиоматизации AtL с помощью
метода корреспондентского анализа.