Sequent Calculus in NetLogo

NetLogo programs sometimes require agents to reason, and one of the simplest forms of reasoning is the sequent calculus. This uses expressions of the form α, β, γ, δ ⊢ ε, ζ, η which are interpreted as α ˄ β ˄ γ ˄ δ ⇒ ε ˅ ζ ˅ η. That is, all the hypotheses α, β, γ, δ are assumed to be true, and from that it should follow that at least one of the conclusions ε, ζ, η is true.

We can resolve the truth of sequents like α, β, γ, δ ⊢ ε, ζ, η using rules which simplify occurrences of ¬ φ (not φ), φ ˄ ψ (φ and ψ), φ ˅ ψ (φ or ψ), and φ ⇒ ψ (φ implies ψ) occurring in the hypotheses and/or conclusions, until we are left with a number of sequents like α, β, γ, δ ⊢ ε, ζ, η containing only atomic formulae. Such an expression is true if one of the atomic formulae on the left also occurs on the right (or, in more advanced versions of the logic, if the atomic formulae on the left somehow imply one of the atomic formulae on the right, in the way that x = y and y = z imply x = z).

The simplification rules are as follows. Note that some rules generate two new sequents, and that the rule for not flips things from the hypotheses to the conclusions or vice versa:

We can code these up easily in NetLogo, using the list [ "and" φ ψ ] to represent φ ˄ ψ, and so forth. The following function takes 4 lists (atomic and non-atomic hypotheses; atomic and non-atomic conclusions) and applies the simplification rules to the hypotheses (with some printing for debugging):

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)
                      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)
                           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

Once all hypotheses are atomic, the following function applies the simplification rules to the conclusions (for some cases it must call sequent-prove-a again):

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)
                  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

Once both hypotheses and conclusions are atomic, checking truth just needs a simple intersection test:

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

Printing requires some code to make sequents look nice:

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

For demonstration purposes, the go button computes some basic facts about two turtles, combining this with a user-supplied list of hypotheses, and tries to prove a user-supplied conclusion (in this case [ "and" [ "implies" "C" "F" ] [ "not" [ "not" "Far" ] ] ], representing (C ⇒ F) ˄ ¬ ¬ Far.

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

The NetLogo interface is shown at the top of this page, and the code is at Modelling Commons. The simple sequent calculus reasoner presented here can be fairly easily extended with quantifiers and other features that might be necessary.

See also my other NetLogo tutorials.

Advertisement