Gore, Rajeev; Kupke, Clemens; Pattinson, Dirk
Deciding whether a modal formula is satisfiable with respect to a given set of (global) assumptions is a question of fundamental importance in applications of logic in computer science. Tableau methods have proved extremely versatile for solving this problem for many different individual logics but they typically do not meet the known complexity bounds for the logics in question. Recently, it has been shown that optimality can be obtained for some logics while retaining practicality by using a...[Show more]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.