resolution based theorem prover for temporal logic

Question

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!

Answer 1

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.