readme: verbose

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]

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
   <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 (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