A labelled sequent calculus for BBI : proof theory and proof search
We present a labelled sequent calculus for Boolean bunched implications (BBI), a classical variant of the logic of Bunched Implications (BI). The calculus is simple, sound, complete and enjoys cut-elimination. We show that all the structural rules in the calculus, i.e. those rules that manipulate la...
محفوظ في:
المؤلفون الرئيسيون: | Hóu, Zhé, Goré, Rajeev, Tiu, Alwen |
---|---|
مؤلفون آخرون: | School of Computer Science and Engineering |
التنسيق: | مقال |
اللغة: | English |
منشور في: |
2020
|
الموضوعات: | |
الوصول للمادة أونلاين: | https://hdl.handle.net/10356/142650 |
الوسوم: |
إضافة وسم
لا توجد وسوم, كن أول من يضع وسما على هذه التسجيلة!
|
مواد مشابهة
-
Extracting proofs from tabled proof search
بواسطة: Miller, Dale., وآخرون
منشور في: (2013) -
Truth in a Logic of Formal Inconsistency: How classical can it get?
بواسطة: LAVINIA MARIA PICOLLO
منشور في: (2021) -
Ophthalmic bottle labeling machine
بواسطة: Andaluz, Francis Gabriel, وآخرون
منشور في: (2009) -
Automated pressure-sensitive labeling machine
بواسطة: Carino, Faye Marie Goyena, وآخرون
منشور في: (2002) -
Computability via the lambda-calculus with patterns
بواسطة: Bodin Skulkiat
منشور في: (2012)