TRS: A
Resolution-based Theorem Prover for Propositional Linear Temporal Logic
TRS: A
Resolution-based Theorem Prover for Propositional Linear Temporal Logic TRS tool is a theorem prover for the Propositional Linear-time Temporal Logic, based on a resolution method called TRS (Temporal Resolution System).
TRS tool allows you to:
a) translate any PLTL-formula into a set of temporal clauses (in normal form CNF) and
b) test the satisfiability for any set of temporal clauses.
It includes a collection of examples for easy first testing.
The application kernel is developed in the programming language Scala.
The system architecture follows a client-server design based on web technologies.
The application is implemented using Google's infrastructure.
YOU CAN ACCESS BY: http://trs-tool.appspot.com/
The Temporal Resolution System (TRS) consists of four main rules named (Res), (R Fix), (U Fix) and (U Set).
In addition to a resolution-like rule (Res), this system includes three fixpoint rules – (R Fix), (U Fix) and (U Set) – for decomposing temporal literals. (R Fix) and (U Fix) are based in the usual inductive definition of the temporal operators R (release) and U (until), whereas (U Set) is based on a more complex inductive definition of U that is the basis of our approach.
Moreover, TRS also uses some simplification and subsumption rules in order to, respectively, simplify and delete clauses during the process.
There is also a rule (Unnext) that obtains, from a given set of clauses, another set of clauses for the next moment of time.
TRS tool implements a concrete algorithm called SR (Systematic Resolution) which is presented in [1]. It basically consists in a set of iterations. In each iteration all these rules are applied (in a concrete order) obtaining new clauses that can be seen as the resolvents of the given clauses. To pass to the following iteration (corresponding to the next moment of time) the rule (Unnext) is applied.
Let us prove the theorem with the two premises:
<>p (in some moment of time the proposition p holds) and
[] (p -> 0p) (it always happens that: if p holds in a moment then in the next moment p also holds)
and the conclusion:
<> [] p (in some moment of time, [] p holds; that is, from some moment the proposition p holds forever).
This theorem can be proven by testing that the negated formula ¬ ( (<>p ^ [] (p -> 0p)) -> (<> [] p) ) is unsatisfiable.
In the following we show how to proceed to test it in TRS tool.
1. Introduce the formula ¬ ( (<>p ^ [] (p -> 0p)) -> (<> [] p) ) either by hand or by File --> Load
2. Click the button Analyze. An error message appears when parsing fails. Otherwise:
3. The system shows the set of clauses (CNF) for the given formula:
Initial clauses
1. <>p
2. [] (¬p v 0p)
3. [] <>p
The set of clauses and the formula are equisatisfiable.
4. Run the algorithm SR, either by clicking Next Step in the Algorithm Control menu, to show each step one to one, or by clicking Next Iteration, to show all steps in each iteration.
5. In this example the process finishes with a set of clauses containing the empty clause (written false), since the initial set of clauses is unsatisfiable.
6. In the examples where the initial formula (or equivalently the set of clauses) is satisfiable, the algorithm finishes with a set of clauses not containing the empty clause.
7. Once the whole process is done, we may want to have a look only to same steps (for instance, those steps when (U set) rule was applied). To do this, we can use the filters in the Algorithm Control menu (by clicking only the box Uset).
[1] Invariant-Free Clausal Temporal Resolution
J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F. Orejas[2] Dual Systems of Tableaux and Sequents for PLTL
J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F. Orejas[JLAP09.pdf] [BibTeX] [Electronic Edition]
[3] A Cut-Free and Invariant-Free Sequent Calculus for PLTL
J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro,
and F.Orejas
In J. Duparc and T.A. Henzinger (Eds.): Computer
Science Logic : 21 International Workshop, CSL 2007,
16th Annual Conference of the EACSL, Lausanne,
Switzerland, September 11-15, 2007, LNCS 4646,
pp. 481–495, Springer-Verlag Berlin Heidelberg, 2007.
[csl07.pdf] [BibTeX] [Electronic Edition]
[4] Systematic Semantic Tableaux for PLTL
J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro
This work has been partially supported by the Spanish Project TIN2007-66523 and the Basque Project LoRea GIU07/35.
Last Modified: June 2011