Abstract We revise our logic for contrary-to-duty (CTD) conditionals, showing how to adjust our logical models in such a way as to avoid the counterintuitive results pointed out by Bjørn Kjos-Hanssen, but keep the main results that support our logical analysis of CTD scenarios.

Journal Article Completeness and decidability results for a logic of contrary-to-duty conditionals Get access José M. C. L. M. Carmo, José M. C. L. M. Carmo Centre of Exact Sciences and Engineering, University of Madeira, Campus Universitario da Penteada, 9020-105 Funchal, Madeira, Portugal. E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar Andrew J. I. Jones Andrew J. I. Jones Department of Informatics, King's College London Strand, London WC2R 2LS, UK. E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 23, Issue 3, June 2013, Pages 585–626, https://doi.org/10.1093/logcom/exs009 Published: 25 April 2012 Article history Received: 01 September 2011 Published: 25 April 2012

The framework underlying CTL* is extended in order to include past operators. Recent developments in areas related to concurrent program specification and verification, as well as database and information systems specification, justify the interest of such extension. The semantics for the language so obtained is defined according to the ockhamist approach to non-deterministic time. The differences between this semantics and the original semantics for CTL* are analysed. A sound axiomatization is proposed for such logic and its completeness is proved.

Abstract A brief overview is given of the temporal logics used in concurrent program verification and in database and systems specification. The properties of the underlying modal frame structures are analysed. The relative advantages of the linear and branching approaches are discussed. The state versus path formulas controversy is revisited. A meta-linear operatorLis proposed and compared with the “in all trajectories” operator considered in the language CTL*. The usefulness of the new operator within the context of a layered methodology for database and information systems specification and verification is illustrated. The operator is seen as a “frame change operator” and other interesting operators of this class are referred. Finitary and infinitary axiomatisations are given for the operatorL. The proof of the completeness of the infinitary axiomatisation is briefly outlined. This proof requires an appropriate extension of the usual Henkin methods.