Automating Quantified Conditional Logics in HOL

Abstract

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.

Cite

Text

Benzmueller. "Automating Quantified Conditional Logics in HOL." International Joint Conference on Artificial Intelligence, 2013.

Markdown

[Benzmueller. "Automating Quantified Conditional Logics in HOL." International Joint Conference on Artificial Intelligence, 2013.](https://mlanthology.org/ijcai/2013/benzmueller2013ijcai-automating/)

BibTeX

@inproceedings{benzmueller2013ijcai-automating,
  title     = {{Automating Quantified Conditional Logics in HOL}},
  author    = {Benzmueller, Christoph},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2013},
  pages     = {746-753},
  url       = {https://mlanthology.org/ijcai/2013/benzmueller2013ijcai-automating/}
}