Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications

From International Center for Computational Logic

Toggle side column

Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications

Christoph WernhardChristoph Wernhard
Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications


Christoph Wernhard
Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications
In Hans de Nivelle, eds., Automated Reasoning with Analytic Tableaux and Related Methods: 24th International Conference, TABLEAUX 2015, volume 9323 of LLNCS (LNAI), 249-265, 2015. Springer
  • 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.
  • Projekt:Project: SOA-VBQP
  • Forschungsgruppe:Research Group: Wissensverarbeitung
The final publication is available at Springer.
@inproceedings{W2015,
  author    = {Christoph Wernhard},
  title     = {Second-Order Quantifier Elimination on Relational Monadic
               Formulas {\textendash} A Basic Method and Some Less Expected
               Applications},
  editor    = {Hans de Nivelle},
  booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods:
               24th International Conference, {TABLEAUX} 2015},
  series    = {LLNCS (LNAI)},
  volume    = {9323},
  publisher = {Springer},
  year      = {2015},
  pages     = {249-265}
}