The Inverse Method Implements the Automata Approach for Modal Satisfiability
From International Center for Computational Logic
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
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
@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},
}
