Some Results in Proof Theory and Automated Reasoning

Bruno Woltzenlogel Paleo

Bruno Wolztenlogel Paleo (Input Output HK) will present "Some Results in Proof Theory and Automated Reasoning" at 11 on Thursday, 20 December in Old Quad G10.

Abstract:  Despite being in Canberra for a while, this will be the first time I will give a talk at the University of Melbourne. Therefore, I assume that the audience is not acquainted with my research in the fields of proof theory and automated reasoning yet. I also believe that the logic community in Melbourne has a very wide range of interests. Therefore, instead of talking about a single topic, I intend to give an overview of some of my results, possibly including the Conflict Resolution calculus, translations between Resolution and Sequent Calculus, para-disagreement logics, the formalization of Gödel’s Ontological Argument, proof compression algorithms for proofs generated by Sat and SMT solvers, a Contextual Natural Deduction calculus, cut-elimination and cut-introduction. I will discuss why and how IOHK is applying logic and formal methods to cryptocurrencies and blockchain technologies. Hopefully, there will be something for everyone in this talk and we will get acquainted with each other’s interests.