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).

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F. Orejas

[Electronic Edition]

**[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]

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro

In

[prole07b.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