Sequent

; © Anthony Dekker, written for a tutorial at scientificgems.wordpress.com

globals [
  computed-facts
  result?
]

to go
  if (verbose?) [ print "------------------------------------------------------------------------" ]
  clear-all
  ask patches [ set pcolor white ]
  create-turtles 1 [ set color blue set size 3 set shape "person" setxy random-xcor random-ycor ]
  create-turtles 1 [ set color red set size 2 set shape "person" setxy random-xcor random-ycor ]

  set result? "?"
  ask (turtle 0) [ compute-basic-facts ]

  let hypotheses (sentence computed-facts (read-from-string other-hypotheses))
  set result? sequent-prove-a [] hypotheses [] (list (read-from-string conclusion))
end 

to compute-basic-facts  ; calculated by a specific turtle
  let fact1 (ifelse-value (xcor < 0) [ "Left" ] [ "Right" ])
  let d (distance (turtle 1))
  let fact2 (ifelse-value (d < 4) [ "Near" ] [ "Far" ])
  set computed-facts (list fact1 fact2)
end 

to-report sequent-prove-a [ atomic-hyp non-at-hyp atomic-conc non-at-conc ]  ; split hypotheses
  nice-print "a" atomic-hyp non-at-hyp atomic-conc non-at-conc ""
  ifelse (non-at-hyp = [])
    [ report sequent-prove-b atomic-hyp atomic-conc non-at-conc ]
    [ let p (first non-at-hyp)
      set non-at-hyp (but-first non-at-hyp)
      ifelse (is-string? p)  ; atomic
        [ report sequent-prove-a (fput p atomic-hyp) non-at-hyp atomic-conc non-at-conc ]
        [ ifelse (first p = "not")  ; not q
            [ let q (item 1 p)
              report sequent-prove-a atomic-hyp non-at-hyp atomic-conc (fput q non-at-conc) ]
            [ ifelse (first p = "and")  ; q /\ r
                [ let q (item 1 p)
                  let r (item 2 p)
                  report sequent-prove-a atomic-hyp (fput q (fput r non-at-hyp)) atomic-conc non-at-conc ]
                [ ifelse (first p = "or")  ; q \/ r
                    [ let q (item 1 p)
                      let r (item 2 p)
                      ;print "fork on hypothesis v"
                      report (sequent-prove-a atomic-hyp (fput q non-at-hyp) atomic-conc non-at-conc)
                         and (sequent-prove-a atomic-hyp (fput r non-at-hyp) atomic-conc non-at-conc) ]
                    [ ifelse (first p = "implies")  ; same as (not q) \/ r
                        [ let q (item 1 p)
                          let r (item 2 p)
                          ;print "fork on hypothesis ->"
                          report (sequent-prove-a atomic-hyp (fput r non-at-hyp) atomic-conc non-at-conc)
                             and (sequent-prove-a atomic-hyp non-at-hyp atomic-conc (fput q non-at-conc)) ]
                        [ error "Unexpected logical" ]
                    ]
                ]
            ]
        ]
    ]
end 

to-report sequent-prove-b [ atomic-hyp atomic-conc non-at-conc ]  ; split conclusions
  nice-print "b" atomic-hyp [] atomic-conc non-at-conc ""
  ifelse (non-at-conc = [])
    [ report sequent-prove-c atomic-hyp atomic-conc ]
    [ let p (first non-at-conc)
      set non-at-conc (but-first non-at-conc)
      ifelse (is-string? p)  ; atomic
        [ report sequent-prove-b atomic-hyp (fput p atomic-conc) non-at-conc ]
        [ ifelse (first p = "not")  ; not q
            [ let q (item 1 p)
              report sequent-prove-a atomic-hyp (list q) atomic-conc non-at-conc ]
            [ ifelse (first p = "and")  ; q /\ r
                [ let q (item 1 p)
                  let r (item 2 p)
                  ;print "fork on conclusion ^"
                  report (sequent-prove-b atomic-hyp atomic-conc (fput q non-at-conc))
                     and (sequent-prove-b atomic-hyp atomic-conc (fput r non-at-conc)) ]
                [ ifelse (first p = "or")  ; q \/ r
                    [ let q (item 1 p)
                      let r (item 2 p)
                      report sequent-prove-b atomic-hyp atomic-conc (fput q (fput r non-at-conc)) ]
                    [ ifelse (first p = "implies")  ; same as (not q) \/ r
                        [ let q (item 1 p)
                          let r (item 2 p)
                          report sequent-prove-a atomic-hyp (list q) atomic-conc (fput r non-at-conc) ]
                        [ error "Unexpected logical" ]
                    ]
                ]
            ]
        ]
    ]
end 

to-report sequent-prove-c [ atomic-hyp atomic-conc ]
  let proved? false
  foreach atomic-conc [
    if ((not proved?) and member? ? atomic-hyp) [ set proved? true ]
  ]
  ifelse (proved?)
    [ nice-print "  c" atomic-hyp [] atomic-conc [] "   ** proved **" ]
    [ nice-print "  c" atomic-hyp [] atomic-conc [] "   failed!" ]
  report proved?
end 

to-report nice-item [ p ]
  ifelse (is-string? p)
    [ report p ]
    [ ifelse (first p = "not")
        [ let q (item 1 p)
          report (word "~ " (nice-item q)) ]
        [ ifelse (first p = "and")
            [ let q (item 1 p)
              let r (item 2 p)
              report (word "(" (nice-item q) " ^ " (nice-item r) ")") ]
            [ ifelse (first p = "or")
                [ let q (item 1 p)
                  let r (item 2 p)
                  report (word "(" (nice-item q) " v " (nice-item r) ")") ]
                [ ifelse (first p = "implies")
                    [ let q (item 1 p)
                      let r (item 2 p)
                      report (word "(" (nice-item q) " -> " (nice-item r) ")") ]
                    [ error "Unexpected logical" ]
                ]
            ]
        ]
    ]
end 

to-report nice-list [ p ]
  ifelse (p = [])
    [ report "" ]
    [ report (reduce [ (word ?1 ", " ?2) ] (map nice-item p)) ]
end 

to nice-print [ lab x y z w t]
  if (verbose?) [
    print (word lab ": " (nice-list (sentence x y)) " |- " (nice-list (sentence z w)) t)
  ]
end