証明のストリング図

digraph {
 label="proof"
 subgraph cluster_not_a {
  label="not_a"
  h[shape=triangle]
  And_left
  h -> And_left[ label="￢A∧￢B"]
 }
 subgraph cluster_not_b {
  label="not_b"
  h1[shape=triangle, label="h"]
  And_right
  h1 -> And_right[ label="￢A∧￢B"]
  And_right[label="And_right"]
  
 }
 And_left -> Or_cotuple[label="￢A"]
 And_right -> Or_cotuple[label="￢B"]
 
 Or_cotuple
 
 Or_cotuple -> concl[label="￢(A∨B)"]
 concl[label="",shape=none]
}

digraph {
  label="proof"
  not_a [shape=triangle]
  not_b [shape=triangle]
  Or_cotuple
  not_a -> Or_cotuple[label="A⇒False"]
  not_b -> Or_cotuple[label="B⇒False"]
  concl[label="",shape=none]
  Or_cotuple -> concl[label="A∨B ⇒False"]
}