Systematic Semantic Tableaux for PLTL

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.