LK-GL rules |
The rules used by the prover are the rules of the Gentzen sequent calculus LK completed by the following rule, which is named necR (necessary right) in the prover
[]Γ, Γ,[]A |-- A ------------------(necR) []Γ |-- []A |
[]Γ, Γ,[]A |-- A -------------------- where A is member of list Δ Λ, []Γ |-- Π, []Δ |
Γ |-- A, Δ B, Γ |-- Δ ---------------------------(implyL) A => B, Γ |-- Δ |
A, Γ |-- B, Δ ----------------- (implyR) Γ |-- A => B, Δ |
A, Γ |-- Δ B, Γ |-- Δ -------------------------(orL) A+B, Γ |-- Δ |
Γ |-- A, B, Δ --------------(orR) Γ |-- A+B, Δ |
examples | rules | syntax | info | home | download | Last Modified : 17-Dec-2021 |