langston-barrrett.github.io
Bunched Logic
A logic that forms the foundation for separation logic.
Links
- The Wikipedia page on bunched logic is quite good.
- https://ncatlab.org/nlab/show/bunched+logic
Cards
Q. What are the two novel logical connectives in bunched logic?
A. ∗ and -∗
Q. In bunched logic, what are the two conjunction-like connectives?
A. ∧ and ∗
Q. In bunched logic, what are the two implication-like connectives?
A. → and -∗
Q. In bunched logic, which of the two conjunctions is called multiplicative, and which is called additive?
A. ∧ is additive and ∗ is multiplicative
Q. In bunched logic, which of the two implications is called multiplicative, and which is called additive?
A. → is additive and -∗ is multiplicative
Q. In bunched logic, how are the ∗ and -∗ connectives related?
A. By the deduction theorem: A ∗ B ⊢ C iff A ⊢ B -∗ C
Q. In bunched logic, what is the name of the "," operator on contexts?
A. Multiplicative composition
Q. In bunched logic, what is the name of the ";" operator on contexts?
A. Additive composition
Q. In bunched logic, what is the introduction rule for ∗?
A. Γ ⊢ A and Δ ⊢ B yield Γ, Δ ⊢ A ∗ B
Q. In bunched logic, what is the introduction rule for ∧?
A. Γ ⊢ A and Δ ⊢ B yield Γ; Δ ⊢ A ∧ B
Q. In bunched logic, which of the "," and ";" operators supports weakening and contraction?
A. ";"