Sequent

Sequent preview image

1 collaborator

Ahdekker Anthony Dekker (Author)

Tags

(This model has yet to be categorized with any tags)
Visible to everyone | Changeable by the author
Model was written in NetLogo 5.1.0 • Viewed 132 times • Downloaded 7 times • Run 0 times
Download the 'Sequent' modelDownload this modelEmbed this model

Do you have questions or comments about this model? Ask them here! (You'll first need to log in.)


WHAT IS IT?

This program is an implementation of reasoning using the Sequent Calculus. It supplements an online tutorial at https://scientificgems.wordpress.com/2015/05/19/sequent-calculus-in-netlogo/

HOW TO USE IT

Edit other-hypotheses and conclusion, if desired, and click "go."

Comments and Questions

Please start the discussion about this model! (You'll first need to log in.)

Click to Run Model

; © 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 

There is only one version of this model, created over 4 years ago by Anthony Dekker.

Attached files

File Type Description Last updated
Sequent.png preview Preview for 'Sequent' over 4 years ago, by Anthony Dekker Download

This model does not have any ancestors.

This model does not have any descendants.