Contextual logic of change and contextual proofs

We discuss CLOC, an alternative approach to reasoning about action and change, which is neither based in the Situation Calculus nor in Circumscription. In our approach, inspired by the Possible Worlds Approach, change is modeled as changing the theory that models the world. We extended First Order Logic, in order to be able to represent elementary and structured changes, and define predicates relating propositions that hold in different situations. We present one rule of inference of this new logic, EXpμ, that is used for concluding what propositions hold after the execution of change. Furthermore, we argue that traditional proof systems, e.g. Fitch´s (1952) and Lemmon´s (1965) proof systems, are not suitable for this logic, and propose a proof system where we can distinguish between propositions that hold before and after change has taken place