[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 [http://www.cs.wisc.edu/~dyer/cs540/notes/fopc.html] 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... ;-(
 
 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]]==[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?
<<categories>> Mathematics | Arts and crafts of Tcl-Tk programming