The Maude Resolution Theorem Prover (RTP)

The Maude Resolution Theorem Prover (RTP) is a refutationally complete resolution theorem prover for order-sorted first order logic without equality, and with support for associative and commutative function symbols.

The tool has been written entirely in Maude and is in fact an executable specification in rewriting logic of the formal inference system that it implements. The fact that rewriting logic is reflective, and that Maude efficiently supports reflective rewriting logic computations is systematically exploited in the design of the tool.

 On the installation and use

The tool is entirely written in Maude. The latest version RTP works on Maude 2.6. To load the tool one just needs to load the Maude code of the RTP. If maude is your Maude executable, and the RTP program is in file rtp.maude, and everything is in the same directory or in your path, you can load the RTP tool as follows:

\$ maude rtp
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.6 built: Dec 10 2010 11:12:39
Sat May 7 21:19:03 2011
Maude>

The RTP implementation offers two commands:
• red ?(<input>) tries to saturate the input by ordered-resolution and displays a tuple with the result (of sort State), if terminating. The first component of the returned tuple is a minimal Herbrand (modulo renamming of variables) if the input does not yield a contradiction, the second and third components are indexed versions of the first component, the fourth component indicates if a contradiction was found (with the keyword empty -> empty) or if no contradiction was found (with the keyword empty), and the fifth component with the total number of resultion steps.

• red !(<input>) similar to the previous command, but less verbose. It returns a pair corresponding to the fourth and fifth components of its verbose version.
In order to use the RTP, a user needs to specify the signature of the theory and the input problem (a set of clauses in the given signature):
• The order-sorted signature of the theory is specified by a functional module in Maude that imports functional module PRED-BASE, available from RTP. The user can define sorts and function symbols using Maude's order-signature syntax. Predicates are symbols with sort Atom, defined in module PRED-BASE. The user provides the total ordering for function symbols and the total ordering for predicate symbols using Maude's metadata operator attribute with a natural number as parameter: the greater the number, the higher the priority of the function/predicate symbol.

• The input problem is specified by a functional module that imports the signature of the theory and functional module RTP. Constant USER-MODULE-NAME needs to be set with the name (as a quoted identifier) of the functional module defining the signature of the theory. The input is a comma-separated set of clausual sequents. A clausal sequent is pair Γ -> Δ, where Γ and Δ are comma-separated sets of atoms, with identity emtpy, in the signature of the theory.

For instance, we can consider the following example:

fmod DAVIS-PUTNAM is
pr PRED-BASE .
sort S .
op F : S S -> Atom [metadata "1"] .
op G : S S -> Atom [metadata "2"] .
op f-z : S S -> S [metadata "1"] .
endfm

fmod TEST is
inc RTP .
inc DAVIS-PUTNAM .
eq USER-MODULE-NAME = 'DAVIS-PUTNAM .
op input : S S -> ClSeqMagma .
vars X Y : S.
eq input(X,Y)
= (((empty -> F(X,Y)),
(F(Y,f-z(X,Y)),F(f-z(X,Y),f-z(X,Y)) -> G(X,Y)),
(F(Y,f-z(X,Y)),F(f-z(X,Y),f-z(X,Y)),G(X,f-z(X,Y)),G(f-z(X,Y),f-z(X,Y)) -> empty))) .
endfm

The RTP finds a proof for example DAVIS-PUTNAM in 7 resolution steps:

Maude> red ?(input(x:S,y:S)) .
reduce in TEST : ?(((empty -> F(x:S, y:S)), (((G(x:S, f-z(x:S, y:S)), G(f-z(
x:S, y:S), f-z(x:S, y:S))), F(f-z(x:S, y:S), f-z(x:S, y:S))), F(y:S, f-z(
x:S, y:S)) -> empty), (F(y:S, f-z(x:S, y:S)), F(f-z(x:S, y:S), f-z(x:S,
y:S)) -> G(x:S, y:S)))) .
rewrites: 3386 in 77ms cpu (84ms real) (43664 rewrites/second)
result State:
[ ("F",'_->_['empty.AtomMagma,'F['x:S,'y:S]],empty -> F(x:S, y:S)), ("F",'_->_[
'F['V#2:S,'f-z['V#1:S,'V#2:S]],'empty.AtomMagma],F(V#2:S, f-z(V#1:S,
V#2:S)) -> empty), ("G",'_->_['empty.AtomMagma,'G['V#2:S,'V#1:S]],empty ->
G(V#2:S, V#1:S)),
"F" : (empty -> F(x:S, y:S)) |-> ((empty).AtomMagma -> (empty).AtomMagma)[F(
x:S, y:S)], "F" : (F(V#2:S, f-z(V#1:S, V#2:S)) -> empty) |-> empty, "G" : (
empty -> G(V#2:S, V#1:S)) |-> ((empty).AtomMagma -> (empty).AtomMagma)[G(
V#2:S, V#1:S)],
"F" : (F(V#2:S, f-z(V#1:S, V#2:S)) -> empty) |-> ([F(V#2:S, f-z(V#1:S,
V#2:S))]empty -> empty),
empty -> empty,
7 ]

Or, equivalently, using the non-verbose command:

Maude> red !(input(x:S,y:S)) .
reduce in TEST : !(((empty -> F(x:S, y:S)), (((G(x:S, f-z(x:S, y:S)), G(f-z(
x:S, y:S), f-z(x:S, y:S))), F(f-z(x:S, y:S), f-z(x:S, y:S))), F(y:S, f-z(
x:S, y:S)) -> empty), (F(y:S, f-z(x:S, y:S)), F(f-z(x:S, y:S), f-z(x:S,
y:S)) -> G(x:S, y:S)))) .
rewrites: 3388 in 77ms cpu (84ms real) (43981 rewrites/second)
result State: [empty -> empty,7]