Elementary Multimodal Logics
Jakub Michaliszyn

TL;DR
This paper investigates the complexity of multimodal logics over classes of frames defined by first-order formulas, revealing undecidability results even with transitivity constraints.
Contribution
It demonstrates that certain universal Horn formulas can define frame classes where the satisfiability problem remains undecidable, even for bimodal logics with transitive relations.
Findings
Universal Horn formulas can define undecidable frame classes.
Undecidability persists in bimodal logics with transitive relations.
Satisfiability remains undecidable under certain first-order definable classes.
Abstract
We study multimodal logics over universally first-order definable classes of frames. We show that even for bimodal logics, there are universal Horn formulas that define set of frames such that the satisfiability problem is undecidable, even if one or two of the binary relations are transitive.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Multi-Agent Systems and Negotiation · Advanced Algebra and Logic
