4
$\begingroup$

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!

$\endgroup$
  • $\begingroup$ If you translate to FOL, why not try an SMT solver like Z3? $\endgroup$ – Radu GRIGore Apr 28 '17 at 9:07
  • $\begingroup$ @ 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. $\endgroup$ – S.N. May 1 '17 at 19:53
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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 $\endgroup$ – S.N. May 6 '17 at 1:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.