An intensional epistemic logic (Q687156)

A quantified multi-modal logic with equality is defined, where terms get additional markers. These markers are integers and denote the nesting depths of the term within the modal context. In an appropriately extended Kripke semantics for the logic, these markers can be used to record the world where the term has to be evaluated, even if it occurs in different modal contexts. Using the markers, several properties which hold in standard predicate logic can be conveyed to the new logic, in particular the possibility to Skolemize existential quantifiers, to substitute terms for universally quantified variables, even if they occur in different modal contexts and to treat equations by replacing equals with equals. Exploiting these properties, a multi-modal version of Horn clauses and a corresponding extension of SLD resolution with paramodulation has been developed.