# statement logic !!!

things that are in here:

## statement things

### [Logic/Statement/Parse.hs](Logic/Statement/Serialize.hs)

- parse string -> statement
- serialize a statement -> plaintext, LaTeX

### [Logic/Language/Impl/L.hs](Logic/Language/Impl/L.hs)

- serialize a statement -> L (the formal language)
- parse L (the formal language) string -> statement

## semantic statement things

### [Logic/Statement/Eval.hs](Logic/Statement/Eval.hs)

- assign truth values and evaluate statements
- determine tautology, contradiction, or contingent

### [Logic/Statement/Serialize.hs](Logic/Statement/Serialize.hs)

- generate a LaTeX truth table from a statement

### [Logic/Statements/Laws.hs](Logic/Statements/Laws.hs)

- match/replace patterns in statements (e.g. logical laws)
- verify logical-law equivalence of statements (TODO)
- find logical-law equivalence of statements with breadth-first search (slow)

## syntactic things

### [Logic/Language.hs](Logic/Language.hs)

- implement formal languages (symbols, axioms schemas, and inference rules)
  with a clunky api, see also
  <https://en.wikipedia.org/wiki/Post_canonical_system>

### [Logic/Language/Derivation.hs](Logic/Language/Derivation.hs)

- verify derivations in formal languages

### formal languages

- [the MIU system](Logic/Language/Impl/MIU.hs) (from "Gödel, Escher, Bach")
- [L](Logic/Language/Impl/L.hs)

## general things

### [Logic/Parse.hs](Logic/Parse.hs)

- generic sequence parser

### [Logic/Graph.hs](Logic/Graph.hs)

- generic breadth-first search


# requirements

a haskell compiler e.g. GHC

# compile it

```sh
make
```

or look in [`Makefile`](Makefile)


# usage

only this has been implemented in the main function:

```sh
echo '((p->q)<->(!q->!p))' | ./logic
```

### output

```
Iff (Implies (Atom "p") (Atom "q")) (Implies (Not (Atom "q")) (Not (Atom "p")))
Tautology
\begin{tabular}{cc||cccccc|c|cccccccc}
$p$ & $q$ & $($ & $($ & $p$ & $\to $ & $q$ & $)$ & $\leftrightarrow $ & $($ & $\neg $ & $q$ & $\to $ & $\neg $ & $p$ & $)$ & $)$ \\
\hline
0 & 0 &  &  & 0 & 1 & 0 &  & \textbf 1 &  & 1 & 0 & 1 & 1 & 0 &  & \\
0 & 1 &  &  & 1 & 0 & 0 &  & \textbf 1 &  & 1 & 0 & 0 & 0 & 1 &  & \\
1 & 0 &  &  & 0 & 1 & 1 &  & \textbf 1 &  & 0 & 1 & 1 & 1 & 0 &  & \\
1 & 1 &  &  & 1 & 1 & 1 &  & \textbf 1 &  & 0 & 1 & 1 & 0 & 1 &  & \\
\end{tabular}
```