The Inverse Method Implements the Automata Approach for Modal Satisfiability

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Toggle side column

The Inverse Method Implements the Automata Approach for Modal Satisfiability

Franz BaaderFranz Baader,  Stephan TobiesStephan Tobies
Franz Baader, Stephan Tobies
The Inverse Method Implements the Automata Approach for Modal Satisfiability
Proceedings of the International Joint Conference on Automated Reasoning IJCAR'01, volume 2083 of Lecture Notes in Artificial Intelligence, 92-106, 2001. Springer
  • KurzfassungAbstract
    This paper ties together two distinct strands in automated reasoning: the tableau- and the automata-based approach. It shows that the inverse tableau method can be viewed as an implementation of the automata approach. This is of interest to automated deduction because Voronkov recently showed that the inverse method yields a viable decision procedure for the modal logic K.
  • Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
The final publication is available at Springer.
@inproceedings{ BaaderTobies-IJCAR,
  author = {F. {Baader} and S. {Tobies}},
  booktitle = {Proceedings of the International Joint Conference on Automated Reasoning {IJCAR'01}},
  pages = {92--106},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Artificial Intelligence},
  title = {The Inverse Method Implements the Automata Approach for Modal Satisfiability},
  volume = {2083},
  year = {2001},
}