Common Lisp Resolution Refutation framework.
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.gitignore
LICENSE
README.md
clause.lisp

README.md

Clause

Clause is a Resolution Refutation framework written in Common Lisp.

Application

James Whitcomb Riley once said: When I see a bird that walks like a duck and swims like a duck and quacks like a duck, I call that bird a duck.

A mallard is a bird walks like a duck, quacks like a duck and swims like a duck. Is it a duck?

is-bird(mallard)
walks-like-duck(mallard)
swims-like-duck(mallard)
quacks-like-duck(mallard)
(is-bird(X)&walks-like-duck(X)&swims-like-duck(X)&quacks-like-duck(X))==>is-duck(X)

To prove: is-duck(mallard)

> (load "clause.lisp")
> (setq is-bird (deffact 'is-bird 'mallard))
#<FACT :FUNC IS-BIRD :PARAMS (MALLARD)>
> (setq walks-like-duck (deffact 'walks-like-duck 'mallard))#<FACT :FUNC WALKS-LIKE-DUCK :PARAMS (MALLARD)>
> (setq swims-like-duck (deffact 'swims-like-duck 'mallard))#<FACT :FUNC SWIMS-LIKE-DUCK :PARAMS (MALLARD)>
> (setq quacks-like-duck (deffact 'quacks-like-duck 'mallard))#<FACT :FUNC QUACKS-LIKE-DUCK :PARAMS (MALLARD)>
> (setq facts (defwff 'and (list (deffact 'is-bird (var 'x)) (deffact 'walks-like-duck (var 'x)) (deffact 'swims-like-duck (var 'x)) (deffact 'quacks-like-duck (var 'x)))))
#<WFF :OPERATOR AND
  :WFFS
  (#<FACT :FUNC IS-BIRD :PARAMS (#<VAR :X X>)> #<FACT :FUNC WALKS-LIKE-DUCK :PARAMS (#<VAR :X X>)>
   #<FACT :FUNC SWIMS-LIKE-DUCK :PARAMS (#<VAR :X X>)> #<FACT :FUNC QUACKS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>
> (setq implications (deffact 'is-duck (var 'x)))
#<FACT :FUNC IS-DUCK :PARAMS (#<VAR :X X>)>
[28]> (setq rule (defrule facts implications))
#<RULE
  :FACTS
  #<WFF :OPERATOR AND
    :WFFS
    (#<FACT :FUNC IS-BIRD :PARAMS (#<VAR :X X>)> #<FACT :FUNC WALKS-LIKE-DUCK :PARAMS (#<VAR :X X>)>
     #<FACT :FUNC SWIMS-LIKE-DUCK :PARAMS (#<VAR :X X>)> #<FACT :FUNC QUACKS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>
  :IMPLICATIONS #<FACT :FUNC IS-DUCK :PARAMS (#<VAR :X X>)>
  :CNF
  #<WFF :OPERATOR OR
    :WFFS
    (#<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC IS-BIRD :PARAMS (#<VAR :X X>)>)>
     #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC WALKS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>
     #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC SWIMS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>
     #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC QUACKS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)> #<FACT :FUNC IS-DUCK :PARAMS (#<VAR :X X>)>)>>
> (setq goal (deffact 'is-duck 'mallard))
#<FACT :FUNC IS-DUCK :PARAMS (MALLARD)>
> (resolve (list is-bird walks-like-duck swims-like-duck quacks-like-duck) (list rule) goal)
Resolvent: #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC IS-DUCK :PARAMS (MALLARD)>)>
Substitution: NIL

Resolvent: 
#<WFF :OPERATOR OR
  :WFFS
  (#<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC IS-BIRD :PARAMS (#<VAR :X X>)>)>
   #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC WALKS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>
   #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC SWIMS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>
   #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC QUACKS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>)>
Substitution: (MALLARD)

Resolvent: 
#<WFF :OPERATOR OR
  :WFFS
  (#<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC WALKS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>
   #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC SWIMS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>
   #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC QUACKS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>)>
Substitution: (MALLARD)

Resolvent: 
#<WFF :OPERATOR OR
  :WFFS
  (#<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC SWIMS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>
   #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC QUACKS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>)>
Substitution: (MALLARD)

Resolvent: #<WFF :OPERATOR OR :WFFS (#<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC QUACKS-LIKE-DUCK :PARAMS (#<VAR :X X>)>)>)>
Substitution: (MALLARD)

Resolvent: #<WFF :OPERATOR OR :WFFS NIL>
Substitution: (MALLARD)

((MALLARD) (MALLARD) (MALLARD) (MALLARD) (MALLARD))

It looks like a mallard is, indeed, a duck!

Sample problem breakdown

 EE-Student(Charley) 
 Hrs-Taken(122,Charley) 
 {EE-Student(X)&Hrs-Taken(Y,X)&Greaterp(Y,120)}==>EE-Sr(X) 

Deduce that Charley is an EE Senior.
Facts
> (setq ee-student (deffact 'ee-student 'charley))
#<FACT :FUNC EE-STUDENT :PARAMS (CHARLEY)>
> (setq hrs-taken (deffact 'hrs-taken 122 'charley))
#<FACT :FUNC HRS-TAKEN :PARAMS (122 CHARLEY)>
> (setq greaterp (deffact 'greaterp 122 120))
#<FACT :FUNC GREATERP :PARAMS (122 120)>
Rules
> (setq facts (defwff 'and (list (deffact 'ee-student (var 'x))
(deffact 'hrs-taken (var 'y) (var 'x)) (deffact 'greaterp (var 'y) 120))))
#<WFF :OPERATOR AND
  :WFFS
  (#<FACT :FUNC EE-STUDENT :PARAMS (#<VAR :X X>)> #<FACT :FUNC HRS-TAKEN :PARAMS (#<VAR :X Y> #<VAR :X X>)>
   #<FACT :FUNC GREATERP :PARAMS (#<VAR :X Y> 120)>)>
> (setq implications (deffact 'ee-sr (var 'x)))
#<FACT :FUNC EE-SR :PARAMS (#<VAR :X X>)>
> (setq rule (defrule facts implications))
#<RULE
  :FACTS
  #<WFF :OPERATOR AND
    :WFFS
    (#<FACT :FUNC EE-STUDENT :PARAMS (#<VAR :X X>)> #<FACT :FUNC HRS-TAKEN :PARAMS (#<VAR :X Y> #<VAR :X X>)>
     #<FACT :FUNC GREATERP :PARAMS (#<VAR :X Y> 120)>)>
  :IMPLICATIONS #<FACT :FUNC EE-SR :PARAMS (#<VAR :X X>)>
  :CNF
  #<WFF :OPERATOR OR
    :WFFS
    (#<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC EE-STUDENT :PARAMS (#<VAR :X X>)>)>
     #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC HRS-TAKEN :PARAMS (#<VAR :X Y> #<VAR :X X>)>)>
     #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC GREATERP :PARAMS (#<VAR :X Y> 120)>)>
     #<FACT :FUNC EE-SR :PARAMS (#<VAR :X X>)>)>>
Goals
> (setq goal (deffact 'ee-sr 'charley))
#<FACT :FUNC EE-SR :PARAMS (CHARLEY)>
Resolution Refutation
> (resolve (list ee-student hrs-taken greaterp) (list rule) goal)
Resolvent: #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC EE-SR :PARAMS (CHARLEY)>)>
Substitution: NIL

Resolvent: 
#<WFF :OPERATOR OR
  :WFFS
  (#<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC EE-STUDENT :PARAMS (#<VAR :X X>)>)>
   #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC HRS-TAKEN :PARAMS (#<VAR :X Y> #<VAR :X X>)>)>
   #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC GREATERP :PARAMS (#<VAR :X Y> 120)>)>)>
Substitution: (CHARLEY)

Resolvent: 
#<WFF :OPERATOR OR
  :WFFS
  (#<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC HRS-TAKEN :PARAMS (#<VAR :X Y> #<VAR :X X>)>)>
   #<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC GREATERP :PARAMS (#<VAR :X Y> 120)>)>)>
Substitution: (CHARLEY)

Resolvent: #<WFF :OPERATOR OR :WFFS (#<WFF :OPERATOR NOT :WFFS (#<FACT :FUNC GREATERP :PARAMS (#<VAR :X Y> 120)>)>)>
Substitution: (CHARLEY 122)

Resolvent: #<WFF :OPERATOR OR :WFFS NIL>
Substitution: (122)

((CHARLEY) (CHARLEY) (CHARLEY 122) (122))