@inproceedings{Ganzinger+Hustadt+Meyer+Schmidt@AiML1998,
 author    = {Harald Ganzinger and
              Ullrich Hustadt and
              Christoph Meyer and
              Renate A. Schmidt},
 title     = {A Resolution-Based Decision Procedure for Extensions of K4},
 year      = {1998},
 pages     = {225-246},
 editor    = {Michael Zakharyaschev and
              Krister Segerberg and
              Maarten de Rijke and
              Heinrich Wansing},
 booktitle = {Advances in Modal Logic 2, papers from the second workshop
              on "Advances in Modal logic," held in Uppsala, Sweden, 1998},
 publisher = {CSLI Publications},
 year      = {2000},
 isbn      = {1-57586-271-9},
 url       = {Ganzinger+Hustadt+Meyer+Schmidt@AiML1998.pdf},
 abstract = {This paper presents a resolution decision procedure for
 transitive propositional modal logics. The procedure combines the
 relational translation method with an ordered chaining calculus
 designed to avoid unnecessary inferences with transitive relations. We
 show the logics K4, KD4 and S4 can be transformed into a bounded class
 of well-structured clauses closed under ordered resolution and
 negative chaining.} 
}

{"_id":"XYgzAqWzAXg6zvMQQ","bibbaseid":"ganzinger-hustadt-meyer-schmidt-aresolutionbaseddecisionprocedureforextensionsofk4-2000","author_short":["Ganzinger, H.","Hustadt, U.","Meyer, C.","Schmidt, R. A."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Harald"],"propositions":[],"lastnames":["Ganzinger"],"suffixes":[]},{"firstnames":["Ullrich"],"propositions":[],"lastnames":["Hustadt"],"suffixes":[]},{"firstnames":["Christoph"],"propositions":[],"lastnames":["Meyer"],"suffixes":[]},{"firstnames":["Renate","A."],"propositions":[],"lastnames":["Schmidt"],"suffixes":[]}],"title":"A Resolution-Based Decision Procedure for Extensions of K4","year":"2000","pages":"225-246","editor":[{"firstnames":["Michael"],"propositions":[],"lastnames":["Zakharyaschev"],"suffixes":[]},{"firstnames":["Krister"],"propositions":[],"lastnames":["Segerberg"],"suffixes":[]},{"firstnames":["Maarten"],"propositions":["de"],"lastnames":["Rijke"],"suffixes":[]},{"firstnames":["Heinrich"],"propositions":[],"lastnames":["Wansing"],"suffixes":[]}],"booktitle":"Advances in Modal Logic 2, papers from the second workshop on \"Advances in Modal logic,\" held in Uppsala, Sweden, 1998","publisher":"CSLI Publications","isbn":"1-57586-271-9","url":"Ganzinger+Hustadt+Meyer+Schmidt@AiML1998.pdf","abstract":"This paper presents a resolution decision procedure for transitive propositional modal logics. The procedure combines the relational translation method with an ordered chaining calculus designed to avoid unnecessary inferences with transitive relations. We show the logics K4, KD4 and S4 can be transformed into a bounded class of well-structured clauses closed under ordered resolution and negative chaining.","bibtex":"@inproceedings{Ganzinger+Hustadt+Meyer+Schmidt@AiML1998,\n author = {Harald Ganzinger and\n Ullrich Hustadt and\n Christoph Meyer and\n Renate A. Schmidt},\n title = {A Resolution-Based Decision Procedure for Extensions of K4},\n year = {1998},\n pages = {225-246},\n editor = {Michael Zakharyaschev and\n Krister Segerberg and\n Maarten de Rijke and\n Heinrich Wansing},\n booktitle = {Advances in Modal Logic 2, papers from the second workshop\n on \"Advances in Modal logic,\" held in Uppsala, Sweden, 1998},\n publisher = {CSLI Publications},\n year = {2000},\n isbn = {1-57586-271-9},\n url = {Ganzinger+Hustadt+Meyer+Schmidt@AiML1998.pdf},\n abstract = {This paper presents a resolution decision procedure for\n transitive propositional modal logics. The procedure combines the\n relational translation method with an ordered chaining calculus\n designed to avoid unnecessary inferences with transitive relations. We\n show the logics K4, KD4 and S4 can be transformed into a bounded class\n of well-structured clauses closed under ordered resolution and\n negative chaining.} \n}\n\n\n","author_short":["Ganzinger, H.","Hustadt, U.","Meyer, C.","Schmidt, R. A."],"editor_short":["Zakharyaschev, M.","Segerberg, K.","de Rijke, M.","Wansing, H."],"key":"Ganzinger+Hustadt+Meyer+Schmidt@AiML1998","id":"Ganzinger+Hustadt+Meyer+Schmidt@AiML1998","bibbaseid":"ganzinger-hustadt-meyer-schmidt-aresolutionbaseddecisionprocedureforextensionsofk4-2000","role":"author","urls":{"Paper":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Ganzinger+Hustadt+Meyer+Schmidt@AiML1998.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj","FgmYE34DdKWThg2dR"],"keywords":[],"search_terms":["resolution","based","decision","procedure","extensions","ganzinger","hustadt","meyer","schmidt"],"title":"A Resolution-Based Decision Procedure for Extensions of K4","year":2000}