# Careful with the resolution theorem prover

One finds readily the following resolution theorem prover on the internet,
it now says it runs with Scryer Prolog, but my suspicion is that it also

Resolution Calculus for Propositional Logic

``````pl_resolvent( ... ) :-
select(Q, As0, As),
select(not(Q), Bs0, Bs),
append(As, Bs, Rs0),
``````

https://www.metalevel.at/logic/plres.pl

Mentioned here:

Theorem Proving with Prolog
https://www.metalevel.at/prolog/theoremproving

But when one reads the fine print by Markus Triska, it says for propositional logic.
Not sure whether it works for first order logic (FOL) as well? There is a FOL
example {p(X), p(Y)} and {~p(U), ~p(V)} which hints that a full flegded resolution

theorem prover needs also “factoring”. Making a resolution theorem prover
only complete when it implements resolution step with factoring:

Φ
ψ
-------------------------------
((Φ’-{φ})∪(Ψ’-{¬ψ}))σ
where τ is a variable renaming on Φ
where Φ’ is a factor of Φτ and φ∈Φ’
where Ψ’ is a factor of Ψ and ¬ψ∈Ψ’
where σ=mgu(φ, ψ)
Introduction to Logic - Chapter 14

Any full fledged resolution theorem provers around written in
Prolog that can be run for example with the SWI-Prolog system?