Context Logic

Abstract

Context Logic (CL) is a logic in the original sense, but more than that, it is a methodology for designing a certain class of logics in such a way that automatically a first-order many-sorted resolution and paramodulation calculus is obtained. This calculus can be executed on a clause based predicate logic theorem prover. The class of logics which can be handled with the CL-methodology is mainly characterized by the existence of “hidden parameters”, parameters like worlds in modal logics defining the context in which the terms and formulae are to be interpreted. The hidden parameters are usually determined implicitly by additional logical operators like for example □ (necessarily) and ◊ (possibly) in modal logic. These operators refer to an underlying semantical structure - Kripke’s possible worlds structure in the case of modal logic, time points and time intervals in the case of temporal logic are examples. CL provides a means for axiomatizing these structures and for expressing the semantics of the desired operators in a formal language. This information about the desired logic is sufficient to translate formulae written in the operator syntax automatically into predicate logic syntax where the operators are replaced by quantifiers and the hidden parameters are made an explicit part of the formula. After the translation, information about a whole bunch of nested operators is shifted into one “context term” that can be handled by an appropriate unification algorithm. Hence, a resolution step may exploit information about many nested operators at once and is therefore much more goal directed than a corresponding step in a tableaux system for example. The main limits of CL are: • Since predicate logic is the “target logic” into which the designed logic is mapped, in order to obtain a complete calculus, its semantical structure must be first-order axiomatizable. This excludes certain properties like discreteness and finiteness. • Due to the current limits of predicate logic resolution (no partial functions allowed for example) two further assumptions are still necessary. For Kripke structures these are the constant-domain assumption and the seriality assumption. For other structures the assumptions are analogous. In order to demonstrate the method, a quite complex first-order many-sorted multi modal logic with operators indexed with arbitrary (possibly non-ground) terms is constructed using the CL tools. The logic is actually an extension of Clarke and Emerson’s CTL temporal logic. Therefore, as a side effect, we get a proof theory for CTL.