How to optimize proof-search in modal logics: a new way of proving redundancy criteria for sequent calculi

Andrei Voronkov

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    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.
    Original languageEnglish
    Title of host publicationProceedings - Symposium on Logic in Computer Science|Proc Symp Logic Comput Sci
    Place of PublicationPiscataway, NJ, United States
    PublisherIEEE
    Pages401-412
    Number of pages11
    Publication statusPublished - 2000
    Event15th Annual IEEE Symposium on Logic in Computer Science - Santa Barbara, CA, USA
    Duration: 1 Jul 2000 → …
    http://dblp.uni-trier.de/db/conf/lics/lics2000.html#Voronkov00http://dblp.uni-trier.de/rec/bibtex/conf/lics/Voronkov00.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/lics/Voronkov00

    Conference

    Conference15th Annual IEEE Symposium on Logic in Computer Science
    CitySanta Barbara, CA, USA
    Period1/07/00 → …
    Internet address

    Fingerprint

    Dive into the research topics of 'How to optimize proof-search in modal logics: a new way of proving redundancy criteria for sequent calculi'. Together they form a unique fingerprint.

    Cite this