Hi,
I have written this piece of lisp hoping to write a linear resolution
proof "thingy".
Basically, I have a knowledge base, KB, add the negated goal and an
arbitrary g, then try to prove it via a depth first search. My goals are
of the form "a" or "not a".
Can anyone suggest what is wrong in my code? Here is the problem I am
having.
(Thanks in advance )
I am having dificulties writing this depth first search. Basically, at
each level of recursion, the search tries to match a literal in the
current resolvant (initially the negated goal) with an opposing literal
in some clause in the KB or on the stack. The search terminates with the
empty clause.
I am using Freelisp from Harlequin, and it parses the program but when
it executes it come with this error:
> CL-USER 14 > (s)
>
> (INPUT GOAL TO SOLVE) a
>
> (THIS IS CAR OF STACK)
> (NOT)
> Error: the function STACK applied to arguments (((NOT ((NOT A) G))
>
> (NOT A)) ((A) ((NOT A) C))) is undefined.
>
Here is the code: ("s" is the main function, "sx" is the search itself)
--- begin here ---
> ;Written by Before C.
> ;linear resolution
> ;;;;;;;;;;;;;;;;;;
> ;set the knowledge base to an initial value
> (setq KB '((a) ((not a) c)))
> ;(setq G '())
>
> ;(defun read-try (arg)
> ; (list (+ arg (read)) (read)))
>
> (defun s ()
> (print '(Input goal to Solve))
> (setq goal (read))
> (setq ngoal (list 'not goal))
> (setq goal (list goal))
> (setq goal_or_g (list ngoal 'g))
> (setq KB (cons goal_or_g KB))
> (setq stack ngoal)
> (setq resolvant (list ngoal))
> (print '(This is car of stack))
> (print (list (car stack)))
> (sx stack resolvant KB)
>
> (print '(Stack is))
> (print stack)
> )
>
> (defun sx (stack resolvant KB)
> (setq item (car KB))
> (setq nitem (list 'not item))
> (setq stack (cons item stack))
> (cond ((mymember nitem resolvant)
> (setq sol stack)
> ); else
> (t
> ;(
> (setq resolvant (cons nitem resolvant))
> (setq KB (cdr KB))
> (sx (stack resolvant KB))
> ;)
> );t
> ); cond
>
>
>
> (print '(This is the original stack))
> ; (list (setq stack (cdr stack)))
> ); end sx
>
> (defun mymember (E L)
> (cond
> ((equal L nil) nil)
> ((equal E (car L)) t)
> (t (mymember E (cdr L)))))
>
> ;eof
>
"Before C." <······@pathfindermail.com> writes:
> > Error: the function STACK [...] is undefined.
What the system is trying to tell you is that it has encountered
"stack" where it expected a function name.
[...]
> > (sx (stack resolvant KB))
Indeed. You probably ment (sx stack resolvant KB) here.
Stig Hemmer.
Stig Hemmer wrote: [...]
> > > (sx (stack resolvant KB))
>
> Indeed. You probably ment (sx stack resolvant KB) here.
>
Yup. Thanks. It's fixed. It works now...Now the problem is that it does
not really perform like a depth first search...
Do you have any suggestions regarding a [better] depth first search
algorithm?
Cheers,
-Before C.