Automating Quantified Conditional Logics in HOL

C. Benzmüller— 2013

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.

TitelAutomating Quantified Conditional Logics in HOL
VerfasserC. Benzmüller
VerlagAAAI Press / International Joint Conferences on Artificial Intelligence
ThemaHigher Order Logic, LEO Prover, Semantic Embedding, Modal Logics, Combinations of Logics
Erschienen inProceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (IJCAI 2013)