@INPROCEEDINGS{Hustadt+Schmidt@SFTP1998,
 AUTHOR    = {Hustadt, U. and Schmidt, R. A.},
 TITLE     = {Issues of Decidability for Description Logics in the Framework of Resolution},
 EDITOR    = {Caferra, R. and Salzer, G.},
 PAGES     = {192-206},
 PMONTH    = jan,
 PYEAR     = {2000},
 CYEAR     = {1998},
 YEAR      = {1999},
 BOOKTITLE = {Automated Deduction in Classical and Non-Classical Logics},
 SERIES    = {LNAI},
 VOLUME    = {1761},
 PUBLISHER = {Springer},
 URL       = {Hustadt+Schmidt@SFTP1998.pdf},
 URL       = {http://dx.doi.org/10.1007/3-540-46508-1_13},
 ABSTRACT  = {We describe two methods on the basis of which efficient
 resolution decision procedures can be developed for a range of
 description logics. The first method uses an ordering restriction and
 applies to the description logic ALB, which extends ALC with the top
 role, full role negation, role intersection, role disjunction, role
 converse, domain restriction, range restriction, and role hierarchies.
 The second method is based solely on a selection restriction and
 applies to reducts of ALB without the top role and role negation. The
 latter method can be viewed as a polynomial simulation of familiar
 tableaux-based decision procedures. It can also be employed for
 automated model generation.}
}

{"_id":"TprXEmPgGZpPxEtkq","bibbaseid":"hustadt-schmidt-issuesofdecidabilityfordescriptionlogicsintheframeworkofresolution-1999","author_short":["Hustadt, U.","Schmidt, R. A."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Hustadt"],"firstnames":["U."],"suffixes":[]},{"propositions":[],"lastnames":["Schmidt"],"firstnames":["R.","A."],"suffixes":[]}],"title":"Issues of Decidability for Description Logics in the Framework of Resolution","editor":[{"propositions":[],"lastnames":["Caferra"],"firstnames":["R."],"suffixes":[]},{"propositions":[],"lastnames":["Salzer"],"firstnames":["G."],"suffixes":[]}],"pages":"192-206","pmonth":"January","pyear":"2000","cyear":"1998","year":"1999","booktitle":"Automated Deduction in Classical and Non-Classical Logics","series":"LNAI","volume":"1761","publisher":"Springer","url":"http://dx.doi.org/10.1007/3-540-46508-1_13","abstract":"We describe two methods on the basis of which efficient resolution decision procedures can be developed for a range of description logics. The first method uses an ordering restriction and applies to the description logic ALB, which extends ALC with the top role, full role negation, role intersection, role disjunction, role converse, domain restriction, range restriction, and role hierarchies. The second method is based solely on a selection restriction and applies to reducts of ALB without the top role and role negation. The latter method can be viewed as a polynomial simulation of familiar tableaux-based decision procedures. It can also be employed for automated model generation.","bibtex":"@INPROCEEDINGS{Hustadt+Schmidt@SFTP1998,\n AUTHOR = {Hustadt, U. and Schmidt, R. A.},\n TITLE = {Issues of Decidability for Description Logics in the Framework of Resolution},\n EDITOR = {Caferra, R. and Salzer, G.},\n PAGES = {192-206},\n PMONTH = jan,\n PYEAR = {2000},\n CYEAR = {1998},\n YEAR = {1999},\n BOOKTITLE = {Automated Deduction in Classical and Non-Classical Logics},\n SERIES = {LNAI},\n VOLUME = {1761},\n PUBLISHER = {Springer},\n URL = {Hustadt+Schmidt@SFTP1998.pdf},\n URL = {http://dx.doi.org/10.1007/3-540-46508-1_13},\n ABSTRACT = {We describe two methods on the basis of which efficient\n resolution decision procedures can be developed for a range of\n description logics. The first method uses an ordering restriction and\n applies to the description logic ALB, which extends ALC with the top\n role, full role negation, role intersection, role disjunction, role\n converse, domain restriction, range restriction, and role hierarchies.\n The second method is based solely on a selection restriction and\n applies to reducts of ALB without the top role and role negation. The\n latter method can be viewed as a polynomial simulation of familiar\n tableaux-based decision procedures. It can also be employed for\n automated model generation.}\n}\n\n","author_short":["Hustadt, U.","Schmidt, R. A."],"editor_short":["Caferra, R.","Salzer, G."],"key":"Hustadt+Schmidt@SFTP1998","id":"Hustadt+Schmidt@SFTP1998","bibbaseid":"hustadt-schmidt-issuesofdecidabilityfordescriptionlogicsintheframeworkofresolution-1999","role":"author","urls":{"Paper":"http://dx.doi.org/10.1007/3-540-46508-1_13"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj"],"keywords":[],"search_terms":["issues","decidability","description","logics","framework","resolution","hustadt","schmidt"],"title":"Issues of Decidability for Description Logics in the Framework of Resolution","year":1999}