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.
TRS tool is a work in progress, current version: September 2012
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
In this example, we can see that the set of clauses consists of the two premises and the negated conclusion.
In general, the formula and its set of clauses are equisatisfiable.
4. Run the algorithm SR. In the Algorithm Control menu you can choose to show the execution either step by step (by clicking Next Step) or word by word (by clicking Next world) or all steps until termination (by clicking Run).
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 its 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).
[2] Dual Systems of Tableaux and Sequents for PLTL
J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F. Orejas
The Journal of Logic and Algebraic Programming
78, pp. 701–722, (2009)
[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
Computer Science Logic : 21 International Workshop, CSL 2007,
Lausanne, Switzerland, September 11-15, 2007.
Lecture Notes in Computer Science 4646, (2007), pp. 481–495
Springer-Verlag
[csl07.pdf]
[BibTeX]
[Electronic Edition]
This work has been partially supported by the Spanish Project TIN2007-66523 and the Basque Project LoRea GIU07/35.
Last Modified: May 2013