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.

Titel
Automating Quantified Conditional Logics in HOL
Verfasser
C. Benzmüller
Verlag
AAAI Press / International Joint Conferences on Artificial Intelligence
Schlagwörter
Higher Order Logic, LEO Prover, Semantic Embedding, Modal Logics, Combinations of Logics
Datum
2013-08
Erschienen in
Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (IJCAI 2013)
Sprache
eng
Art
Text