Maxixe is a simple proof-checking language. Given a proof written out fully and explicitly (including all rules of inference), a computer can check if it is valid or not.

## Sample Program

```
given
Modus_Ponens = impl(P, Q) ; P |- Q
Simplification = and(P, Q) |- Q
Commutativity_of_Conjunction = and(P, Q) |- and(Q, P)
Premise = |- and(p, impl(p, q))
show
q
proof
Step_1 = and(p, impl(p, q)) by Premise
Step_2 = and(impl(p, q), p) by Commutativity_of_Conjunction with Step_1
Step_3 = impl(p, q) by Simplification with Step_1
Step_4 = p by Simplification with Step_2
Step_5 = q by Modus_Ponens with Step_3, Step_4
qed
```

## Computational Class

## Programming Paradigms

## Defined by

Maxixe distribution

## Documentation

## Download

## Development

Github: catseye/Maxixe

Issue tracker: on github