FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic

Author: Paul Tarau

Paper Information

Title:Shaving with Occam's Razor: Deriving Minimalist Theorem Provers for Minimal Logic
Authors:Paul Tarau
Proceedings:RCRA Full papers
Editor: Marco Maratea
Keywords:Curry-Howard isomorphism, propositional implicational intuitionistic logic, type inference and type inhabitation, simply typed lambda terms, theorem proving, declarative algorithms, logic programming, combinatorial search algorithms
Abstract:

ABSTRACT. Proving a theorem in intuitionistic propositional logic, with {\em implication} as its only primitive (also called minimal logic), is known as one of the simplest to state PSPACE-complete problem. At the same time, via the Curry-Howard isomorphism, it is instrumental to finding lambda terms that may inhabit a given type.

However, as hundreds of papers witness it, all starting with Gentzen's {\bf LJ} calculus, conceptual simplicity has not come in this case with comparable computational counterparts. Implementing such theorem provers faces challenges related not only to soundness and completeness but also to termination and scalability problems.

Can a simple solution, in the tradition of "lean theorem provers" be uncovered that matches the conceptual simplicity of the problem, while being able to handle also large randomly generated formulas?

In search for an answer, starting from Dyckhoff's {\bf LJT calculus}, we derive a sequence of minimalist theorem provers using declarative program transformations steps, while highlighting connections, via the Curry-Howard isomorphism, to type inference mechanisms for the simply typed lambda calculus.

We chose Prolog as our meta-language. Being derived from essentially the same formalisms as those we are covering reduces the semantic gap and results in surprisingly concise and efficient declarative implementations. Our implementation is available at: {\bf \url{https://github.com/ptarau/TypesAndProofs}}.

Pages:16
Talk:Jul 13 11:00 (Session 86J: Logic)
Paper: