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