A general first-order solution to the ramification problem with cycles

Hannes Strass, Michael Thielscher

    Research output: Contribution to journalArticlepeer-review

    Abstract

    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.
    Original languageEnglish
    Pages (from-to)289-308
    Number of pages20
    JournalJournal of Applied Logic
    Volume11
    Issue number3
    DOIs
    Publication statusPublished - 2013

    Fingerprint

    Dive into the research topics of 'A general first-order solution to the ramification problem with cycles'. Together they form a unique fingerprint.

    Cite this