Logic and Computation Courses

Introductory Courses

Semantics based proof-search methods for non-classical logics

Camillo Fiorentini

Week 1, August 3-7, 2020


Proof theory for non-classical logics has been deeply investigated. Standard techniques to prove the completeness of a calculus are based on syntactic methods, mostly relying on cut-elimination. The main drawback is that, from a failed proof-search, no information about the non-validity of a formula is gained. An alternative way is to exploit semantics: to prove that a calculus is complete, one has to show that, whenever a formula is not provable in the calculus, a countermodel for it can be built.

A countermodel can be viewed as a certificate of the non-validity of a formula; moreover, from an inspection of the completeness proof, one can design efficient proof-search strategies for the calculus at hand. In the course we present efficient proof-search strategies supporting countermodel generation, focusing on Intuitionistic Propositional Logic. We present the main ideas beyond the technique and some significant examples.

Connect with us

32nd European Summer School in Logic, Language and Information - ESSLLI 2021
Please send any queries to

  • esslli@uu.nl