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?