Hai Dang

Saarland University Computer Science

Research Immersion Lab: Results on Propositional Logic

Advisor: Prof. Dr. Gert Smolka


We study the properties of Propositional Logic in both classical and intuitionistic formulations. We formalize constructive proofs of results known from proof theory and model theory. This includes the studies of natural deduction systems, Gentzen's sequent calculi, and Hilbert systems. We study 2 models for intuitionistic logic: Kripke structures and Heyting algebras and their connection. We also study the decision procedures of semantic tableaux for classical logic (Beth, Smullyan) and intuitionistic logic (Kripke, Fitting). The intuitionistic tableau system give insights to the process of finding countermodels, and a connection between the two logics.

Attached Documents

Reference List

Hai Dang, Fri Oct 23 15:51:00 2015