sessions.yaml

- name: Session 1
  logic: predicate
  visible-rules:
    - conjI
    - conjE
  tasks:
  - assumptions: ["A"]
    conclusions: ["A"]
    min-blocks: 2
  - assumptions: ["A", "B"]
    conclusions: ["A"]
    min-blocks: 3
  - assumptions: ["A", "B"]
    conclusions: ["B", "A"]
    min-blocks: 4
  - assumptions: ["A", "B"]
    conclusions: ["A∧B"]
    min-blocks: 4
  - assumptions: ["A"]
    conclusions: ["A∧A"]
    min-blocks: 3
  - assumptions: ["A∧B"]
    conclusions: ["A"]
    min-blocks: 3
  - assumptions: ["A∧B"]
    conclusions: ["A", "B"]
    min-blocks: 4
  - assumptions: ["A∧B"]
    conclusions: ["A∧B"]
    min-blocks: 2
  - assumptions: ["A∧B"]
    conclusions: ["B∧A"]
    min-blocks: 4
  - assumptions: ["A∧B∧C"]
    conclusions: ["A","B","C"]
    min-blocks: 6
  - assumptions: ["A∧B∧C"]
    conclusions: ["A∧C"]
    min-blocks: 5
  - assumptions: ["A∧B∧C"]
    conclusions: ["A∧(B∧C)"]
    min-blocks: 6
- name: Session 2
  logic: predicate
  visible-rules:
    - conjI
    - conjE
    - impI
    - impE
  tasks:
  - assumptions: ["A","A→B"]
    conclusions: ["B"]
    min-blocks: 4
  - assumptions: ["A","A→B","B→C"]
    conclusions: ["C"]
    min-blocks: 6
  - assumptions: ["A","A→B","A→C","B→D", "C→D"]
    conclusions: ["D"]
    min-blocks: 8
  - assumptions: ["A","A→A"]
    conclusions: ["A"]
    min-blocks: 3
  - assumptions: ["A→B","B→C"]
    conclusions: ["A→C"]
    min-blocks: 6
  - assumptions: ["A→B","A→B→C"]
    conclusions: ["A→C"]
    min-blocks: 7
  - assumptions: []
    conclusions: ["A→A"]
    min-blocks: 2
  - assumptions: ["A→C","B→C","A∧B"]
    conclusions: ["C"]
    min-blocks: 6
  - assumptions: ["A→C","B→C"]
    conclusions: ["(A∧B)→C"]
    min-blocks: 6
  - assumptions: ["B"]
    conclusions: ["A→B"]
    min-blocks: 3
  - assumptions: ["(A∧B)→C"]
    conclusions: ["A→B→C"]
    min-blocks: 6
  - assumptions: ["A→B→C"]
    conclusions: ["(A∧B)→C"]
    min-blocks: 6
  - assumptions: ["(A→B)∧(A→C)"]
    conclusions: ["A→(B∧C)"]
    min-blocks: 7
  - assumptions: ["A→(A→B)", "(A→B)→A"]
    conclusions: ["B"]
    min-blocks: 8
- name: Session 3
  logic: predicate
  visible-rules:
    - conjI
    - conjE
    - impI
    - impE
    - disjI1
    - disjI2
    - disjE
  tasks:
  - assumptions: ["A", "B"]
    conclusions: ["A∨B"]
    min-blocks: 4
  - assumptions: ["A"]
    conclusions: ["A∨B"]
    min-blocks: 3
  - assumptions: ["B"]
    conclusions: ["A∨B"]
    min-blocks: 3
  - assumptions: ["A"]
    conclusions: ["A∨A"]
    min-blocks: 3
  - assumptions: ["A∨B"]
    conclusions: ["B∨A"]
    min-blocks: 5
  - assumptions: ["A∨(B∨C)"]
    conclusions: ["(A∨B)∨C"]
    min-blocks: 9
  - assumptions: ["A∧B"]
    conclusions: ["A∨B"]
    min-blocks: 4
  - assumptions: ["(A∧B)∨C"]
    conclusions: ["(A∨C)∧(B∨C)"]
    min-blocks: 10
  - assumptions: ["(A∨B)∧C"]
    conclusions: ["(A∧C)∨(B∧C)"]
    min-blocks: 8
  - assumptions: ["(A→C)∧(B→C)"]
    conclusions: ["(A∨B)→C"]
    min-blocks: 7
  - assumptions: ["(A∨B)→C"]
    conclusions: ["(A→C)∧(B→C)"]
    min-blocks: 9
  - assumptions: ["(A→B)∨(A→C)"]
    conclusions: ["A→(B∨C)"]
    min-blocks: 8
