## Playing first-order logic

Richard Suchenwirth 2002-05-19 - First-Order Logic (FOL) is an extension to predicate logic, where quantifiers ("universal": for all or "existential": there exists — see forall) can bind variables in sentences. (I derive most of my wisdom on FOL from [1 ] which I also recommend for additional reading.) In the Tcl implementation, I however took some liberties to make this Pentecost fun project easier. Functions and predicates are written as Polish(Tcl)-style lists:

` fun(x) ==> {fun x} ; pred(x,y,z) ==> {pred x y z}`

Likewise, "connectives" (operators) are pulled to front position:

` P ^ (Q v ~R) ==> {and P {or Q {not R}}}`

and quantifiers braced, for a uniform interface:

``` (Ax)(Ey)(Et) loves(x,y,t) ==> all x {ex y {ex t {loves x y t}}}
# "Everybody loves somebody sometimes"```

A typical use case is: given a knowledge base (a set of FOL sentences), prove another sentence. My simple starting example ("all cats eat fish; cats eat what they like; Felix is a cat"):

``` prove {
all x {impl {cat x} {likes x Fish}}
all x {all y {impl {and {cat x} {likes x y}} {eats x y}}}
cat Felix
} {eats Felix Fish}```

could however not be proven yet...

For notation convenience, sentences in a FOL knowledge base are delimited with newlines. The first task is to convert this rather "rich" language to an equivalent simpler one, where the knowledge base is a list of clauses (implicitly joined with "and") and each clause is a list of (possibly negated) simple predicates, implicitly joined by "or". Here is my converter:

``` proc fol2clauses sentences {
set res {}
foreach sentence [split [string trim \$sentences] \n] {
regsub {;#.+} \$sentence "" sentence
set c [fol2clause \$sentence]
foreach {pred p q} \$c break
switch -- \$pred {
and {eval lappend res [fol2clauses \$p] [fol2clauses \$q]}
or  {lappend res [flattenOr \$c]}
default {lappend res \$c}
}
}
set res2 {}; set n 0
foreach clause \$res {
incr n
set theta {}
foreach var [variables \$clause] {
lappend theta \$var \$var\$n
}
lappend res2 [subs \$theta \$clause]
}
set res2
}
proc flattenOr {c} {
#-- turn (or (or P Q) s), (or P (or Q S)).. to P Q S
foreach {pred p q} \$c break
if {\$pred=="or"} {
concat [flattenOr \$p] [flattenOr \$q]
} else {
list \$c
}
}
proc variables clause {
set res {}
foreach word [string map {\{ "" \} ""} \$clause] {
if {[isVar \$word] && [lsearch \$res \$word]<0} {
lappend res \$word
}
}
set res
}
proc isVar x {regexp {^[a-z][0-9]*\$} \$x}
proc fol2clause sentence {
foreach {pred p q} \$sentence break
if {![info exist pred]} return
set p1 [fol2clause \$p]
if [info exist q] {set q1 [fol2clause \$q]}
switch -- \$pred {
all  {set q1 ;# eliminate universal quantifier}
equ  {and [or [not \$p1] \$q1] [or [not \$q1] \$p1]}
impl {or [fol2clause [not \$p1]]  \$q1}
not  {
foreach {pred2 p2 q2} \$p break
set p3 [fol2clause \$p2]
set q3 [fol2clause \$q2]
switch -- \$pred2 {
and     {or  [not \$p3] [not \$q3]}
or      {and [not \$p3] [not \$q3]}
default {not [fol2clause \$p]}
}
}
or  {
if {[lindex \$p1 0]=="and"} {
foreach {- p4 q4} \$p1 break
and [fol2clause [or \$p4 \$q1]] [fol2clause [or \$q4 \$q1]]
} elseif {[lindex \$q1 0]=="and"} {
foreach {- p4 q4} \$q1 break
and [or \$p1 \$p4] [or \$p1 \$q4]
} else {set sentence}
}
default {set sentence}
}
}
#---------- these "connectives" only build up lists
proc and {p q} {list and \$p \$q}
proc or  {p q} {list or  \$p \$q}
proc not p {
if {[lindex \$p 0] == "not"} {
lindex \$p 1
} else {
list not \$p
}
}
proc test {name cases} {
puts "testing \$name..."
foreach {test expected} \$cases {
puts \$test:
set res [eval \$test]
if {\$res!=\$expected} {
puts "***** [join \$res ,\n]/\$expected"
} else {puts OK:\$res}
}
}
proc testFOL2Clauses {} {
set ::fol {
all x {impl {cat x} {likes x Fish}}
all x {all y {impl {and {cat x} {likes x y}} {eats x y}}}
cat Felix
}
test FOL2clauses {{fol2clauses \$::fol} ?}
}```

