94 lines
2.4 KiB
Markdown
94 lines
2.4 KiB
Markdown
# statement logic !!!
|
|
|
|
things that are in here:
|
|
|
|
### general 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 things (statements have meaning I guess)
|
|
|
|
#### [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 (statements are strings of symbols)
|
|
|
|
#### [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 implemented
|
|
|
|
- [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}
|
|
```
|