Skip to main content

2001 | OriginalPaper | Buchkapitel

The Inverse Method Implements the Automata Approach for Modal Satisfiability

verfasst von : Franz Baader, Stephan Tobies

Erschienen in: Automated Reasoning

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Metadaten
Titel
The Inverse Method Implements the Automata Approach for Modal Satisfiability
verfasst von
Franz Baader
Stephan Tobies
Copyright-Jahr
2001
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/3-540-45744-5_8