Compare commits
No commits in common. "c60ae342545468c8ea43c2ac3f44167b48da31e9" and "93e2f8d5e98c4d0d9a9fb1b93a271f1997aaa4b3" have entirely different histories.
c60ae34254
...
93e2f8d5e9
2 changed files with 26 additions and 56 deletions
|
@ -19,41 +19,41 @@ instance Language AlphaMIU where
|
||||||
|
|
||||||
axiom0 = [[M, I]]
|
axiom0 = [[M, I]]
|
||||||
infer1 =
|
infer1 =
|
||||||
[ miuRule1
|
[ mRule1
|
||||||
, miuRule2
|
, mRule2
|
||||||
, miuRule3
|
, mRule3
|
||||||
, miuRule4
|
, mRule4
|
||||||
]
|
]
|
||||||
|
|
||||||
-- RULE I: If you possess a string whose last letter is I, you can add on a U at the end.
|
-- RULE I: If you possess a string whose last letter is I, you can add on a U at the end.
|
||||||
miuRule1 :: StringMIU -> [StringMIU]
|
mRule1 :: StringMIU -> [StringMIU]
|
||||||
miuRule1 [I] = [[I, U]]
|
mRule1 [I] = [[I, U]]
|
||||||
miuRule1 (x:xs) = (x:) <$> miuRule1 xs
|
mRule1 (x:xs) = (x:) <$> mRule1 xs
|
||||||
miuRule1 _ = []
|
mRule1 _ = []
|
||||||
|
|
||||||
-- RULE II: Suppose you have Mx. Then you may add Mxx to your collection.
|
-- RULE II: Suppose you have Mx. Then you may add Mxx to your collection.
|
||||||
miuRule2 :: StringMIU -> [StringMIU]
|
mRule2 :: StringMIU -> [StringMIU]
|
||||||
miuRule2 string@(M:xs) = [string ++ xs]
|
mRule2 string@(M:xs) = [string ++ xs]
|
||||||
miuRule2 _ = []
|
mRule2 _ = []
|
||||||
|
|
||||||
-- RULE III: If III occurs in one of the strings in your collection, you may
|
-- RULE III: If III occurs in one of the strings in your collection, you may
|
||||||
-- make a new string with U in place of III.
|
-- make a new string with U in place of III.
|
||||||
miuRule3 :: StringMIU -> [StringMIU]
|
mRule3 :: StringMIU -> [StringMIU]
|
||||||
miuRule3 string@(M:xs) = (M:) <$> aux xs
|
mRule3 string@(M:xs) = (M:) <$> aux xs
|
||||||
where
|
where
|
||||||
aux (x@I:xs@(I:I:xs')) = (U:xs'):((x:) <$> aux xs)
|
aux (x@I:xs@(I:I:xs')) = (U:xs'):((x:) <$> aux xs)
|
||||||
aux (x:xs) = (x:) <$> aux xs
|
aux (x:xs) = (x:) <$> aux xs
|
||||||
aux _ = []
|
aux _ = []
|
||||||
miuRule3 _ = []
|
mRule3 _ = []
|
||||||
|
|
||||||
-- RULE IV: If UU occurs inside one of your strings, you can drop it.
|
-- RULE IV: If UU occurs inside one of your strings, you can drop it.
|
||||||
miuRule4 :: StringMIU -> [StringMIU]
|
mRule4 :: StringMIU -> [StringMIU]
|
||||||
miuRule4 string@(M:xs) = (M:) <$> aux xs
|
mRule4 string@(M:xs) = (M:) <$> aux xs
|
||||||
where
|
where
|
||||||
aux (x@U:xs@(U:xs')) = xs':((x:) <$> aux xs)
|
aux (x@U:xs@(U:xs')) = xs':((x:) <$> aux xs)
|
||||||
aux (x:xs) = (x:) <$> aux xs
|
aux (x:xs) = (x:) <$> aux xs
|
||||||
aux _ = []
|
aux _ = []
|
||||||
miuRule4 _ = []
|
mRule4 _ = []
|
||||||
|
|
||||||
{-
|
{-
|
||||||
ghci> map ConcatShowList infer0 :: [ConcatShowList AlphaMIU]
|
ghci> map ConcatShowList infer0 :: [ConcatShowList AlphaMIU]
|
||||||
|
|
48
readme.md
48
readme.md
|
@ -1,61 +1,31 @@
|
||||||
# statement logic !!!
|
# statement logic !!!
|
||||||
|
|
||||||
things that are in here:
|
things you can do with this:
|
||||||
|
|
||||||
### general statement things
|
### general things
|
||||||
|
|
||||||
#### [Logic/Statement/Parse.hs](Logic/Statement/Serialize.hs)
|
|
||||||
|
|
||||||
- parse string -> statement
|
- parse string -> statement
|
||||||
- serialize a statement -> plaintext, LaTeX, or L (the formal language)
|
|
||||||
|
|
||||||
#### [Logic/Language/Impl/L.hs](Logic/Language/Impl/L.hs)
|
|
||||||
|
|
||||||
- parse L (the formal language) string -> statement
|
- parse L (the formal language) string -> statement
|
||||||
|
- serialize a statement to plaintext, LaTeX, L (the formal language)
|
||||||
|
|
||||||
### semantic things (statements have meaning I guess)
|
### semantic things (statements have meaning I guess)
|
||||||
|
|
||||||
#### [Logic/Statement/Eval.hs](Logic/Statement/Eval.hs)
|
- evaluate statements
|
||||||
|
- from a statement generate a LaTeX truth table
|
||||||
- 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)
|
- match/replace patterns in statements (e.g. logical laws)
|
||||||
- verify logical-law equivalence of statements (TODO)
|
- verify logical-law equivalence of statements (TODO)
|
||||||
- find logical-law equivalence of statements with breadth-first search (slow)
|
- find logical-law equivalence of statements with breadth-first search
|
||||||
|
|
||||||
### syntactic things (statements are strings of symbols)
|
### syntactic things (statements are strings of symbols)
|
||||||
|
|
||||||
#### [Logic/Language.hs](Logic/Language.hs)
|
- implement formal languages (symbols, axioms schemas, and inference rules):
|
||||||
|
|
||||||
- implement formal languages (symbols, axioms schemas, and inference rules)
|
|
||||||
with a clunky api, see also
|
|
||||||
<https://en.wikipedia.org/wiki/Post_canonical_system>
|
<https://en.wikipedia.org/wiki/Post_canonical_system>
|
||||||
|
|
||||||
### [Logic/Language/Derivation.hs](Logic/Language/Derivation.hs)
|
|
||||||
|
|
||||||
- verify derivations in formal languages
|
- verify derivations in formal languages
|
||||||
|
|
||||||
### formal languages implemented
|
### formal languages implemented
|
||||||
|
|
||||||
- [the MIU system](Logic/Language/Impl/MIU.hs) (from "Gödel, Escher, Bach")
|
- the MIU system (from "Gödel, Escher, Bach")
|
||||||
- [L](Logic/Language/Impl/L.hs)
|
- L
|
||||||
|
|
||||||
### general things
|
|
||||||
|
|
||||||
#### [Logic/Parse.hs](Logic/Parse.hs)
|
|
||||||
|
|
||||||
- generic sequence parser
|
|
||||||
|
|
||||||
#### [Logic/Graph.hs](Logic/Graph.hs)
|
|
||||||
|
|
||||||
- generic breadth-first search
|
|
||||||
|
|
||||||
## requirements
|
## requirements
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue