Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics

TL;DR

This paper introduces a syntactic abstraction technique that enables reasoning in first-order modal logics by leveraging existing theorem provers for standard first-order and propositional modal logics.

Contribution

The paper proposes a novel syntactic abstraction method that simplifies reasoning in first-order modal logics using existing theorem proving tools.

Findings

Enables reasoning in first-order modal logics with standard theorem provers

Reduces complexity of reasoning tasks in modal logics

Facilitates practical applications of modal reasoning

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.