The Inverse Method Implements the Automata Approach for Modal Satisfiability

Details The Inverse Method Implements the Automata Approach for Modal Satisfiability The Inverse Method Implements the Automata Approach for Modal Satisfiability

2004-12-22

arxiv.org/abs/cs/0412101v1

Computer Science

Logic in Computer Science

A short version of this report has appeared at the First International Joint Conference on Automated Reasoning, IJCAR 2001

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

The Inverse Method Implements the Automata Approach for Modal Satisfiability does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with The Inverse Method Implements the Automata Approach for Modal Satisfiability, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and The Inverse Method Implements the Automata Approach for Modal Satisfiability will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-542948