Coalescing for Reasoning in First-Order Modal Logics

Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, and Stephan Merz

Abstract

We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic.

Intl. Wsh. Automated Reasoning in Quantified Non-Classical Logics, 2014.

Available as: PDF

Reference

@InProceedings{doligez:coalescing-arqnl,
  author =       {Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, and Stephan Merz},
  title =        {Coalescing for Reasoning in First-Order Modal Logics},
  booktitle = {Intl. Wsh. Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014)},
  year =      2014,
  editor =    {Christoph Benzm{\"u}ller and Jens Otten},
  pages =     {15},
  address =   {Vienna, Austria},
  publisher = {arXiv CORR},
  url       = {http://arxiv.org/abs/1409.3819},
}