CS 537 Assignment
Logical Reasoning for Propositions
------------------------------------------------------------------------------------------------------------------------------------------
Implement Wang's propositional theorem prover for WFF as a CLIPS application.
Help for the Assignment:
The
following codes have to be modified and then put together to work.
* I
have added several new functions you may want to use. You may find
some of these functions repeated or not useful…..
Deftemplates:
(deftemplate left (multislot
leftside))
(deftemplate right
(multislot rightside))
(deftemplate is-it-valid
(slot valid))
List
of the facts:
(deffacts factsList
(is-it-valid (valid FALSE))
(left (leftside a , b ))
(right (rightside b , c))
)
product: A function which returns
the first Atom (I named it product) from
a phrase (left or right side of the WFF).
(deffunction product
($?phrase) ;return the first product of the phrase
(bind ?comma (first$ (create$ , ,)))
(bind $?result x x) ; just to bind the variable with something
to start
(bind ?result (delete-member$ $?result $?result))
(if (> (length$ $?phrase) 0) then
(bind ?comp (first$ $?phrase))
(while (and (neq ?comma ?comp) (> (length$ $?phrase)
0))
(bind ?result $?result ?comp)
(bind ?phrase (rest$ $?phrase))
(bind ?comp (first$ $?phrase))
)
)
$?result
)
product-del: A function which returns
the rest of a phrase (left or right side
of the WFF) after deleting the first atom (product) from it.
(deffunction product-del
($?phrase) ; delete the first product of the phrase
(if (> (length$ $?phrase) 0) then
(bind $?fproduct(product $?phrase))
(bind ?len (length$ $?fproduct))
;(printout t "length: " ?len " phrase: " ?phrase crlf)
(bind $?phrase (delete$ $?phrase 1 ?len))
(if (> (length$ $?phrase) 0) then
(bind $?phrase (delete$ $?phrase 1 1))
)
)
$?phrase
;(printout t $?phrase)
)
parant: Returns TRUE if [ … ].
(deffunction parant
($?phrase) ;returns true if ( .... )
(bind ?stock 0)
(bind ?open (first$ (create$ [ [)))
(bind ?close (first$ (create$ ] ])))
(bind ?interrupt FALSE)
(bind ?flag FALSE)
(if (and (> (length$ $?phrase) 2) (eq (first$ $?phrase)
?open)) then
(while (> (length$ $?phrase) 0) do
(bind ?compare (first$ $?phrase))
(if (<> ?stock 0) then
(bind ?flag TRUE)
)
(if (eq ?compare ?open) then
(bind ?stock (+ ?stock 1))
)
(if (eq ?compare ?close) then
(bind ?stock (- ?stock 1))
)
(if (and (eq ?flag TRUE) (= ?stock 0) (>
(length$ $?phrase) 1) ) then
(bind ?interrupt TRUE)
)
(bind $?phrase (rest$ $?phrase))
)
(if (and (eq ?stock 0) (eq ?interrupt FALSE)) then
TRUE
else
FALSE
)
else
(if (and (> (length$ $?phrase) 2) (neq (first$
$?phrase) ?open)) then
FALSE
else
(if (< (length$ $?phrase) 3) then
TRUE
)
)
)
)
parent-balance: A function which check to
see if the number of “[“ is equal to
the number of “]”. This is useful when you want to find an atom.
(deffunction parant-balance
($?phrase); check to see if the # of "[" is equal to the # of
"]"
(bind ?stock 0)
(bind ?open (first$ (create$ [ [)))
(bind ?close (first$ (create$ ] ])))
(while (> (length$ $?phrase) 0) do
(bind ?compare (first$ $?phrase))
(if (eq ?compare ?open) then
(bind ?stock (+ ?stock 1))
)
(if (eq ?compare ?close) then
(bind ?stock (- ?stock 1))
)
(bind $?phrase (rest$ $?phrase))
)
(if (eq ?stock 0) then
TRUE
else
FALSE
)
)
drop-parant: if [ … ] then drop the
parenthesis
(deffunction
drop-parant($?phrase); if [ .... ] then drops the parenthesis
(bind ?open (first$ (create$ [ [)))
(if (> (length$ $?phrase) 2) then
(if (and (parant $?phrase) (eq ?open (first$ $?phrase)))
then
(bind ?phrase (delete$ ?phrase 1 1))
(bind ?phrase (delete$ ?phrase (length$ $?phrase)
(length$ $?phrase)))
)
)
$?phrase
)
drop-unnecessary-parant: A function which drops
extra parenthesis from the left and the right side.
(defrule
drop-unnecessary-parant; from letf and right phrases
?left <- (left (leftside $?leftside1))
?right <- (right (rightside $?rightside1))
?nnot <- (drop-unnec-parant-control) ;This is a control fact which you insert
(from other rules) to get this rule to fire.
=>
(bind ?righttemp (delete-member$ $?rightside1 $?rightside1))
(bind ?lefttemp (delete-member$ $?leftside1 $?leftside1))
(bind ?left-is-changed FALSE)
(bind ?right-is-changed FALSE)
(while (> (length$ $?leftside1) 0) do
(bind $?leftcomp (product $?leftside1))
(bind $?leftside1 (product-del $?leftside1))
(bind ?leftcomp (drop-parant $?leftcomp))
(if (> (length$ ?lefttemp) 0) then
(bind $?lefttemp $?lefttemp , $?leftcomp)
else (bind
$?lefttemp $?lefttemp $?leftcomp)
)
)
(while (> (length$ $?rightside1) 0) do
(bind $?rightcomp (product $?rightside1))
(bind $?rightside1 (product-del $?rightside1))
(bind ?rightcomp (drop-parant $?rightcomp))
(if (> (length$ ?righttemp) 0) then
(bind $?righttemp $?righttemp , $?rightcomp)
else (bind
$?righttemp $?righttemp $?rightcomp)
)
)
(retract ?left ?right ?nnot)
(assert (left (leftside $?lefttemp)))
(assert (right (rightside $?righttemp)))
)
not-not : if you have two #s that means no #. If you have three #s that mean
just one # and so on.
(defrule not-not
?left <- (left (leftside $?leftside1))
?right <- (right (rightside $?rightside1))
?nnot <- (not-not-control); this is a control fact which
should be insert anytime you want this rule be fired.
=>
(bind $?lefttemp (delete-member$ $?leftside1 $?leftside1))
(bind $?righttemp (delete-member$ $?rightside1 $?rightside1))
(bind ?nnno (first$ (create$ # #)))
(while (> (length$ $?leftside1) 0) do
(bind $?leftcomp (product $?leftside1))
(bind $?leftside1 (product-del $?leftside1))
(bind ?counter 0)
(while (eq ?nnno (first$ $?leftcomp)) do
(bind ?leftcomp (rest$ $?leftcomp))
(bind ?counter (+ ?counter 1))
)
(if (oddp ?counter) then
(bind ?lefttemp $?lefttemp , # $?leftcomp)
else
(bind ?lefttemp $?lefttemp , $?leftcomp)
)
)
(while (> (length$ $?rightside1) 0) do
(bind $?rightcomp (product $?rightside1))
(bind $?rightside1 (product-del $?rightside1))
(bind ?counter 0)
(while (eq ?nnno (first$ $?rightcomp)) do
(bind ?rightcomp (rest$ $?rightcomp))
(bind ?counter (+ ?counter 1))
)
(if (oddp ?counter) then
(bind ?righttemp $?righttemp , # $?rightcomp)
else
(bind ?righttemp $?righttemp , $?rightcomp)
)
)
(retract ?left ?right ?nnot)
(if (> (length$ $?lefttemp) 0) then
(bind $?lefttemp
(delete$ ?lefttemp 1 1))
)
(if (> (length$ $?righttemp) 0) then
(bind $?righttemp (delete$ ?righttemp 1 1))
)
(assert (left (leftside $?lefttemp)))
(assert (right (rightside $?righttemp)))
)
Here is W1:
(defrule w1
?left <- (left (leftside $?leftside1))
?right <- (right (rightside $?rightside1))
?val <- (is-it-valid (valid FALSE))
=>
(bind ?identical FALSE)
(while (and (> (length$ $?leftside1) 0) (eq ?identical
FALSE)) do
(bind $?leftcomp (product $?leftside1))
(bind $?leftside1 (product-del $?leftside1))
(bind $?righttemp $?rightside1)
(while (and (> (length$ $?righttemp) 0) (eq ?identical
FALSE))
(bind $?rightcomp (product $?righttemp))
(if (eq $?leftcomp $?rightcomp) then
(bind ?identical TRUE)
)
(bind $?righttemp (product-del $?righttemp))
)
)
(if (eq ?identical FALSE) then
(printout t "It's not a Tautology." crlf)
else (printout t
"It's a Tautology." crlf)
(retract ?val )
(assert (is-it-valid (valid TRUE)))
)
)
(defrule w2a
?left <- (left (leftside $?leftside1))
?right <- (right (rightside $?rightside1))
?val <- (is-it-valid (valid FALSE))
=>
(bind ?identical FALSE)
(bind ?T-true (product (create$ T , T)))
(bind ?F-false(product (create$ F , F)))
(while (or (> (length$ $?rightside1) 0) (> (length$
$?leftside1) 0) )
(if (> (length$ $?rightside1) 0) then
(bind ?rightcomp (product $?rightside1))
(if (eq ?rightcomp ?T-true) then
(bind ?identical TRUE)
)
(bind ?rightside1 (product-del $?rightside1))
)
(if (> (length$ $?leftside1) 0) then
(bind ?leftcomp (product $?leftside1))
(if (eq ?leftcomp ?F-false) then
(bind ?identical TRUE)
)
(bind ?leftside1 (product-del $?leftside1))
)
)
(if (eq ?identical FALSE) then
;(printout t "It's not a Tautology." crlf)
(retract ?val)
(assert (is-it-valid (valid TRUE))
else ;(printout t "It's a Tautology." crlf)
)
)
W4a:
(defrule w4a ;presence of
"not = #" at left side
?left <- (left (leftside $?leftside1))
?right <- (right (rightside $?rightside1))
?val <- (is-it-valid (valid FALSE))
=>
(bind ?is-changed FALSE)
(bind $?lefttemp (delete-member$ $?leftside1 $?leftside1))
(bind ?nnno (first$ (create$ # #)))
(while (> (length$ $?leftside1) 0) do
(bind $?leftcomp (product $?leftside1))
(bind $?leftside1 (product-del $?leftside1))
(if (eq ?nnno (first$ $?leftcomp)) then
(bind ?leftcomp (rest$ $?leftcomp))
(if (or (= (length$ $?leftcomp) 1) (parant
$?leftcomp)) then
(bind ?leftcomp (drop-parant $?leftcomp))
(if (> (length$ ?rightside1) 0) then
(bind $?rightside1 $?rightside1 ,
$?leftcomp)
else (bind
$?rightside1 $?rightside1 $?leftcomp)
)
(bind ?is-changed TRUE)
else
(bind ?lefttemp $?lefttemp , # $?leftcomp)
)
else
(bind ?lefttemp $?lefttemp , $?leftcomp)
)
)
(if (> (length$ $?lefttemp) 0) then
(bind $?lefttemp (delete$ ?lefttemp 1 1))
)
(if (eq ?is-changed TRUE) then
(retract ?left ?right)
(assert (left (leftside $?lefttemp)))
(assert (right (rightside $?rightside1)))
)
(assert (not-not-control) (drop-unnec-parant-control))
)
W7a:
(defrule w7a ; left side
?left <- (left (leftside $?leftside1))
?val <- (is-it-valid (valid FALSE))
=>
(bind $?lefttemp (delete-member$ $?leftside1 $?leftside1))
(bind ?nnno (nth$ 1 (create$ => =>)))
(bind ?it-is-changed FALSE)
(while (> (length$ $?leftside1) 0) do
(bind $?leftcomp (product $?leftside1))
(bind $?leftside1 (product-del $?leftside1))
(bind ?position 0)
(bind ?flag FALSE)
;(bind ?position (member$ ?nnno $?leftcomp))
;(printout t "position: " ?position crlf)
(while (and (< ?position (length$ $?leftcomp)) (eq
?flag FALSE)) do
(if (eq (nth$ ?position $?leftcomp) ?nnno) then
(bind ?thisside (subseq$ $?leftcomp 1 (-
?position 1)))
(bind ?thatside (subseq$ $?leftcomp (+
?position 1) (length$ $?leftcomp)))
;(printout t "thisside: " ?thisside
" thatside: " ?thatside crlf)
(if (and (eq (parant-balance $?thisside)
TRUE) (eq (parant-balance $?thatside) TRUE)) then
(bind $?lefttemp $?lefttemp , #
$?thisside v $?thatside)
(bind ?flag TRUE)
(bind ?it-is-changed TRUE)
)
)
(bind ?position (+ ?position 1))
)
(if (eq ?flag FALSE) then
(bind ?lefttemp $?lefttemp , $?leftcomp)
)
)
(if (eq ?it-is-changed TRUE) then
(retract ?left)
(assert (drop-unnec-parant-control))
; (assert (w5a) (w5b) (w4a) (w4b) ) At this point you need to be sure that w5a,
w5b, w4a, w4b be fired….
(if (> (length$ $?lefttemp) 0) then
(bind $?lefttemp (delete$ ?lefttemp 1 1))
)
(assert (left (leftside $?lefttemp)))
)
)