<p>Your translation goes into Presburger arithmetic, which is decidable. </p>

<p>You could take your translated formula, do quantifier elimination on it, and then hand it over to a proof-producing SMT solver. Since pretty much all SMT solvers are (fancy extensions of) DPLL, I would guess you can turn those proofs into resolution proofs without too much difficulty. </p>

<p>I'm pretty sure that CVC4 can directly give you the resolution proofs, and would be surprised if Z3 couldn't.</p>

CC BY-SA 3.0
2017-05-06T01:26:43.370Z
This is somewhat OT, but only the arithmetic part goes to Presburger. There are still the uninterpreted predicates (eg p(i), q(i)) that arise from the translation of the temporal propositions, p, q,... which take you back into FOL. Although these predicates are monadic, I am not sure whether the combination with the binary < predicate retains decidability
Motorhead
CC BY-SA 3.0
2017-05-04T10:09:01.573Z
2017-05-04T10:09:01.573Z
Neel Krishnaswami
<p>I am looking at implementing a a resolution-based theorem prover for propositional linear temporal logic (PLTL) (as opposed to a model checker). The ones out there (by Fisher et. al. and others) are complex on account have having to deal directly with temporal resolution. So looking for something quick and good enough for now (I'm not too concerned with retaining decidability or its efficiency at this point), I am considering the translation of PLTL into first order logic (FOL). The propositions are turned into unary predicates over numbers. This translation is well known and described in several places (eg Fisher)</p>

<p>p → p(i)</p>

<p>$\circ$p → p(i + 1)</p>

<p>$\diamond$p → ∃j. (j ≥ i) ∧ p(j)</p>

<p>$\Box$p → ∀j. (j ≥ i) ⇒ p(j)</p>

<p>The problem is that these first order formulas have distinguished symbols > and succ (as well as equality) - alternatively the FOL formulas are meant to be interpreted w.r.t. a natural number line which corresponds to the timeline of PLTL. Is there a good way to implement a resolution prover that can take into account or provide these symbols with their required interpretation? More specifically:</p>

<ul>
<li>For example, would it work to add the theory of the successor function to the translation and go from there? </li>
<li>How would I handle equality? (paramodulation?)</li>
<li>I'd like to be able to implement this in Prolog but you can't encode equational theories like subsets of arithmetic in Prolog, but would Prolog's built-in arithmetic operators perhaps suffice?</li>
</ul>

<p>Thanks!</p>

CC BY-SA 3.0
2017-04-28T09:07:52.893Z
If you translate to FOL, why not try an SMT solver like Z3?
Radu GRIGore
CC BY-SA 3.0
2017-05-01T19:53:33.013Z
@ Radu: Due to some other constraints, I specifically am looking for a resolution prover. Besides, SMT solvers aren't complete for FOL, they make a best effort for certain fragments of FOL.
Motorhead
<automated-theorem-proving><temporal-logic><linear-temporal-logic><logic-programming><resolution>
resolution based theorem prover for temporal logic
Motorhead
# resolution based theorem prover for temporal logic

(Asked by: username_0 on 2017-04-27)

I am looking at implementing a a resolution-based theorem prover for propositional linear temporal logic (PLTL) (as opposed to a model checker). The ones out there (by Fisher et. al. and others) are complex on account have having to deal directly with temporal resolution. So looking for something quick and good enough for now (I'm not too concerned with retaining decidability or its efficiency at this point), I am considering the translation of PLTL into first order logic (FOL). The propositions are turned into unary predicates over numbers. This translation is well known and described in several places (eg Fisher)

p → p(i)

$\circ$p → p(i + 1)

$\diamond$p → ∃j. (j ≥ i) ∧ p(j)

$\Box$p → ∀j. (j ≥ i) ⇒ p(j)

The problem is that these first order formulas have distinguished symbols > and succ (as well as equality) - alternatively the FOL formulas are meant to be interpreted w.r.t. a natural number line which corresponds to the timeline of PLTL. Is there a good way to implement a resolution prover that can take into account or provide these symbols with their required interpretation? More specifically:

* For example, would it work to add the theory of the successor function to the translation and go from there?
* How would I handle equality? (paramodulation?)
* I'd like to be able to implement this in Prolog but you can't encode equational theories like subsets of arithmetic in Prolog, but would Prolog's built-in arithmetic operators perhaps suffice?

Thanks!

**Tags:** automated-theorem-proving, temporal-logic, linear-temporal-logic, logic-programming, resolution
> **Comments:**
> **username_1**: If you translate to FOL, why not try an SMT solver like Z3?  
> **username_0**: @ Radu: Due to some other constraints, I specifically am looking for a resolution prover. Besides, SMT solvers aren't complete for FOL, they make a best effort for certain fragments of FOL.  

---

## 1 answers

### Answer by username_2 on 2017-05-04. Score: 2

Your translation goes into Presburger arithmetic, which is decidable.

You could take your translated formula, do quantifier elimination on it, and then hand it over to a proof-producing SMT solver. Since pretty much all SMT solvers are (fancy extensions of) DPLL, I would guess you can turn those proofs into resolution proofs without too much difficulty.

I'm pretty sure that CVC4 can directly give you the resolution proofs, and would be surprised if Z3 couldn't.

> **Comments:**
> **username_0**: This is somewhat OT, but only the arithmetic part goes to Presburger. There are still the uninterpreted predicates (eg p(i), q(i)) that arise from the translation of the temporal propositions, p, q,... which take you back into FOL. Although these predicates are monadic, I am not sure whether the combination with the binary < predicate retains decidability  

---

