diff --git a/Logic/Language/Impl/MIU.hs b/Logic/Language/Impl/MIU.hs index 9b52411..24a4093 100644 --- a/Logic/Language/Impl/MIU.hs +++ b/Logic/Language/Impl/MIU.hs @@ -19,41 +19,41 @@ instance Language AlphaMIU where axiom0 = [[M, I]] infer1 = - [ mRule1 - , mRule2 - , mRule3 - , mRule4 + [ miuRule1 + , miuRule2 + , miuRule3 + , miuRule4 ] -- RULE I: If you possess a string whose last letter is I, you can add on a U at the end. -mRule1 :: StringMIU -> [StringMIU] -mRule1 [I] = [[I, U]] -mRule1 (x:xs) = (x:) <$> mRule1 xs -mRule1 _ = [] +miuRule1 :: StringMIU -> [StringMIU] +miuRule1 [I] = [[I, U]] +miuRule1 (x:xs) = (x:) <$> miuRule1 xs +miuRule1 _ = [] -- RULE II: Suppose you have Mx. Then you may add Mxx to your collection. -mRule2 :: StringMIU -> [StringMIU] -mRule2 string@(M:xs) = [string ++ xs] -mRule2 _ = [] +miuRule2 :: StringMIU -> [StringMIU] +miuRule2 string@(M:xs) = [string ++ xs] +miuRule2 _ = [] -- 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. -mRule3 :: StringMIU -> [StringMIU] -mRule3 string@(M:xs) = (M:) <$> aux xs +miuRule3 :: StringMIU -> [StringMIU] +miuRule3 string@(M:xs) = (M:) <$> aux xs where aux (x@I:xs@(I:I:xs')) = (U:xs'):((x:) <$> aux xs) aux (x:xs) = (x:) <$> aux xs aux _ = [] -mRule3 _ = [] +miuRule3 _ = [] -- RULE IV: If UU occurs inside one of your strings, you can drop it. -mRule4 :: StringMIU -> [StringMIU] -mRule4 string@(M:xs) = (M:) <$> aux xs +miuRule4 :: StringMIU -> [StringMIU] +miuRule4 string@(M:xs) = (M:) <$> aux xs where aux (x@U:xs@(U:xs')) = xs':((x:) <$> aux xs) aux (x:xs) = (x:) <$> aux xs aux _ = [] -mRule4 _ = [] +miuRule4 _ = [] {- ghci> map ConcatShowList infer0 :: [ConcatShowList AlphaMIU] diff --git a/readme.md b/readme.md index 0f0c19d..67afc16 100644 --- a/readme.md +++ b/readme.md @@ -1,31 +1,61 @@ # statement logic !!! -things you can do with this: +things that are in here: -### general things +### general statement things + +#### [Logic/Statement/Parse.hs](Logic/Statement/Serialize.hs) - 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 -- serialize a statement to plaintext, LaTeX, L (the formal language) ### semantic things (statements have meaning I guess) -- evaluate statements -- from a statement generate a LaTeX truth table +#### [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 +- find logical-law equivalence of statements with breadth-first search (slow) ### syntactic things (statements are strings of symbols) -- implement formal languages (symbols, axioms schemas, and inference rules): +#### [Logic/Language.hs](Logic/Language.hs) + +- implement formal languages (symbols, axioms schemas, and inference rules) + with a clunky api, see also + +### [Logic/Language/Derivation.hs](Logic/Language/Derivation.hs) + - verify derivations in formal languages ### formal languages implemented -- the MIU system (from "Gödel, Escher, Bach") -- L +- [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