Resolution Theorem Prover in Lisp

Page 1 of 1

0 Replies - 963 Views - Last Post: 05 November 2015 - 08:42 PM

#1 SamDc

Reputation: 0
• Posts: 1
• Joined: 05-November 15

Resolution Theorem Prover in Lisp

Posted 05 November 2015 - 08:42 PM

I have to Implement in LISP a theorem prover based on propositional resolution. I assume that the axioms and the negation of the theorem to prove are already in clause form.
Each clause will be represented as a list of two elements.
The first element is a list containing the propositions from the left hand side of the clause.
The second element is a list containing the propositions from the right hand side of the clause.
That is, the clause
A1,...,Am <- B1,...,Bn,X
should be represented as
((A1 ... Am) (B1 ... Bn X))
In particular
A1, A2 <-
should be represented as
((A1 A2) ())

The main function of your system should be called "prove", and should have only one parameter, as shown in the following:
(defun prove (lc)
;; lc is a list of at least two propositional clauses representing
;; a set of axioms and the negation of the theorem to prove.

The function "prove" will print the message "A contradiction had been found" and will return NIL, or it will print the message "There is no contradiction in the given set of clauses" and will return T, as illustrated in the following examples:
(prove '( ((C D)(A)) ((A D E)()) (()(A C)) (()(D)) (()(E)) ))
NIL
(prove '( ((A)(B C)) ((B)()) (()(A)) (©()) ))
NIL
(prove '( ((A)(B C)) ((B)()) (©()) ))
There is no contradiction in the given set of clauses
T

Here is what I got so far, but it is not working the way it is supposed to. Please help:
```;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;The function checks whether or not there is a pair of literals
;in the two clauses that are unifiable. If not, return 'fail, otherwise
;resolve the two clauses
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(Defun Check (C1 C2)

(let ((i1 0) (i2 0) (L1 Nil) (L2 Nil))

(setf resolvent 'unsolved)
(do ((i1 0 (setf i1 (+ 1 i1))))  ; check every literal of C1
((= i1 (length C1)))

(if (Not (eq resolvent 'unsolved))
(return resolvent))		;complementary and unifiable
;literals found	and resolved.
;Get out of the function

(setf L1 (nth i1 C1))           ; check every literal of C2
(do ((i2 0 (setf i2 (+ 1 i2))))
((= i2 (length C2)))

(setf L2 (nth i2 C2))
(if (and (complementary-lits L1 L2) ;these two clauses are
; resolvable
(Not (eql (setf Subst (Unifiable L1 L2)) 'Fail)))

(let ()
(setf C1cp (copy C1))	    ;To remain C1, C2 unchanged,
(setf C2cp (copy C2))	    ;apply resolving on their copies
(setf resolvent (Resolve C1cp C2cp i1 i2 Subst))

; Record the resolve by making a new node
(setf newnode (make-Node  :resolvent C
:clause1   C1
:clause2   C2
:subst     Subst))
; Add the new node to the list
(setf record (append record (list newnode)))
(return resolvent))
)))

resolvent))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;This function tests whether two literals are complementary
;i.e. one positive and one negative literal with the same predicate
;a positive literal is of the form (P t1 .. tn), and a negative
;literal is of the form (~ P t1 .. tn) where ti is a FO term
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(Defun complementary-lits (L1 L2)
(cond
((or (atom L1) (atom L2)) Nil)
((eql '~ (car L1)) (eql (cadr L1) (car L2)))
((eql '~ (car L2)) (eql (cadr L2) (car L1)))
(t Nil)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;This is the main procedure which proves the theorem by using
;resolution.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(Defun Prove (Clauses)

(let ((i1 0) (i2 0) (C1 Nil) (C2 Nil) )
(setf NumOfPre (- (length Clauses) 1)) ;to remember the number of axioms input

;choose the first clause from the end of the list
(do ((i1 (- (length Clauses) 1) (setf i1 (- i1 1))))
((= i1 (- NumOfPre 1)))
;inner loop over Clauses for
;the choice of C1
(setf C1 (nth i1 Clauses))      ;C1 is from the set of newly
;generated clauses

;choose the second clause from
;the beginning of the list
(do ((i2 0 (setf i2 (+ 1 i2))))
((= i2 NumOfPre))
; outer loop over Clauses for the
; choice of C2

(setf C2 (nth i2 Clauses))  ;C2 is from the set of axioms

;check the two clauses to see
;whether we can resolve them
(setf result (Check C1 C2))
;if the newly derived resolvent
;in the Clauses, we just go to the
;to Clauses and starts all over again
(if (and (Not (eq 'unsolved result))
(Not (member result Clauses :test 'equal)))
;get out of the function
(return-from Prove result))))

(return-from prove 'Fail)))   ; no clause can resolve, can't prove.

```

This post has been edited by macosxnerd101: 05 November 2015 - 09:02 PM
Reason for edit:: Added code tags and moved thread to Functional Programming

Is This A Good Question/Topic? 0

Page 1 of 1

 .related ul { list-style-type: circle; font-size: 12px; font-weight: bold; } .related li { margin-bottom: 5px; background-position: left 7px !important; margin-left: -35px; } .related h2 { font-size: 18px; font-weight: bold; } .related a { color: blue; }