logic: justification
system: tableau
name: Logic of proofs
description: |
    This is the system for LP described in my thesis.
rules:
    - name: "F→"
      consume: ["[F] A → B"]
      produce: 
          - ["[T] A", "[F] B"]
    - name: "F+"
      consume: ["[F] T+S:A"]
      produce: 
          - ["[F] T:A", "[F] S:A"]
    - name: "e"
      consume: ["[T] T:A"]
      produce:
          - ["[T] A"]
    - name: "!"
      consume: ["[F] !T:T:A"]
      produce:
          - ["[F] T:A"]
    - name: "T→"
      consume: ["[T] A -> B"]
      produce:
          - ["[F] A"]
          - ["[T] B"]
    - name: "F·"
      consume: ["[F] (S * T) : B"]
      produce:
          - ["[F] S:(A → B)"]
          - ["[F] T:A"]
      generate:
          match: "A → B"
          with: [subterms, formulas]
          in:
              union: [root, assumptions]
    - name: "CSr"
      consume: []
      produce:
          - ["[T] A"]
      generate:
          match: "A"
          with: all
          in: assumptions
assumptions: []