Deutsch
 
Benutzerhandbuch Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae

MPG-Autoren
/persons/resource/persons45401

Schmidt,  Renate A.
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44660

Hustadt,  Ullrich
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44050

Baader,  Franz
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Schmidt, R. A., & Hustadt, U. (2003). A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. In Automated deduction, CADE-19: 19th International Conference on Automated Deduction (pp. 412-426). Berlin, Germany: Springer.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-2C3F-4
Zusammenfassung
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.