Proof

Enter a sequent to proof

Proof rule schemas

  • H, P ⊢ Phyp
  • H ⊢ Q
    H, P ⊢ Qmon
  • H ⊢ PH, P ⊢ Q
    H ⊢ Qcut
  • H, ⊥ ⊢ P⊥hyp
  • H, ¬P ⊢ ⊥
    H ⊢ Pcontr
  • H, P ⊢ ⊥
    H ⊢ ¬P¬goal
  • H ⊢ P
    H, ¬P ⊢ Q¬hyp
  • H ⊢ PH ⊢ Q
    H ⊢ P ∧ Q∧goal
  • H, P, Q ⊢ R
    H, P ∧ Q ⊢ R∧hyp

Instantiation

Please select a proof rule schema