- name: Session 4
  logic: predicate
  visible-rules:
    - conjI
    - conjE
    - impI
    - impE
    - disjI1
    - disjI2
    - disjE
    - falseE
  tasks:
  - assumptions: ["⊥"]
    conclusions: ["A"]
    min-blocks: 3
  - assumptions: ["⊥"]
    conclusions: ["A","B"]
    min-blocks: 5
  - assumptions: ["A"]
    conclusions: ["⊥∨A"]
    min-blocks: 3
  - assumptions: ["⊥∨A"]
    conclusions: ["A"]
    min-blocks: 4
  - assumptions: ["⊥∧A"]
    conclusions: ["⊥"]
    min-blocks: 3
  - conclusions: ["⊥→A"]
    min-blocks: 3
  - assumptions: ["A→B"]
    conclusions: ["(B→⊥)→(A→⊥)"]
    min-blocks: 6
  - assumptions: ["(A∨B)→⊥"]
    conclusions: ["(A→⊥)∧(B→⊥)"]
    min-blocks: 9
  - assumptions: ["(A→⊥)∧(B→⊥)"]
    conclusions: ["(A∨B)→⊥"]
    min-blocks: 7
  - assumptions: ["(A→⊥)∨(B→⊥)"]
    conclusions: ["(A∧B)→⊥"]
    min-blocks: 7
  - assumptions: ["(((A→⊥)→⊥)→⊥)"]
    conclusions: ["A→⊥"]
    min-blocks: 6
  - assumptions: ["(A→⊥)∨B"]
    conclusions: ["A→B"]
    min-blocks: 6
  - assumptions: ["A→⊥", "B→A"]
    conclusions: ["B→⊥"]
    min-blocks: 6
  - assumptions: ["(A→⊥)∨(B→⊥)∨(C→⊥)"]
    conclusions: ["(A∧B∧C)→⊥"]
    min-blocks: 10
  - assumptions: []
    conclusions: ["((A∨(A→⊥))→⊥)→⊥"]
    min-blocks: 7
- name: Session 5
  logic: predicate
  visible-rules:
    - conjI
    - conjE
    - impI
    - impE
    - disjI1
    - disjI2
    - disjE
    - falseE
    - TND
  tasks:
  - conclusions: ["A∨(A→⊥)"]
    min-blocks: 2
  - assumptions: ["(B→⊥)→(A→⊥)"]
    conclusions: ["A→B"]
    min-blocks: 8
  - assumptions: ["(A∧B)→⊥"]
    conclusions: ["(A→⊥)∨(B→⊥)"]
    min-blocks: 9
  - assumptions: ["((A→⊥)→⊥)"]
    conclusions: ["A"]
    min-blocks: 6
  - assumptions: ["A→B"]
    conclusions: ["(A→⊥)∨B"]
    min-blocks: 7
  - assumptions: ["A→B", "B→C"]
    conclusions: ["(A→⊥)∨C"]
    min-blocks: 9
  - conclusions: ["((A→B)→A)→A"]
    min-blocks: 8
  - assumptions: ["(A∧B∧C)→⊥"]
    conclusions: ["(A→⊥)∨(B→⊥)∨(C→⊥)"]
    min-blocks: 14
  - assumptions: ["(A→B)→⊥"]
    conclusions: ["A∧(B→⊥)"]
    min-blocks: 12
- name: Session 6
  logic: predicate
  tasks:
  - assumptions: ["∀x.P(x)"]
    conclusions: ["P(a)"]
    min-blocks: 3
  - assumptions: ["∀x.P(x)"]
    conclusions: ["P(a) ∧  P(b)"]
    min-blocks: 5
  - assumptions: ["P(a)"]
    conclusions: ["∃x.P(x)"]
    min-blocks: 3
  - assumptions: ["∀x.P(x)"]
    conclusions: ["∃x.P(x)"]
    min-blocks: 4
  - assumptions: ["∀x.A"]
    conclusions: ["A"]
    min-blocks: 3
  - assumptions: ["∃x.A"]
    conclusions: ["A"]
    min-blocks: 3
  - assumptions: ["A∧(∀x.P(x))"]
    conclusions: ["∀x.A∧P(x)"]
    min-blocks: 6
  - assumptions: ["(∀x.P(x)) ∧ (∀x.Q(x))"]
    conclusions: ["∀x.P(x)∧Q(x)"]
    min-blocks: 7
  - assumptions: ["(∃x.P(x)) ∨ (∃x.Q(x))"]
    conclusions: ["∃x.P(x)∨Q(x)"]
    min-blocks: 9
  - assumptions: ["(∃x.P(x))→A"]
    conclusions: ["∀x.P(x)→A"]
    min-blocks: 6
  - assumptions: ["∀x.(P(x)→Q(x))", "P(a)"]
    conclusions: ["Q(a)"]
    min-blocks: 5
# Das tut noch nicht. Bug?
#  - assumptions: ["∀x.∃y.P(x,y)"]
#    conclusions: ["∃f.∀x.P(x,f(x))"]
  - assumptions: ["∀x.∀y.P(x,y)"]
    conclusions: ["∀y.∀x.P(x,y)"]
    min-blocks: 6
  - assumptions: ["∃x.∃y.P(x,y)"]
    conclusions: ["∃y.∃x.P(x,y)"]
    min-blocks: 6
  - assumptions: ["∃x.∀y.P(x,y)"]
    conclusions: ["∀y.∃x.P(x,y)"]
    min-blocks: 6
  - assumptions: ["∀x.P(x)"]
    conclusions: ["(∃x.P(x)→⊥)→⊥"]
    min-blocks: 6
  - assumptions: ["(∀x.P(x))→⊥"]
    conclusions: ["∃x.P(x)→⊥"]
    min-blocks: 12
  - assumptions: ["(∀x.P(x))→A"]
    conclusions: ["∃x.P(x)→A"]
    min-blocks: 16
- name: Session 7
  logic: predicate
  tasks:
  - conclusions: ["∃x.t(x)→(∀x.t(x))"]
    min-blocks: 14
  - assumptions: ["∀x.(r(x)→⊥)→r(f(x))"]
    conclusions: ["∃x.r(x)∧r(f(f(x)))"]
    min-blocks: 22
- name: Hilbert system
  logic: hilbert
  tasks:
  - conclusions: ["A→A"]
    min-blocks: 6
  - conclusions: ["(B→C)→(A→B)→A→C"]
    min-blocks: 8
  - conclusions: ["(A→B→C)→B→A→C"]
    min-blocks: 20
  - conclusions: ["~A→A→B"]
    min-blocks: 8
  - conclusions: ["(~A→A)→A"]
    min-blocks: 20
  - conclusions: ["~~A→A"]
    min-blocks: 18
  - conclusions: ["A→~~A"]
    min-blocks: 20
  - conclusions: ["(B→A)→~A→~B"]
    min-blocks: 60
  - conclusions: ["(A→B)→(~A→B)→B"]
    min-blocks: 82
- name: NAND calculus
  logic: nand
  tasks:
  - assumptions: ["A↑B"]
    conclusions: ["B↑A"]
    min-blocks: 4
  - assumptions: ["A"]
    conclusions: ["(A↑A)↑(A↑A)"]
    min-blocks: 4
  - conclusions: ["A↑A↑A"]
    min-blocks: 2
  - assumptions: ["(A↑A)↑(A↑A)"]
    conclusions: ["A"]
    min-blocks: 6
  - assumptions: ["A","B"]
    conclusions: ["A↑B↑(A↑B)"]
    min-blocks: 6
  - assumptions: ["A↑B↑(A↑B)"]
    conclusions: ["A","B"]
    min-blocks: 14
- name: Simply typed lambda calculus
  logic: STLC
  tasks:
  - conclusions: ["(λx.x):a→a"]
  - conclusions: ["(λx.(λy.x)):a→b→a"]
  - conclusions: ["(λx.(λy.(λz.(x⋅z)⋅(y⋅z)))):(a→b→c)→(a→b)→a→c"]
# - name: Classical logic
#   logic: classical
#   tasks:
#   - conclusions: ["p(¬(⊥ ∧ ⊥))"]
#   - conclusions: ["p((A∧B∧C) → (A∧C))"]