Merge pull request #135 from zacharybonagura/master

Updated images, new biconditional rule category, parsing update
Bram-Hub · Oct 18, 2024 · 8b386a7 · 8b386a7
2 parents fce5e3c + 3645722
commit 8b386a7
Show file tree

Hide file tree

Showing 38 changed files with 281 additions and 197 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/aris/src/equivs.rs b/aris/src/equivs.rs
@@ -120,13 +120,6 @@ define_rewrite_rule! {
     ]
 }
 // equivalence
-define_rewrite_rule! {
-    CONDITIONAL_BIIMPLICATION,
-    &[
-        ("(phi -> psi) & (psi -> phi)", "phi <-> psi"),
-        ("(phi & psi) | (~phi & ~psi)", "phi <-> psi"),
-    ]
-}
 define_rewrite_rule! {
     CONDITIONAL_CONTRAPOSITION,
     &[
@@ -172,11 +165,12 @@ define_rewrite_rule! {
         ("~phi -> phi", "phi"),
     ]
 }
+
+// Biconditional Equivalences
 define_rewrite_rule! {
-    BICONDITIONAL_NEGATION,
+    BICONDITIONAL_ASSOCIATION,
     &[
-        ("~phi <-> psi", "~(phi <-> psi)"),
-        ("phi <-> ~psi", "~(phi <-> psi)"),
+        ("phi <-> (psi <-> lambda)", "(phi <-> psi) <-> lambda"),
     ]
 }
 define_rewrite_rule! {
@@ -186,9 +180,17 @@ define_rewrite_rule! {
     ]
 }
 define_rewrite_rule! {
-    BICONDITIONAL_ASSOCIATION,
+    BICONDITIONAL_EQUIVALENCE,
     &[
-        ("phi <-> (psi <-> lambda)", "(phi <-> psi) <-> lambda"),
+        ("(phi -> psi) & (psi -> phi)", "phi <-> psi"),
+        ("(phi & psi) | (~phi & ~psi)", "phi <-> psi"),
+    ]
+}
+define_rewrite_rule! {
+    BICONDITIONAL_NEGATION,
+    &[
+        ("~phi <-> psi", "~(phi <-> psi)"),
+        ("phi <-> ~psi", "~(phi <-> psi)"),
     ]
 }
 define_rewrite_rule! {
@@ -220,7 +222,7 @@ mod tests {
     #[test]
     fn bruteforce_equivalence_truthtables() {
         use std::collections::HashMap;
-        let rules: Vec<&RewriteRule> = vec![&*DOUBLE_NEGATION, &*DISTRIBUTION, &*COMPLEMENT, &*IDENTITY, &*ANNIHILATION, &*INVERSE, &*ABSORPTION, &*REDUCTION, &*ADJACENCY, &*CONDITIONAL_ANNIHILATION, &*CONDITIONAL_IMPLICATION, &*CONDITIONAL_CONTRAPOSITION, &*CONDITIONAL_CURRYING, &*CONDITIONAL_COMPLEMENT, &*CONDITIONAL_IDENTITY, &*CONDITIONAL_BIIMPLICATION, &*CONDITIONAL_DISTRIBUTION, &*CONDITIONAL_REDUCTION, &*KNIGHTS_AND_KNAVES, &*CONDITIONAL_IDEMPOTENCE, &*BICONDITIONAL_NEGATION, &*BICONDITIONAL_COMMUTATION, &*BICONDITIONAL_ASSOCIATION, &*BICONDITIONAL_SUBSTITUTION];
+        let rules: Vec<&RewriteRule> = vec![&*DOUBLE_NEGATION, &*DISTRIBUTION, &*COMPLEMENT, &*IDENTITY, &*ANNIHILATION, &*INVERSE, &*ABSORPTION, &*REDUCTION, &*ADJACENCY, &*CONDITIONAL_ANNIHILATION, &*CONDITIONAL_IMPLICATION, &*CONDITIONAL_CONTRAPOSITION, &*CONDITIONAL_CURRYING, &*CONDITIONAL_COMPLEMENT, &*CONDITIONAL_IDENTITY, &*CONDITIONAL_DISTRIBUTION, &*CONDITIONAL_REDUCTION, &*KNIGHTS_AND_KNAVES, &*CONDITIONAL_IDEMPOTENCE, &*BICONDITIONAL_ASSOCIATION, &*BICONDITIONAL_COMMUTATION, &*BICONDITIONAL_EQUIVALENCE, &*BICONDITIONAL_NEGATION, &*BICONDITIONAL_SUBSTITUTION];
         for rule in rules {
             for (lhs, rhs) in rule.reductions.iter() {
                 println!("Testing {lhs} -> {rhs}");