First-Order Modal Logic Theorem Proving and Functional Simulation

Abstract

We propose a translation approach from modal logics to first‐order predicate \\u000Alogic which combines advantages from both, the (standard) relational \\u000Atranslation and the (rather compact) functional translation method and avoids \\u000Amany of their respective disadvantages (exponential growth versus equality \\u000Ahandling).\\\\ In particular in the application to serial modal logics it allows \\u000Aconsiderable simplifications such that often even a simple unit clause suffices \\u000Ain order to express the accessibility relation properties.\\\\ Although we \\u000Arestrict the approach here to first‐order modal logic theorem proving it has \\u000Abeen shown to be of wider interest, as e.g.~sorted logic or terminological \\u000Alogic.