@INPROCEEDINGS{Schmidt+Hustadt@CADE2003,
 AUTHOR    = {Schmidt, R. A. and Hustadt, U.},
 YEAR      = {2003},
 TITLE     = {A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae},
 XEDITOR   = {Baader, F.},
 BOOKTITLE = {Proceedings of the 19th International Conference on Automated Deduction 
 (CADE-19) [Miami Beach, USA, July/August 2003]},
 SERIES    = {Lecture Notes in Artificial Intelligence},
 VOLUME    = {2741},
 PUBLISHER = {Springer},
 PAGES     = {412-426},
 URL       = {Schmidt+Hustadt@CADE2003.pdf},
 URL       = {http://dx.doi.org/10.1007/978-3-540-45085-6_36},
 ABSTRACT = {In this paper we present a translation principle, called the
 \emph{axiomatic translation}, for reducing propositional modal logics
 with background theories, including triangular properties such as 
 transitivity, Euclideanness and functionality, to decidable logics.
 The goal of the axiomatic translation principle is to find simplified 
 theories, which capture the inference problems in the original theory, 
 but in a way that is more amenable to automation and easier to deal with 
 by existing theorem provers.
 The principle of the axiomatic translation is conceptually very simple
 and can be largely automated.
 Soundness is automatic under reasonable assumptions, and termination of
 ordered resolution is easily achieved, but the non-trivial part of the 
 approach is proving completeness.}
}

{"_id":"rHnKaLuBSmA7ZDo9w","bibbaseid":"schmidt-hustadt-aprincipleforincorporatingaxiomsintothefirstordertranslationofmodalformulae-2003","author_short":["Schmidt, R. A.","Hustadt, U."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Schmidt"],"firstnames":["R.","A."],"suffixes":[]},{"propositions":[],"lastnames":["Hustadt"],"firstnames":["U."],"suffixes":[]}],"year":"2003","title":"A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae","xeditor":"Baader, F.","booktitle":"Proceedings of the 19th International Conference on Automated Deduction (CADE-19) [Miami Beach, USA, July/August 2003]","series":"Lecture Notes in Artificial Intelligence","volume":"2741","publisher":"Springer","pages":"412-426","url":"http://dx.doi.org/10.1007/978-3-540-45085-6_36","abstract":"In this paper we present a translation principle, called the \\emphaxiomatic translation, for reducing propositional modal logics with background theories, including triangular properties such as transitivity, Euclideanness and functionality, to decidable logics. The goal of the axiomatic translation principle is to find simplified theories, which capture the inference problems in the original theory, but in a way that is more amenable to automation and easier to deal with by existing theorem provers. The principle of the axiomatic translation is conceptually very simple and can be largely automated. Soundness is automatic under reasonable assumptions, and termination of ordered resolution is easily achieved, but the non-trivial part of the approach is proving completeness.","bibtex":"@INPROCEEDINGS{Schmidt+Hustadt@CADE2003,\n AUTHOR = {Schmidt, R. A. and Hustadt, U.},\n YEAR = {2003},\n TITLE = {A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae},\n XEDITOR = {Baader, F.},\n BOOKTITLE = {Proceedings of the 19th International Conference on Automated Deduction \n (CADE-19) [Miami Beach, USA, July/August 2003]},\n SERIES = {Lecture Notes in Artificial Intelligence},\n VOLUME = {2741},\n PUBLISHER = {Springer},\n PAGES = {412-426},\n URL = {Schmidt+Hustadt@CADE2003.pdf},\n URL = {http://dx.doi.org/10.1007/978-3-540-45085-6_36},\n ABSTRACT = {In this paper we present a translation principle, called the\n \\emph{axiomatic translation}, for reducing propositional modal logics\n with background theories, including triangular properties such as \n transitivity, Euclideanness and functionality, to decidable logics.\n The goal of the axiomatic translation principle is to find simplified \n theories, which capture the inference problems in the original theory, \n but in a way that is more amenable to automation and easier to deal with \n by existing theorem provers.\n The principle of the axiomatic translation is conceptually very simple\n and can be largely automated.\n Soundness is automatic under reasonable assumptions, and termination of\n ordered resolution is easily achieved, but the non-trivial part of the \n approach is proving completeness.}\n}\n","author_short":["Schmidt, R. A.","Hustadt, U."],"key":"Schmidt+Hustadt@CADE2003","id":"Schmidt+Hustadt@CADE2003","bibbaseid":"schmidt-hustadt-aprincipleforincorporatingaxiomsintothefirstordertranslationofmodalformulae-2003","role":"author","urls":{"Paper":"http://dx.doi.org/10.1007/978-3-540-45085-6_36"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj","FgmYE34DdKWThg2dR"],"keywords":[],"search_terms":["principle","incorporating","axioms","first","order","translation","modal","formulae","schmidt","hustadt"],"title":"A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae","year":2003}