|
| | | | |
| | | |
| Stat |
Members: 3644
Articles: 2'499'343
Articles rated: 2609
17 April 2024 |
|
| | | | |
|
Article overview
| |
|
|
The Inverse Method Implements the Automata Approach for Modal Satisfiability | | Franz Baader
; Stephan Tobies
; | | Date: |
22 Dec 2004 | | Subject: | Logic in Computer Science | cs.LO | | Abstract: | Tableaux-based decision procedures for satisfiability of modal and description logics behave quite well in practice, but it is sometimes hard to obtain exact worst-case complexity results using these approaches, especially for EXPTIME-complete logics. In contrast, automata-based approaches often yield algorithms for which optimal worst-case complexity can easily be proved. However, the algorithms obtained this way are usually not only worst-case, but also best-case exponential: they first construct an automaton that is always exponential in the size of the input, and then apply the (polynomial) emptiness test to this large automaton. To overcome this problem, one must try to construct the automaton "on-the-fly" while performing the emptiness test. In this paper we will show that Voronkov’s inverse method for the modal logic K can be seen as an on-the-fly realization of the emptiness test done by the automata approach for K. The benefits of this result are two-fold. First, it shows that Voronkov’s implementation of the inverse method, which behaves quite well in practice, is an optimized on-the-fly implementation of the automata-based satisfiability procedure for K. Second, it can be used to give a simpler proof of the fact that Voronkov’s optimizations do not destroy completeness of the procedure. We will also show that the inverse method can easily be extended to handle global axioms, and that the correspondence to the automata approach still holds in this setting. In particular, the inverse method yields an EXPTIME-algorithm for satisfiability in K w.r.t. global axioms. | | Source: | arXiv, cs.LO/0412101 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser claudebot
|
| |
|
|
|
|
News, job offers and information for researchers and scientists:
| |
REGISTER