@INCOLLECTION{Hustadt+Schmidt@SAT2000,
 AUTHOR        = {Hustadt, U. and Schmidt, R. A.},
 TITLE         = {Using Resolution for Testing Modal Satisfiability and Building Models},
 BOOKTITLE     = {{SAT2000}: Highlights of Satisfiability Research in the Year 2000},
 PAGES         = {459-483},
 PUBLISHER     = {IOS Press},
 PADDRESS      = {Amsterdam},
 YEAR          = {2000},
 EDITOR        = {Gent, I. and van Maaren, H. and Walsh, T.},
 SERIES        = {Frontiers in Artificial Intelligence and Applications},
 VOLUME        = {63},
 ISBN          = {1-58603-061-2},
 URL           = {Hustadt+Schmidt@SAT2000.pdf},
 ABSTRACT      = {This paper presents a translation-based resolution
 decision procedure for the multi-modal logic K_m(\cap,\cup,\conv)
 defined over families of relations closed under intersection, union
 and converse. The relations may satisfy certain additional frame
 properties. Different from previous resolution decision procedures
 which are based on ordering refinements our procedure is based on a
 selection refinement, the derivations of which correspond to
 derivations of tableaux or sequent proof systems. This procedure has
 the advantage that it can be used both as a satisfiability checker and
 a model builder. We show that tableaux and sequent-style proof systems
 can be polynomially simulated with our procedure. Furthermore, the
 finite model property follows for a number of extended modal logics.} 
}

{"_id":"X7vXWKcbjyjEg4jrT","bibbaseid":"hustadt-schmidt-usingresolutionfortestingmodalsatisfiabilityandbuildingmodels-2000","author_short":["Hustadt, U.","Schmidt, R. A."],"bibdata":{"bibtype":"incollection","type":"incollection","author":[{"propositions":[],"lastnames":["Hustadt"],"firstnames":["U."],"suffixes":[]},{"propositions":[],"lastnames":["Schmidt"],"firstnames":["R.","A."],"suffixes":[]}],"title":"Using Resolution for Testing Modal Satisfiability and Building Models","booktitle":"SAT2000: Highlights of Satisfiability Research in the Year 2000","pages":"459-483","publisher":"IOS Press","paddress":"Amsterdam","year":"2000","editor":[{"propositions":[],"lastnames":["Gent"],"firstnames":["I."],"suffixes":[]},{"propositions":["van"],"lastnames":["Maaren"],"firstnames":["H."],"suffixes":[]},{"propositions":[],"lastnames":["Walsh"],"firstnames":["T."],"suffixes":[]}],"series":"Frontiers in Artificial Intelligence and Applications","volume":"63","isbn":"1-58603-061-2","url":"Hustadt+Schmidt@SAT2000.pdf","abstract":"This paper presents a translation-based resolution decision procedure for the multi-modal logic K_m(∩,∪,o̧nv) defined over families of relations closed under intersection, union and converse. The relations may satisfy certain additional frame properties. Different from previous resolution decision procedures which are based on ordering refinements our procedure is based on a selection refinement, the derivations of which correspond to derivations of tableaux or sequent proof systems. This procedure has the advantage that it can be used both as a satisfiability checker and a model builder. We show that tableaux and sequent-style proof systems can be polynomially simulated with our procedure. Furthermore, the finite model property follows for a number of extended modal logics.","bibtex":"@INCOLLECTION{Hustadt+Schmidt@SAT2000,\n AUTHOR = {Hustadt, U. and Schmidt, R. A.},\n TITLE = {Using Resolution for Testing Modal Satisfiability and Building Models},\n BOOKTITLE = {{SAT2000}: Highlights of Satisfiability Research in the Year 2000},\n PAGES = {459-483},\n PUBLISHER = {IOS Press},\n PADDRESS = {Amsterdam},\n YEAR = {2000},\n EDITOR = {Gent, I. and van Maaren, H. and Walsh, T.},\n SERIES = {Frontiers in Artificial Intelligence and Applications},\n VOLUME = {63},\n ISBN = {1-58603-061-2},\n URL = {Hustadt+Schmidt@SAT2000.pdf},\n ABSTRACT = {This paper presents a translation-based resolution\n decision procedure for the multi-modal logic K_m(\\cap,\\cup,\\conv)\n defined over families of relations closed under intersection, union\n and converse. The relations may satisfy certain additional frame\n properties. Different from previous resolution decision procedures\n which are based on ordering refinements our procedure is based on a\n selection refinement, the derivations of which correspond to\n derivations of tableaux or sequent proof systems. This procedure has\n the advantage that it can be used both as a satisfiability checker and\n a model builder. We show that tableaux and sequent-style proof systems\n can be polynomially simulated with our procedure. Furthermore, the\n finite model property follows for a number of extended modal logics.} \n}\n","author_short":["Hustadt, U.","Schmidt, R. A."],"editor_short":["Gent, I.","van Maaren, H.","Walsh, T."],"key":"Hustadt+Schmidt@SAT2000","id":"Hustadt+Schmidt@SAT2000","bibbaseid":"hustadt-schmidt-usingresolutionfortestingmodalsatisfiabilityandbuildingmodels-2000","role":"author","urls":{"Paper":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Hustadt+Schmidt@SAT2000.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"incollection","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj","FgmYE34DdKWThg2dR"],"keywords":[],"search_terms":["using","resolution","testing","modal","satisfiability","building","models","hustadt","schmidt"],"title":"Using Resolution for Testing Modal Satisfiability and Building Models","year":2000}