Documentation and clean up code

Bram-Hub · Dec 24, 2024 · c296abe · c296abe
1 parent 8928835
commit c296abe
Show file tree

Hide file tree

Showing 14 changed files with 317 additions and 171 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/aris/Cargo.toml b/aris/Cargo.toml
@@ -1,8 +1,11 @@
 [package]
 name = "aris"
 version = "0.1.0"
-authors = ["Avi Weinstock <[email protected]>"]
+authors = ["Avi Weinstock <[email protected]>", "Zach Bonagura <[email protected]>"]
 edition = "2021"
+description = "Aris is a formal logic proof-building tool designed to help users learn and practice logic."
+repository = "https://github.com/Bram-Hub/aris"
+license = "GPL-3.0"
 
 [dependencies]
 base64 = "0.21.0"

diff --git a/aris/src/equivs.rs b/aris/src/equivs.rs
@@ -35,13 +35,6 @@ define_rewrite_rule! {
         ("(P | Q) & (P | R)", "P | (Q & R)"),
     ]
 }
-define_rewrite_rule! {
-    COMPLEMENT,
-    &[
-        ("phi & ~phi", "_|_"),
-        ("phi | ~phi", "^|^"),
-    ]
-}
 define_rewrite_rule! {
     IDENTITY,
     &[
@@ -63,29 +56,6 @@ define_rewrite_rule! {
         ("~_|_", "^|^"),
     ]
 }
-define_rewrite_rule! {
-    ABSORPTION,
-    &[
-        ("phi & (phi | psi)", "phi"),
-        ("phi | (phi & psi)", "phi"),
-    ]
-}
-define_rewrite_rule! {
-    REDUCTION,
-    &[
-        ("phi & (~phi | psi)", "phi & psi"),
-        ("~phi & (phi | psi)", "~phi & psi"),
-        ("phi | (~phi & psi)", "phi | psi"),
-        ("~phi | (phi & psi)", "~phi | psi"),
-    ]
-}
-define_rewrite_rule! {
-    ADJACENCY,
-    &[
-        ("(phi | psi) & (phi | ~psi)", "phi"),
-        ("(phi & psi) | (phi & ~psi)", "phi"),
-    ]
-}
 
 // Conditional Equivalences
 define_rewrite_rule! {
@@ -175,12 +145,6 @@ define_rewrite_rule! {
         ("(phi & psi) | (~phi & ~psi)", "phi <-> psi"),
     ]
 }
-define_rewrite_rule! {
-    BICONDITIONAL_CONTRAPOSITION,
-    &[
-        ("phi <-> psi", "psi <-> phi"),
-    ]
-}
 define_rewrite_rule! {
     BICONDITIONAL_COMMUTATION,
     &[
@@ -247,10 +211,11 @@ mod tests {
         }
     }
 
+    /// Test function to verify the logical equivalence of rewrite rules using brute-force truth tables.
     #[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_ABSORPTION, &*CONDITIONAL_ANNIHILATION, &*CONDITIONAL_IMPLICATION, &*CONDITIONAL_CONTRAPOSITION, &*CONDITIONAL_EXPORTATION, &*CONDITIONAL_COMPLEMENT, &*CONDITIONAL_IDENTITY, &*CONDITIONAL_DISTRIBUTION, &*CONDITIONAL_REDUCTION, &*KNIGHTS_AND_KNAVES, &*CONDITIONAL_IDEMPOTENCE, &*BICONDITIONAL_CONTRAPOSITION, &*BICONDITIONAL_ASSOCIATION, &*BICONDITIONAL_COMMUTATION, &*BICONDITIONAL_REDUCTION, &*BICONDITIONAL_COMPLEMENT, &*BICONDITIONAL_IDENTITY, &*BICONDITIONAL_EQUIVALENCE, &*BICONDITIONAL_NEGATION, &*BICONDITIONAL_SUBSTITUTION];
+        let rules: Vec<&RewriteRule> = vec![&*DOUBLE_NEGATION, &*DISTRIBUTION, &*IDENTITY, &*ANNIHILATION, &*INVERSE, &*CONDITIONAL_ABSORPTION, &*CONDITIONAL_ANNIHILATION, &*CONDITIONAL_IMPLICATION, &*CONDITIONAL_CONTRAPOSITION, &*CONDITIONAL_EXPORTATION, &*CONDITIONAL_COMPLEMENT, &*CONDITIONAL_IDENTITY, &*CONDITIONAL_DISTRIBUTION, &*CONDITIONAL_REDUCTION, &*KNIGHTS_AND_KNAVES, &*CONDITIONAL_IDEMPOTENCE, &*BICONDITIONAL_ASSOCIATION, &*BICONDITIONAL_COMMUTATION, &*BICONDITIONAL_REDUCTION, &*BICONDITIONAL_COMPLEMENT, &*BICONDITIONAL_IDENTITY, &*BICONDITIONAL_EQUIVALENCE, &*BICONDITIONAL_NEGATION, &*BICONDITIONAL_SUBSTITUTION];
         for rule in rules {
             for (lhs, rhs) in rule.reductions.iter() {
                 println!("Testing {lhs} -> {rhs}");