An important part of proving is unification, finding a set of substitutions ("most general unifier") so that two clauses which partially contain variables can be matched:

``` proc unify {p q {theta {}}} {
foreach {r s} [disagree \$p \$q] break
if {![info exists r]} {return \$theta}
if [isVar \$r] {
lappend theta \$r \$s
} elseif [isVar \$s] {
lappend theta \$s \$r
} else {return false}
unify [subs \$theta \$p] [subs \$theta \$q] \$theta
}
proc disagree {p q} {
# find the first position where p and q are not equal
regsub -all "not " \$p "" p
regsub -all "not " \$q "" q
foreach i \$p j \$q {
if {\$i != \$j} {
if {[llength \$i]>1 && [llength \$j]>1} {
return [disagree \$i \$j]
} else {
return [list \$i \$j]
}
}
}
}
proc subs {theta p} {
# replace "from" with "to" in p, where theta is a {from to..} list
set res {}
foreach word \$p {
if {[llength \$word]>1} {
set word [subs \$theta \$word]
} else {
foreach {from to} \$theta {
if {\$word==\$from} {set word \$to; break}
}
}
lappend res \$word
}
set res
}
proc testUnify {} {
test Unify {
{unify {parents x {father x} {mother Bill}} \
{parents Bill {father Bill} y}}
{x Bill y {mother Bill}}
{unify {parents x {father x} {mother Bill}} \
{parents Bill {father y} z}}
{x Bill y Bill z {mother Bill}}
{unify {parents x {father x} {mother Jane}} \
{parents Bill {father y} {mother y}}}
false
}
}```

Now the core of proving, the resolution rule where two rules from KB make a new one, which is shorter than just concatenating the two, because a pair of contradicting terms is cancelled out:

``` proc resolution-rule {p q {theta {}}} {
set p1 [subs \$theta \$p]
set q1 [subs \$theta \$q]
set canceled {} ;# find only one pair for canceling
foreach i \$p1 {
foreach j \$q1 {
if {[not \$i]== \$j} {
set canceled [list \$i \$j]; break
}
}
if [llength \$canceled] break
}
set res {}
foreach i [concat \$p1  \$q1] {
if {[lsearch \$canceled \$i]<0 && [lsearch \$res \$i]<0} {
lappend res \$i
}
}
if {[llength \$res]==2} {
foreach {r s} \$res break
if {[not \$r] == \$s} {set res true}
}
set res
}
proc testResolution {} {
test resolution {
{resolution-rule P {{not P} Q} ;# Modus ponens} Q
{resolution-rule {{not P} Q} {{not Q} R}} {{not P} R}
{resolution-rule P {{not P}}} {}
{resolution-rule {P Q} {{not P} {not Q}}} true
}
}```

Now that we got all the needed parts together, let's go prove! Strictly following Dyer's lecture notes, I use "resolution by refutation", i.e. I add the negated goal to the knowledge base, and if that raises a contradiction, the goal is proven to be consistent:

``` proc prove {kb goal} {
set kb [fol2clauses \$kb]
set goal [fol2clauses [not \$goal]]
while 1 {
set found 0
foreach clause \$kb {
foreach atom \$clause {
set theta [unify \$atom \$goal]
if {\$theta != "false" || [not \$atom] == \$goal} {
set resolvent [resolution-rule \$clause \$goal \$theta]
if {\$resolvent == \$clause} break
if {\$resolvent == ""} {return true}
if {\$resolvent == \$goal} {return true}
puts resolvent:\$resolvent,theta:\$theta
lappend kb \$goal
incr found
set goal \$resolvent
break ;# start another provin' round...
}
}
}
if !\$found {return false}
}
}
proc testProve {} {
test Prove {{prove \$::fol {eats Felix Fish}} true}
} ;# this still fails... ;-(

{prove {
impl Tails YouLose
equ  IWin  YouLose
} IWin} true}
}
#------------------------------------- self-test
if {[file tail [info script]]==[file tail \$argv0]} {
testFOL2Clauses
testUnify
testResolution
##testProve