A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic

Abstract

Claessen and R´osen have recently presented an automated theorem prover, intuit, for intuitionistic propositional logic which utilises a SAT-solver. We present a sequent calculus perspective of the theory underpinning intuit by showing that it implements a generalisation of the implication-left rule from the sequent calculus LJT, also known as G4ip and popularised by Roy Dyckhoff. Show more