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 [L1 ] 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]
lassign $c pred p q
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
lassign $c pred p q
if {$pred eq "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 {
lassign $sentence pred p q
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 {
lassign $p pred2 p2 q2
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] eq "and"} {
lassign $p1 - p4 q4
and [fol2clause [or $p4 $q1]] [fol2clause [or $q4 $q1]]
} elseif {[lindex $q1 0] eq "and"} {
lassign $q1 - p4 q4
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] eq "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 {}}} {
lassign [disagree $p $q] r s
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 eq $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] eq $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} {
lassign $res r s
if {[not $r] eq $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 ne "false" || [not $atom] eq $goal} {
set resolvent [resolution-rule $clause $goal $theta]
if {$resolvent eq $clause} break
if {$resolvent eq ""} {return true}
if {$resolvent eq $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... ;-(
proc testHeadsTails {} {
test HeadsTails {
{prove {
impl Heads IWin
impl Tails YouLose
or Heads Tails
equ IWin YouLose
} IWin} true}
}
#------------------------------------- self-test
if {[file tail [info script]] eq [file tail $argv0]} {
testFOL2Clauses
testUnify
testResolution
##testProve
testHeadsTails
}A meager result so far, considering how much code it is - but feel free to improve on it! Come time, I will have to add the "real" meat, Skolemized variables and functions, but first Felix must be proven to eat fish...
Finally, trying to think logically, what would "last-order logic" be? Maybe that what's being thought shortly before the pub closes?