How to optimize proof-search in modal logics
Андрей Воронков · ACM Transactions on Computational Logic · 2001
We present a bottom-up decision procedure for propositional modal logic K based on the inverse method. The procedure is based on the “inverted” version of a sequent calculus. To restrict the search space, we prove a number of redundancy criteria for derivations in the sequent calculus. We introduce a new technique of proving redundancy criteria, based on the analysis of tableau-based derivations in K. Moreover, another new technique is based on so-called traces . A new search with a strong notion of subsumption. This technique is based on so-called traces . A new formalization of the inverse method in the form of a path calculus considerably simplifies all proofs as compared to the previously published presentations of the inverse method. Experimental results demonstrate that our method is competitive with many state-of-the-art implementations of K.