Meredith

Meredith¹ is an interactive environment for $L{\to}$, the positive implicational fragment of intuitionistic propositional logic. This currently implements a parser and a 'resolution rule'², condensed detachment, for $L{\to}$. Condensed detachment does some substitution and modus ponens on a pair of $L{\to}$ formulae, and makes use of the Unification algorithm from Hindley-Milner type inference.

An overview of some background material is here.³

Installation

Provided you have GHC, stack, etc., installed, clone this repository and run in the /positive-imp directory:

$ stack setup
$ stack build
$ stack exec positive-imp-exe

You will be greeted with a REPL to compute (condensed) detachments:

These input formulae are written prefix-style, using $C$ for ${\to}$, and compute the final detachment in this paper. The conclusion $CCp_2Cp_0p_1CCp_2p_0Cp_2p_1$ is ${\alpha}$-equivalent to $CCpCqrCCpqCpr$. There is also a parser to go between prefix and infix notation for formulae.

This is a work in progress.

Footnotes

1. Named after C.A. Meredith and David Meredith ↩

2. Hindley, J.R. (1997), Basic Simple Type Theory, p.93 ↩

3. See also Hindley, J.R. & Meredith, D. (1990), 'Principal Type-Schemes and Condensed Detachment', The Journal of Symbolic Logic, 55(1):90–105 ↩