Tableaux for reasoning about atomic updates

Fermüller, Christian G., Georg Moser, and Richard Zach. 2001. “Tableaux for Reasoning about Atomic Updates.” In Logic for Programming, Artificial Intelligence, and Reasoning, edited by Robert Nieuwenhuis and Andrei Voronkov, 639–53. LNCS. Berlin: Springer. https://doi.org/10.1007/3-540-45653-8_44.

A simple model of dynamic databases is studied from a modal logic perspecitve. A state \(\alpha\) of a database is an atomic update of a state \(\beta\) if at most one atomic statement is evaluated differently in \(\alpha\) compared to \(\beta\). The corresponding restriction on Kripke-like structures yields so-called update logics. These logics are studied also in a many-valued context. Adequate tableau calculi are given.

Continue reading