Sciweavers

Share
ENTCS
2008

Systematic Semantic Tableaux for PLTL

9 years 1 months ago
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.
Joxe Gaintzarain, Montserrat Hermo, Paqui Lucio, M
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Joxe Gaintzarain, Montserrat Hermo, Paqui Lucio, Marisa Navarro
Comments (0)
books