|
|
|
|
|
|
Help | Seminars List | Add Seminar | Edit Seminars | Tips for organisers | RSS | ics Calendar | Search | Send comments about this website to seminar-master@cecs.anu.edu.au
Contact: Michelle.Moravec@anu.edu.au CS PHD MONITORING
Deep Inference in Bi-intuitionistic LogicMs Linda Postniece (School of Computer Science, CECS)DATE: 2009-09-24 TIME: 14:00:00 - 14:30:00 LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU ABSTRACT: Bi-intuitionistic logic is the extension of intuitionistic logic with exclusion, a connective dual to implication. Cut-elimination in bi-intuitionistic logic is complicated due to the interaction between these two connectives, and various extended sequent calculi, including a display calculus, have been proposed to address this problem. In this talk, I will present a new extended sequent calculus DBiInt for bi-intuitionistic logic which uses nested sequents and “deep inference”, i.e., inference rules can be applied at any level in the nested sequent. I will show that DBiInt can simulate our previous “shallow” sequent calculus LBiInt. In particular, I show that deep inference can simulate the residuation rules in the display-like shallow calculus LBiInt. I also consider proof search and give a simple restriction of DBiInt which allows terminating proof search. Thus my work is another step towards addressing the broader problem of proof search in display logic.
|