For relational monadic formulas (the Lowenheim 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.
CITATION STYLE
Wernhard, C. (2015). Second-order quantifier elimination on relational monadic formulas – a basic method and some less expected applications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9323, pp. 253–269). Springer Verlag. https://doi.org/10.1007/978-3-319-24312-2_18
Mendeley helps you to discover research relevant for your work.