Algebraic and Model Theoretic Techniques for Fusion Decidability in Modal Logics

摘要

We introduce a new method (derived from model theoretic general combination procedures in automated deduction) for proving fusion decidability in modal systems. We apply it to show fusion decidability in case not only the boolean connectives, but also a universal modality and nominals are shared symbols.