Emma Bastås: A proof searching procedure for intuitionistic propositional logic in Agda

Abstract.

Sequent calculus for intuitionistic propositional logic (IPC) is briefly presented and later formalized in Agda, an interactive theorem prover. The main result of this thesis is a proof searching procedure for IPC using sequent calculus, which is proven correct in Agda. We facilitate this in two ways; first by restricting the “normal” sequent calculus into a “contraction-free” version along the lines of R. Dyckhoff [1], guaranteeing termination of the search procedure. Secondly, the decision procedure itself is encoded in the inference rules, similarly to the “focused” sequent calculus of R. J. Simmons [2], leaving us with a slightly more complicated set of inference rules, but also a search procedure that is correct almost by construction. In the end, we end up with a sequent calculus LJf¹ for which a search procedure is implemented and proven correct in Agda.