Paper: How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi (at LICS 2000)

Authors: Andrei Voronkov

Abstract

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 used to prove completeness of proof-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 reported elsewhere demonstrate that our method is competitive with many state-of-the-art implementations of K.

BibTeX

  @InProceedings{Voronkov-HowtoOptimizeProofS,
    author = 	 {Andrei Voronkov},
    title = 	 {How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2000)},
    year =	 {2000},
    month =	 {June}, 
    pages =      {401--412},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }