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
Copyright 1997-2010 SRI International
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: