Tableaux for Reasoning About Atomic Updates

A simple model of dynamic databases is studied from a modal logic perspecitve. A state α of a database is an atomic update of a state β if at most one atomic statement is evaluated differently in α compared to β. 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.

• Type: Conference
• Year: 2001
• Where: LPAR
• Authors: Christian G. Fermüller, Georg Moser, Richard Zach
• Keywords: Adequate Tableau Calculi, Automated Reasoning, LPAR 2001, Modal Logic Perspecitve, So-called Update Logics