# Sequent

Model was written in NetLogo 5.1.0
•
Viewed 140 times
•
Downloaded 9 times
•
Run 0 times

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 about 5 years ago by Anthony Dekker.

## Attached files

File | Type | Description | Last updated | |
---|---|---|---|---|

Sequent.png | preview | Preview for 'Sequent' | about 5 years ago, by Anthony Dekker | Download |

This model does not have any ancestors.

This model does not have any descendants.