#  minimal-logic 

## Proof assistant

Part of this programme is a proof assistant. This lets you construct proofs of statements in minimal logic composably. It also keeps track of assumptions for you.

### Example

The Curry-Howard correspondence can be interpreted as an equivalence between types and deductions where for example the composition of functions corresponds to the composition of implications.

import Minimal

compose :: Deduction -> Deduction -> Proof
compose dAB dBC = do
-- get the antecedent of the conclusion of dAB
let (Implication a _) = conclusion dAB
dA  <- assume a
dB  <- implElim dA dAB
dC  <- implElim dB dBC
dAC <- implIntro a dC
return dAC

pAB, pBC :: Proof
pAC = do
dAB <- pAB
dBC <- pBC
compose dAB dBC


## Model checker

The other half is the model checker. This lets you construct models and then check whether formulae are or are not forced by those models.

### Example

A model with only a single world is a model of classical logic.

import Model

exampleWorld :: World
exampleWorld = World
{ forcedProps = Set.singleton (Proposition "P")
, childWorlds = Set.empty
, name = "W"
}

example :: Model
example = Model
{ abnormalWorlds = Set.empty
, rootWorld = exampleWorld
}