Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
424215 | Electronic Notes in Theoretical Computer Science | 2008 | 15 Pages |
Abstract
The better known methods of semantic tableaux for deciding satisfiability in propositional linear temporal logic generate graphs in addition to classical trees. The test of satisfaction is made from the graph and it does not correspond with the application of rules in any calculus for PLTL. We present here a new method of semantic tableaux without using additional graphs. The method is based on a new complete finitary sequent calculus for PLTL which allows us to incorporate all the information in a tree. This approach makes our tableaux better suited for completely automatic theorem proving.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics