Techreport3022: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Christoph Wernhard (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
Christoph Wernhard (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
||
| Zeile 11: | Zeile 11: | ||
{{Publikation Details | {{Publikation Details | ||
|Abstract=For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, forgetting and projection, always succeeds. The decidability proof for this class by Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. We reconstruct Behmann's method, relate it to the modern DLS elimination algorithm and show some applications where the essential monadicity becomes apparent only at second sight. In particular, deciding ALCOQH knowledge bases, elimination in DL-Lite knowledge bases, and the justification of the success of elimination methods for Sahlqvist formulas. | |Abstract=For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, forgetting and projection, always succeeds. The decidability proof for this class by Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. We reconstruct Behmann's method, relate it to the modern DLS elimination algorithm and show some applications where the essential monadicity becomes apparent only at second sight. In particular, deciding ALCOQH knowledge bases, elimination in DL-Lite knowledge bases, and the justification of the success of elimination methods for Sahlqvist formulas. | ||
|Link=http://www.wv.inf.tu-dresden.de/Publications/2015/report-15-04.pdf | |Link=http://www.wv.inf.tu-dresden.de/Publications/2015/report-15-04.pdf | ||
|Projekt=SOA-VBQP | |Projekt=SOA-VBQP | ||
|Forschungsgruppe=Wissensverarbeitung | |Forschungsgruppe=Wissensverarbeitung | ||
}} | }} | ||
Version vom 21. August 2015, 08:22 Uhr
Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications (Extended Version)
Christoph WernhardChristoph Wernhard
Christoph Wernhard
Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications (Extended Version)
Technical Report, TU Dresden, volume Knowledge Representation and Reasoning 15-04, 2015
Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications (Extended Version)
Technical Report, TU Dresden, volume Knowledge Representation and Reasoning 15-04, 2015
- KurzfassungAbstract
For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, forgetting and projection, always succeeds. The decidability proof for this class by Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. We reconstruct Behmann's method, relate it to the modern DLS elimination algorithm and show some applications where the essential monadicity becomes apparent only at second sight. In particular, deciding ALCOQH knowledge bases, elimination in DL-Lite knowledge bases, and the justification of the success of elimination methods for Sahlqvist formulas. - Weitere Informationen unter:Further Information: Link
- Projekt:Project: SOA-VBQP
- Forschungsgruppe:Research Group: WissensverarbeitungKnowledge Representation and Reasoning
@techreport{W2015,
author = {Christoph Wernhard},
title = {Second-Order Quantifier Elimination on Relational Monadic
Formulas {\textendash} A Basic Method and Some Less Expected
Applications (Extended Version)},
institution = {TU Dresden},
year = {2015}
}
