;;; Logic problem inference system
;;; Meta-inference rule version

;; Establish categories

to category :category.name :members
print (list "category :category.name :members)
if not namep "categories [make "categories []]
make "categories lput :category.name :categories
make :category.name :members
foreach :members [pprop ? "category :category.name]
end

;; Verify and falsify matches

to verify :a :b
settruth :a :b "true
end

to falsify :a :b
settruth :a :b "false
end

to settruth :a :b :truth.value
if equalp (gprop :a "category) (gprop :b "category) [stop]
localmake "oldvalue get :a :b
if equalp :oldvalue :truth.value [stop]
if equalp :oldvalue (not :truth.value) ~
   [(throw "error (sentence [inconsistency in settruth]
                            :a :b :truth.value))]
print (list :a :b "-> :truth.value)
store :a :b :truth.value
settruth1 :a :b :truth.value
settruth1 :b :a :truth.value
if not emptyp :oldvalue ~
   [foreach (filter [equalp first ? :truth.value] :oldvalue)
            [apply "settruth butfirst ?]]
end

to settruth1 :a :b :truth.value
apply (word "find not :truth.value) (list :a :b)
foreach (gprop :a "true) [settruth ? :b :truth.value]
if :truth.value [foreach (gprop :a "false) [falsify ? :b]
                 pprop :a (gprop :b "category) :b]
pprop :a :truth.value (fput :b gprop :a :truth.value)
end

to findfalse :a :b
foreach (filter [not equalp get ? :b "true] peers :a) ~
        [falsify ? :b]
end

to findtrue :a :b
if equalp (count peers :a) (1+falses :a :b) ~
   [verify (find [not equalp get ? :b "false] peers :a)
           :b]
end

to falses :a :b
output count filter [equalp "false get ? :b] peers :a
end

to peers :a
output thing gprop :a "category
end

;; Common types of clues

to differ :list
print (list "differ :list)
foreach :list [differ1 ? ?rest]
end

to differ1 :a :them
foreach :them [falsify :a ?]
end

to neighbor :this :that :lineup
falsify :this :that
implies :this first :lineup "true :that first bf :lineup "true
implies :that first :lineup "true :this first bf :lineup "true
implies :this last :lineup "true :that last bl :lineup "true
implies :that last :lineup "true :this last bl :lineup "true
neighbor1 :lineup count :lineup
end

to neighbor1 :lineup :count
if :count=0 [stop]
foreach (bf bf bf :lineup) [
  implies :this first bf :lineup "true :that ? "false
  implies :that first bf :lineup "true :this ? "false
]
neighbor1 (lput first :lineup bf :lineup) :count-1
end

to justbefore :this :that :lineup
falsify :this :that
falsify :this last :lineup
falsify :that first :lineup
justbefore1 :this :that :lineup
end

to justbefore1 :this :that :slotlist
if emptyp butfirst :slotlist [stop]
equiv :this (first :slotlist) :that (first butfirst :slotlist)
justbefore1 :this :that (butfirst :slotlist)
end

;; Remember conditional linkages

to implies :who1 :what1 :truth1 :who2 :what2 :truth2
if equalp (gprop :who1 "category) (gprop :what1 "category) [stop]
if equalp (gprop :who2 "category) (gprop :what2 "category) [stop]
implies1 :who1 :what1 :truth1 :who2 :what2 :truth2
implies1 :who2 :what2 (not :truth2) :who1 :what1 (not :truth1)
end

to implies1 :who1 :what1 :truth1 :who2 :what2 :truth2
localmake "old1 get :who1 :what1
if equalp :old1 :truth1 [settruth :who2 :what2 :truth2  stop]
if equalp :old1 (not :truth1) [stop]
if memberp (list :truth1 :who2 :what2 :truth2) :old1 [stop]
if memberp (list :truth1 :what2 :who2 :truth2) :old1 [stop]
if memberp (list :truth1 :who2 :what2 (not :truth2)) :old1 ~
   [settruth :who1 :what1 (not :truth1)  stop]
if memberp (list :truth1 :what2 :who2 (not :truth2)) :old1 ~
   [settruth :who1 :what1 (not :truth1)  stop]
store :who1 :what1 ~
      fput (list :truth1 :who2 :what2 :truth2) :old1
if :truth2 [foreach (remove :who2 peers :who2)
                    [implies :who1 :what1 :truth1 ? :what2 "false]
            foreach (remove :what2 peers :what2)
                    [implies :who1 :what1 :truth1 :who2 ? "false]]
if not :truth2 [implies2 :what2 (remove :who2 peers :who2)
                implies2 :who2 (remove :what2 peers :what2)]
foreach (gprop :who2 "true) ~
        [implies :who1 :what1 :truth1 ? :what2 :truth2]
foreach (gprop :what2 "true) ~
        [implies :who1 :what1 :truth1 :who2 ? :truth2]
if :truth2 ~
   [foreach (gprop :who2 "false)
            [implies :who1 :what1 :truth1 ? :what2 "false]
    foreach (gprop :what2 "false)
            [implies :who1 :what1 :truth1 :who2 ? "false]]
end

to implies2 :one :others
localmake "left filter [not (or memberp (list :truth1 :one ? "false) :old1
                                memberp (list :truth1 ? :one "false) :old1
                                (and :truth1
                                     (or (and equalp ? :who1
                                              equalp gprop :what1 "category
                                                     gprop :one "category)
                                         (and equalp ? :what1
                                              equalp gprop :who1 "category
                                                     gprop :one "category))
                                     (not or equalp :one :who1 
                                             equalp :one :what1))
                                equalp get :one ? "false)] ~
                       :others
if emptyp :left [settruth :who1 :what1 (not :truth1) stop]
if emptyp butfirst :left ~
   [implies :who1 :what1 :truth1 :one first :left "true]
end

to equiv :who1 :what1 :who2 :what2
implies :who1 :what1 "true :who2 :what2 "true
implies :who2 :what2 "true :who1 :what1 "true
end

to xor :who1 :what1 :who2 :what2
implies :who1 :what1 "true :who2 :what2 "false
implies :who1 :what1 "false :who2 :what2 "true
end

;; Interface to property list mechanism

to get :a :b
output gprop :a :b
end

to store :a :b :val
pprop :a :b :val
pprop :b :a :val
end

;; Print the solution

to solution
foreach thing first :categories [solve1 ? butfirst :categories]
end

to solve1 :who :order
type :who
foreach :order [type "| |   type gprop :who ?]
print []
end

;; Get rid of old problem data

to cleanup
if not namep "categories [stop]
ern :categories
ern "categories
erpls
end