TY - JOUR
T1 - A general first-order solution to the ramification problem with cycles
AU - Strass, Hannes
AU - Thielscher, Michael
PY - 2013
Y1 - 2013
N2 - We provide a solution to the ramification problem that integrates findings of different axiomatic approaches to ramification from the last ten to fifteen years. For the first time, we present a solution that: (1) is independent of a particular time structure, (2) is formulated in classical first-order logic, (3) treats cycles - a notoriously difficult aspect - properly, and (4) is assessed against a state-transition semantics via a formal correctness proof. This is achieved as follows: We introduce indirect effect laws that enable us to specify ramifications that are triggered by activation of a formula rather than just an atomic effect. We characterise the intended models of these indirect effect laws by a state-transition semantics. Afterwards, we show how to compile a class of indirect effect laws into first-order effect axioms that then solve the ramification and frame problems. We finally prove the resulting effect axioms sound and complete with respect to the semantics defined earlier.
AB - We provide a solution to the ramification problem that integrates findings of different axiomatic approaches to ramification from the last ten to fifteen years. For the first time, we present a solution that: (1) is independent of a particular time structure, (2) is formulated in classical first-order logic, (3) treats cycles - a notoriously difficult aspect - properly, and (4) is assessed against a state-transition semantics via a formal correctness proof. This is achieved as follows: We introduce indirect effect laws that enable us to specify ramifications that are triggered by activation of a formula rather than just an atomic effect. We characterise the intended models of these indirect effect laws by a state-transition semantics. Afterwards, we show how to compile a class of indirect effect laws into first-order effect axioms that then solve the ramification and frame problems. We finally prove the resulting effect axioms sound and complete with respect to the semantics defined earlier.
UR - http://handle.uws.edu.au:8081/1959.7/548991
U2 - 10.1016/j.jal.2013.05.003
DO - 10.1016/j.jal.2013.05.003
M3 - Article
SN - 1570-8683
VL - 11
SP - 289
EP - 308
JO - Journal of Applied Logic
JF - Journal of Applied Logic
IS - 3
ER -