Recent Drafts

    (currently none)

Journals

  1. Syntactic cut-elimination for a fragment of the modal mu-calculus
    with Thomas Studer

    December 2012

    Annals of Pure and Applied Logic
    BibTeX entry
    @article {bs12,
    	title = {Syntactic cut-elimination for a fragment of the modal mu-calculus},
    	journal = {Annals of Pure and Applied Logic},
    	volume = {163},
    	number = {12},
    	year = {2012},
    	pages = {1838-1853},
    	url = {http://www.iam.unibe.ch/ltgpub/2012/bs12.pdf},
    	author = {Kai Br{\"u}nnler and Thomas Studer}
    }
    
  2. Deep Sequent Systems for Modal Logic

    June 3, 2009

    Archive for Mathematical Logic
    BibTeX entry
    @article{Br09,
      title = "Deep Sequent Systems for Modal Logic",
      journal = "Archive for Mathematical Logic",
      volume = "48",
      number = "6",
      pages = "551--577",
      year = "2009",
      author = "Kai Br{\"u}nnler",
    }
    
  3. Syntactic Cut-Elimination for Common Knowledge
    with Thomas Studer

    January 12, 2009

    Annals of Pure and Applied Logic
    BibTeX entry
    @article{BrSt09,
      title = "Syntactic cut-elimination for common knowledge",
      journal = "Annals of Pure and Applied Logic",
      volume = "160",
      number = "1",
      pages = "82 - 95",
      year = "2009",
      issn = "0168-0072",
      doi = "DOI: 10.1016/j.apal.2009.01.014",
      author = "Kai Br{\"u}nnler and Thomas Studer",
    }
    
  4. Cut-Free Sequent Systems for Temporal Logic
    with Martin Lange

    March 27, 2008

    Journal of Logic and Algebraic Programming
    BibTeX entry
    @article{BrLa08,
      title = "Cut-free sequent systems for temporal logic",
      journal = "Journal of Logic and Algebraic Programming",
      volume = "76",
      number = "2",
      pages = "216 - 225",
      year = "2008",
      issn = "1567-8326",
      doi = "DOI: 10.1016/j.jlap.2008.02.004",
      author = "Kai Br{\"u}nnler and Martin Lange",
    }
    
  5. On Contraction and the Modal Fragment
    with Dieter Probst and Thomas Studer

    October 2007

    Mathematical Logic Quarterly
    BibTeX entry
    @article{BPS08,
      author = {Br{\"u}nnler, Kai and Probst, Dieter and Studer, Thomas},
      title = {On contraction and the modal fragment},
      year = {2008},
      journal = {Mathematical Logic Quarterly},
      volume = {54},
      number = {4},
      pages = {345{--}349},
    }
    
  6. Cut Elimination inside a Deep Inference System for Classical Predicate Logic

    February 9, 2006

    Studia Logica
    BibTeX entry
    @article{Bru06, 
      author = {Kai {Br\"unnler}}, 
      title = {Cut Elimination inside a Deep Inference System for Classical Predicate Logic}, 
      year = 2006, 
      number = 1, 
      journal = {Studia Logica}, 
      volume = 82, 
      pages = "51--71"
    }
    
  7. Locality for Classical Logic

    March 10, 2006

    Notre Dame Journal of Formal Logic
    BibTeX entry
    @article{BruLCL06,
      author = {Kai {Br\"unnler}},
      title = {Locality for Classical Logic},
      journal = {Notre Dame Journal of Formal Logic},
      year = {2006},
      volume = {47},
      pages = {557--580}
    }
    
  8. Two Restrictions on Contraction

    August 3, 2003

    Logic Journal of the IGPL
    BibTeX entry
    @article{BruRC03, 
      author = {Kai {Br\"unnler}}, 
      title = {Two Restrictions on Contraction}, 
      year = 2003, 
      number = 5, 
      journal = {Logic Journal of the IGPL}, 
      volume = 11, 
      pages = "525--529"
    }
    

Conferences

  1. How to Universally Close the Existential-Rule

    July 31, 2010

    LPAR 2010
    BibTeX entry
    @incollection{Bru10,
       author = {Br{\"u}nnler, Kai},
       title = {How to Universally Close the Existential Rule},
       booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning},
       series = {Lecture Notes in Computer Science},
       editor = {Ferm{\"u}ller, Christian and Voronkov, Andrei},
       publisher = {Springer},
       pages = {172-186},
       volume = {6397},
       url = {http://dx.doi.org/10.1007/978-3-642-16242-8_13},
       year = {2010},
       note = {\url{http://www.iam.unibe.ch/~kai/Papers/2010hucer.pdf}},
    }
    
  2. A Syntactic Realization Theorem for Justification Logics
    with Remo Goetschi and Roman Kuznets

    April 3, 2010

    AiML 2010
    BibTeX entry
    @incollection{BGK10,
      author = {Kai Br{\"u}nnler and Remo Goetschi and Roman Kuznets},
      title = {A Syntactic Realization Theorem for Justification Logics},
      booktitle = {Advances in Modal Logic, Volume 8},
      publisher = {College Publications},
      year = {2010},
      editor = {Lev Beklemishev and Valentin Goranko and Valentin Shehtman},
      pages = {39--58},
      note = {\url{http://www.iam.unibe.ch/~kai/Papers/2010srtjl.pdf}},
    }
    
  3. Modular Sequent Systems for Modal Logic
    with Lutz Straßburger

    February 2, 2009

    TABLEAUX 2009
    BibTeX entry
    @inproceedings{BrStr09,
      Author = {Br{\"u}nnler, Kai and Stra{\ss}burger, Lutz},
      Booktitle = {Tableaux 2009},
      Editor = {Giese, Martin and Waaler, Arild},
      Publisher = {Springer-Verlag},
      Series = {Lecture Notes in Computer Science},
      Title = {Modular Sequent Systems for Modal Logic},
      Volume = {5607},
      Year = {2009},
      Pages = {152--166}
    }
    
  4. An Algorithmic Interpretation of a Deep Inference System
    with Richard McKinley

    November 2008

    LPAR 2008
    BibTeX entry
    @inproceedings{BrMc08,
      Author = {Br{\"u}nnler, Kai and McKinley, Richard},
      Booktitle = {LPAR 2008},
      Editor = {Cervesato, I. and Veith, H. and Voronkov, A.},
      Pages = {482---496},
      Publisher = {Springer-Verlag},
      Series = {Lecture Notes in Computer Science},
      Title = {An Algorithmic Interpretation of a Deep Inference System},
      Volume = {5330},
      Year = {2008}
    }
    
  5. (Syntactic Cut-Elimination for Common Knowledge)
    superseded by the journal version
    with Thomas Studer

    November 2007

    M4M 2007
    BibTeX entry
    @article{BruStu07,
      author = {Kai Br{\"u}nnler and Thomas Studer},
      title = "Syntactic Cut-elimination for Common Knowledge",
      journal = "Electronic Notes in Theoretical Computer Science",
      volume = "231",
      number = "",
      pages = "227 - 240",
      year = "2009",
      note = "Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007)",
    }
    
  6. (Deep Sequent Systems for Modal Logic)
    superseded by the journal version

    March 24, 2006

    AiML 2006
    BibTeX entry
    @CONFERENCE{Bru06ds,
      author = {Br{\"u}nnler, Kai},
      title = {Deep Sequent Systems for Modal Logic},
      booktitle = {Advances in Modal Logic},
      year = {2006},
      editor = {Guido Governatori and Ian Hodkinson and Yde Venema},
      volume = {6},
      pages = {107--119},
      publisher = {College Publications}
    }
    
  7. Deep Inference and its Normal Form of Derivations

    March 29, 2006

    CiE 2006
    BibTeX entry
    @INPROCEEDINGS{Bru06nf,
      author = {Br{\"u}nnler, Kai},
      title = {Deep inference and its normal form of derivations},
      booktitle = {Logical Approaches to Computational Barriers, Second Conference on
    	Computability in Europe},
      year = {2006},
      editor = {Arnold Beckmann, Ulrich Berger, Benedikt L{\"o}we, John V Tucker},
      volume = {3988},
      series = {Lecture Notes in Computer Science},
      pages = {65--74},
      publisher = {Springer-Verlag}
    }
    
  8. (A First Order System with Finite Choice of Premises)
    superseded by my PhD thesis
    with Alessio Guglielmi

    November 30, 2003

    FOL75 2003
    BibTeX entry
    @INCOLLECTION{BruGugFin,
      author = {Br\"unnler, Kai and Guglielmi, Alessio},
      title = {A First Order System with Finite Choice of Premises},
      booktitle = {First-Order Logic Revisited},
      publisher = {Logos Verlag},
      year = {2004},
      editor = {Vincent Hendricks and Fabian Neuhaus and Stig Andur Pedersen and
    	Uwe Scheffler and Heinrich Wansing},
      pages = {59--74},
      city = {Berlin}
    }
    
  9. (Atomic Cut Elimination for Classical Logic)
    superseded by my PhD thesis

    April 10, 2003

    CSL 2003
    BibTeX entry
    @INPROCEEDINGS{BruACECL,
      author = {Br\"unnler, Kai},
      title = {Atomic Cut Elimination for Classical Logic},
      booktitle = {CSL 2003},
      year = {2003},
      editor = {M. Baaz and J. A. Makowsky},
      volume = {2803},
      series = {Lecture Notes in Computer Science},
      pages = {86--97},
      publisher = {Springer-Verlag}
    }
    
  10. (A Local System for Classical Logic)
    superseded by the journal version: Locality for Classical Logic
    with Alwen Fernanto Tiu

    October 2, 2001

    LPAR 2001
    BibTeX entry
    @INPROCEEDINGS{BruTiu01,
      author = {Br\"unnler, Kai and Tiu, Alwen Fernanto},
      title = {A Local System for Classical Logic},
      booktitle = {LPAR 2001},
      year = {2001},
      editor = {R. Nieuwenhuis and A. Voronkov},
      volume = {2250},
      series = {Lecture Notes in Artificial Intelligence},
      pages = {347--361},
      publisher = {Springer-Verlag}
    }
    

Workshops

  1. On Two Forms of Bureaucracy in Derivations
    with Stéphane Lengrand

    June 10, 2005

    Structures and Deduction 2005
    BibTeX entry
    @INPROCEEDINGS{BruLen05,
      author = {Br\"unnler, Kai and Lengrand, St\'ephane},
      title = {On Two Forms of Bureaucracy in Derivations},
      booktitle = {Structures and Deduction},
      year = {2005},
      editor = {Paola Bruscoli and {Fran{\c c}ois} Lamarche and Charles Stewart},
      pages = {69--80},
      publisher = {Technische Universit\"at Dresden}
    }
    

Theses

  1. Nested Sequents
    Habilitation Thesis, Universität Bern

    April 13, 2010

    BibTeX entry
    @misc{BruHabil,
       author =  {Kai Br\"unnler},
       title =   {Nested Sequents},
       school =  {Universit\"at Bern},
       year =    2010,
       url = {http://arxiv.org/abs/1004.1845v1},
       }
    
  2. Deep Inference and Symmetry in Classical Proofs
    PhD Thesis, Technische Universität Dresden
    Defended September 22, 2003

    Revised March 12, 2004

    It is also available as a book, © Logos Verlag Berlin.
    BibTeX entry
    @PHDTHESIS{BruTh,
      author = {Br\"unnler, Kai},
      title = {Deep Inference and Symmetry in Classical Proofs},
      school = {Technische Universit{\"a}t Dresden},
      year = {2003},
    }
    
  3. Mechanizing Coinduction with Maude

    May 2000

    Master's Thesis, Technische Universität Dresden
    BibTeX entry
    @MASTERSTHESIS{BruMS,
       author =  {Kai Br{\"u}nnler},
       title =   {Mechanizing Coinduction with Maude},
       school =  {Technische Universit{\"a}t Dresden},
       year =    2000
    }
    

Unpublished Notes

  1. Finitisation for Propositional Linear Temporal Logic

    May 3, 2006

    An exercise in using the small model property to get a cut-free finitary proof system.
  2. Deep inference for intuitionistic logic.

    February 7, 2006

  3. What's contraction good for?

    December 5, 2003

    A negative answer to the question by Alwen Tiu whether (KS - contraction) + cocontraction is complete.
  4. Deep inference for modal logic K

    2003

    Exercise: completeness by maximally consistent sets for a deep inference system for the modal logic K.