DocumentCode :
2222310
Title :
How to optimize proof-search in modal logics: a new way of proving redundancy criteria for sequent calculi
Author :
Voronkov, Andrei
Author_Institution :
Dept. of Comput. Sci., Manchester Univ., UK
fYear :
2000
fDate :
2000
Firstpage :
401
Lastpage :
412
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
Keywords :
formal logic; optimisation; search problems; theorem proving; bottom-up decision procedure; completeness; inverse method; path calculus; proof search optimization; propositional modal logic; redundancy criteria; search space; sequent calculi; subsumption; tableau-based derivations; Boolean functions; Calculus; Computer science; Data structures; Inverse problems; Knowledge representation; Logic; Optimization methods;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on
Conference_Location :
Santa Barbara, CA
ISSN :
1043-6871
Print_ISBN :
0-7695-0725-5
Type :
conf
DOI :
10.1109/LICS.2000.855787
Filename :
855787
Link To Document :
بازگشت