Click on each link:
- if you manage to finish the proof (green background), click on the
button to get an associated URL and send it by e-mail; - if the sequent is not provable, justify why it is not possible to build a proof.
- ⊢ A⊥ ⅋ A
- ⊢ A, B⊥ ⊗ A⊥, B
- A ⊗ B ⊢ B ⊗ A
- ⊢ A ⊗ A⊥, B, B⊥
- ⊢ (A ⊗ A) ⅋ (A⊥ ⅋ A⊥)
- ⊢ (A⊥ ⊗ A) ⅋ (A⊥ ⅋ A)
- A ⊢ A ⊗ A
- A ⊗ A ⊢ A
- (A ⅋ A⊥) ⊗ (A ⅋ A⊥) ⊢ A ⅋ A⊥
- ⊢ A⊥ ⅋ B, B⊥ ⊗ C, C⊥ ⊗ D, A ⊗ D⊥
- ⊢ 1, ⊥
- A ⊗ 1 ⊢ A
- A ⊢ ⊥ ⊗ A
- ⊢ 1, A⊥ ⊗ A
- ⊢ (1 ⅋ 1) ⊗ ⊥
- ⊢ A⊥ ⅋ B, B⊥ ⅋ A, ⊥ ⊗ ⊥
- ⊢ A ⊗ (B⊥ ⅋ C), (A⊥ ⅋ B) ⅋ (⊥ ⊗ C⊥)
- A ⊢ A & A
- A ⊢ A ⊕ A
- A ⊕ B ⊢ B ⊕ A
- ⊢ A⊥ ⊕ A
- A & B ⊢ A ⊗ B
- A & B, A & B ⊢ A ⊗ B
- (A ⊗ B) & (A ⊗ C) ⊢ A ⊗ (B & C)
- (A ⊗ B) ⊕ (A ⊗ C) ⊢ A ⊗ (B ⊕ C)
- ⊢ 1 ⊕ ⊤
- (A & 1) ⊗ (B & 1) ⊢ A & B
- ⊢ (A⊥ ⅋ B) ⊗ ⊤, A ⊗ ⊤
- ⊢ ((((⊤ ⅋ 1) ⊗ ⊥) ⅋ 0) ⊗ ⊤) ⅋ 1
- ⊢ (1 ⊕ A⊥) & (A⊥ ⅋ B), A ⊗ (B⊥ ⅋ (⊥ ⊕ B))