Embedding and automating conditional logics in classical higher-order logic (Q1935597)

A semantic embedding of conditional logics in classical higher-order logic HOL (Church's type theory) is presented. This embedding exploits the natural correspondence between selection function semantics for conditional logics and HOL. It is proved that the presented embedding is sound and complete. This result does not trivially follow from previous literature on embedding modal logics into HOL because of the complexity of the selection function. In fact, standard modalities are usually evaluated over a so-called accessibility relation of type \(R(i,w)\), where \(i\) is an index and \(w\) is a world. Conditional modalities are instead evaluated over selection functions of type \(f(w,A)\) where \(w\) is a world, \(A\) is a set of worlds and \(f\) is a function which returns a set of worlds. In the second part of the paper it is shown how to apply off-the-shelf higher-order theorem provers and model finders for reasoning within and about conditional logics. Several correspondence results between prominent conditional logic axioms and related semantic conditions have been automatically verified.