Friday 23 September, 10:30: A Unified Procedure for Provability and Counter-Model Generation in Minimal Implicational Logic​​, Jefferson Santos (Pontifícia Universidade Católica do Rio de Janeiro, Brazil).

Abstract. This presentation shows results on the definition of a sequent calculus for Minimal Implicational Propositional Logic (M→) aimed to be used for provability and counter-model generation in this logic. The system tracks the attempts to construct a proof in such a way that, if the original formula is a M→ tautology, the tree structure produced by the proving process is a proof, otherwise, it is used to construct a counter-model using Kripke semantics.

Bio. Doctoral student in Computer Science at Pontifícia Universidade Católica of Rio de Janeiro (PUC-Rio). He has got his M.Sc. and B.Sc. at the same university. Nowadays, he is IT coordinator at Brazilian School of Public and Business Administration of the Getulio Vargas Foundation (EBAPE/FGV). He is also an undergraduate professor of IT subjects in the same institution. He also teaches the Introduction to Logic course at PUC-Rio for Engineering and Computer Science students. He is visiting Deducteam until December 2016.