caa a22 4500 463187296 CHVBK 20180406164857.0 cr unu---uuuuu 170326e20070401xx s 000 0 eng 10.1007/s10472-007-9051-8 doi (NATIONALLICENCE)springer-10.1007/s10472-007-9051-8 Sofronie-Stokkermans Viorica Max-Planck-Institut für Informatik, Stuhlsatzenhausweg 85, D-66123, Saarbrücken, Germany aut Automated theorem proving by resolution in non-classical logics [Elektronische Daten] [Viorica Sofronie-Stokkermans] This paper is an overview of a variety of results, all centered around a common theme, namely embedding of non-classical logics into first order logic and resolution theorem proving. We present several classes of non-classical logics, many of which are of great practical relevance in knowledge representation, which can be translated into tractable and relatively simple fragments of classical logic. In this context, we show that refinements of resolution can often be used successfully for automated theorem proving, and in many interesting cases yield optimal decision procedures. Springer Science+Business Media B.V., 2007 Non-classical logics nationallicence Automated theorem proving nationallicence Representation theorems nationallicence Annals of Mathematics and Artificial Intelligence Springer Netherlands 49/1-4(2007-04-01), 221-252 1012-2443 49:1-4<221 2007 49 10472 https://doi.org/10.1007/s10472-007-9051-8 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10472-007-9051-8 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Sofronie-Stokkermans Viorica Max-Planck-Institut für Informatik, Stuhlsatzenhausweg 85, D-66123, Saarbrücken, Germany aut NATIONALLICENCE 773 0- Annals of Mathematics and Artificial Intelligence Springer Netherlands 49/1-4(2007-04-01), 221-252 1012-2443 49:1-4<221 2007 49 10472 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer