A notion of quantified conditional logics is provided that includes quantification over individual and propositional variables. The former is supported with respect to constant and variable domain semantics. In addition, a sound and complete embedding of this framework in classical higher-order logic is presented. Using prominent examples from the literature it is demonstrated how this embedding enables effective automation of reasoning within (object-level) and about (meta-level) quantified conditional logics with off-the-shelf higher-order theorem provers and model finders.
Automating Quantified Conditional Logics in HOL
AAAI Press / International Joint Conferences on Artificial Intelligence
Higher Order Logic, LEO Prover, Semantic Embedding, Modal Logics, Combinations of Logics