Seminario sulla logica BI.
Materiale introduttivo:
- The Logic of Bunched Implications, by Peter W. O'Hearn; David J.
Pym The Bulletin of Symbolic Logic 1999 Association for Symbolic Logic (PDF).
- David Pym, Peter O'Hearn, and Hongseok Yang. Possible Worlds
and Resources: The Semantics of BI. Theoretical Computer Science 315
(2004) 257-305. (PS)
Schedula:
Prossimi Argomenti:
- Labelled Tableaux:
D. Galmiche and al.
Semantic Labelled Tableaux for propositional BI (without bottom). (PS) Implementation: The BILL Theorem Prover
(Bunched Implication Logic with
Labels). Sarebbe utile del materiale su Labelled Deduction (link?).
Più in generale, Hybrid logics:
Areces, C. and ten Cate, B. Hybrid Logics. In Blackburn, P., Wolter,
F., and van Benthem, J., editors, Handbook of Modal Logics,
Elsevier, 2006. (PDF)
- Resource Tableaux:
Semantics of BI and
Resource Tableaux. D. Galmiche and D. Mery and D. Pym Mathematical
Structures in Computer Science, vol. 15, n. 6, pp 1033-1088, 2005. (PDF)
- Proof search on the sequent
calculus:
- Nozioni di base sul calcolo dei sequenti: note di Pfenning (PS),
capitolo 3
- Focusing;
capitolo 4 di Pfenning e più in dettaglio: Focusing
and Polarization in Linear, Intuitionistic, and Classical
Logic by Chuck
Liang and Dale Miller. 2007. (pdf)
- Inverse Method capitolo
5 di Pfenning e più in dettaglio: The Inverse Method (2001)
Anatoli Degtyarev, Andrei
Voronkov Handbook of Automated Reasoning, (link).
- Inverse e logica lineare: Kaustuv Chaudhuri and Frank
Pfenning: A Focusing Inverse Method
Theorem Prover for First-Order Linear Logic (PDF).
- Inverse e BI: Kevin
Donnelly at al "The Inverse Method for the Logic of Bunched Implications" (PDF).
Nota: manca la parte focusing.
- Applicazioni.
- Reti di Petri: Petri Net
Semantics of Bunched Implications Peter
O'Hearn And Hongseok Yang. (PDF)
- PCC: ILC: A Foundation for Automated Reasoning about Pointer
Programs. Limin Jia and
David Walker. (PS)
-