diff --git a/Cargo.lock b/Cargo.lock index bf05fd3f..fc5b6388 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -28,9 +28,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.93" +version = "1.0.94" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c95c10ba0b00a02636238b814946408b1322d5ac4760326e6fb8ec956d85775" +checksum = "c1fd03a028ef38ba2276dce7e33fcd6369c158a1bca17946c4b1b701891c1ff7" [[package]] name = "anymap2" @@ -204,9 +204,9 @@ checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b" [[package]] name = "bytes" -version = "1.8.0" +version = "1.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9ac0150caa2ae65ca5bd83f25c7de183dea78d4d366469f148435e2acfbad0da" +checksum = "325918d6fe32f23b19878fe4b34794ae41fc19ddbe53b10571a4874d44ffd39b" [[package]] name = "cbindgen" @@ -335,7 +335,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "13b588ba4ac1a99f7f2964d24b3d896ddc6bf847ee3855dbd4366f058cfcd331" dependencies = [ "quote", - "syn 2.0.89", + "syn 2.0.90", ] [[package]] @@ -359,7 +359,7 @@ dependencies = [ "proc-macro2", "quote", "rustc_version", - "syn 2.0.89", + "syn 2.0.90", ] [[package]] @@ -407,12 +407,12 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" [[package]] name = "errno" -version = "0.3.9" +version = "0.3.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "534c5cf6194dfab3db3242765c03bbe257cf92f22b38f6bc0c58d59108a820ba" +checksum = "33d852cb9b869c2a9b3df2f71a3074817f01e1844f839a144f5fcef059a4eb5d" dependencies = [ "libc", - "windows-sys 0.52.0", + "windows-sys", ] [[package]] @@ -427,9 +427,9 @@ dependencies = [ [[package]] name = "fastrand" -version = "2.2.0" +version = "2.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "486f806e73c5707928240ddc295403b1b93c96a02038563881c4a2fd84b81ac4" +checksum = "37909eebbb50d72f9059c3b6d82c0463f2ff062c9e95845c43a6c9c0355411be" [[package]] name = "fixedbitset" @@ -515,7 +515,7 @@ checksum = "162ee34ebcb7c64a8abebc059ce0fee27c2262618d7b60ed8faf72fef13c3650" dependencies = [ "proc-macro2", "quote", - "syn 2.0.89", + "syn 2.0.90", ] [[package]] @@ -849,9 +849,9 @@ dependencies = [ [[package]] name = "indexmap" -version = "2.6.0" +version = "2.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "707907fe3c25f5424cce2cb7e1cbcafee6bdbe735ca90ef77c29e84591e5b9da" +checksum = "62f822373a4fe84d4bb149bf54e584a7f4abec90e072ed49cda0edea5b95471f" dependencies = [ "equivalent", "hashbrown 0.15.2", @@ -900,10 +900,11 @@ checksum = "8eaf4bc02d17cbdd7ff4c7438cafcdf7fb9a4613313ad11b4f8fefe7d3fa0130" [[package]] name = "js-sys" -version = "0.3.72" +version = "0.3.76" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6a88f1bda2bd75b0452a14784937d796722fdebfe50df998aeb3f0b7603019a9" +checksum = "6717b6b5b077764fb5966237269cb3c64edddde4b14ce42647430a78ced9e7b7" dependencies = [ + "once_cell", "wasm-bindgen", ] @@ -921,9 +922,9 @@ checksum = "884e2677b40cc8c339eaefcb701c32ef1fd2493d71118dc0ca4b6a736c93bd67" [[package]] name = "libc" -version = "0.2.166" +version = "0.2.168" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c2ccc108bbc0b1331bd061864e7cd823c0cab660bbe6970e66e2c0614decde36" +checksum = "5aaeb2981e0606ca11d79718f8bb01164f1d6ed75080182d3abf017e6d244b6d" [[package]] name = "linux-raw-sys" @@ -1127,7 +1128,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b4c5cc86750666a3ed20bdaf5ca2a0344f9c67674cae0515bec2da16fbaa47db" dependencies = [ "fixedbitset", - "indexmap 2.6.0", + "indexmap 2.7.0", ] [[package]] @@ -1239,7 +1240,7 @@ checksum = "3c0f5fad0874fc7abcd4d750e76917eaebbecaa2c20bde22e1dbeeba8beb758c" dependencies = [ "proc-macro2", "quote", - "syn 2.0.89", + "syn 2.0.90", ] [[package]] @@ -1497,15 +1498,15 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.41" +version = "0.38.42" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d7f649912bc1495e167a6edee79151c84b1bad49748cb4f1f1167f459f6224f6" +checksum = "f93dc38ecbab2eb790ff964bb77fa94faf256fd3e73285fd7ba0903b76bedb85" dependencies = [ "bitflags 2.6.0", "errno", "libc", "linux-raw-sys", - "windows-sys 0.52.0", + "windows-sys", ] [[package]] @@ -1605,7 +1606,7 @@ checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.89", + "syn 2.0.90", ] [[package]] @@ -1744,9 +1745,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.89" +version = "2.0.90" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44d46482f1c1c87acd84dea20c1bf5ebff4c757009ed6bf19cfd36fb10e92c4e" +checksum = "919d3b74a5dd0ccd15aeb8f93e7006bd9e14c295087c9896a110f490752bcf31" dependencies = [ "proc-macro2", "quote", @@ -1775,7 +1776,7 @@ dependencies = [ "fastrand", "once_cell", "rustix", - "windows-sys 0.59.0", + "windows-sys", ] [[package]] @@ -1827,14 +1828,14 @@ checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" dependencies = [ "proc-macro2", "quote", - "syn 2.0.89", + "syn 2.0.90", ] [[package]] name = "tokio" -version = "1.41.1" +version = "1.42.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "22cfb5bee7a6a52939ca9224d6ac897bb669134078daa8735560897f69de4d33" +checksum = "5cec9b21b0450273377fc97bd4c33a8acffc8c996c987a7c5b319a0083707551" dependencies = [ "backtrace", "pin-project-lite", @@ -1842,9 +1843,9 @@ dependencies = [ [[package]] name = "tokio-stream" -version = "0.1.16" +version = "0.1.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4f4e6ce100d0eb49a2734f8c0812bcd324cf357d21810932c5df6b96ef2b86f1" +checksum = "eca58d7bba4a75707817a2c44174253f9236b2d5fbd055602e9d5c07c139a047" dependencies = [ "futures-core", "pin-project-lite", @@ -1879,7 +1880,7 @@ checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d" dependencies = [ "proc-macro2", "quote", - "syn 2.0.89", + "syn 2.0.90", ] [[package]] @@ -2053,9 +2054,9 @@ checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" [[package]] name = "wasm-bindgen" -version = "0.2.95" +version = "0.2.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "128d1e363af62632b8eb57219c8fd7877144af57558fb2ef0368d0087bddeb2e" +checksum = "a474f6281d1d70c17ae7aa6a613c87fce69a127e2624002df63dcb39d6cf6396" dependencies = [ "cfg-if", "once_cell", @@ -2066,36 +2067,36 @@ dependencies = [ [[package]] name = "wasm-bindgen-backend" -version = "0.2.95" +version = "0.2.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cb6dd4d3ca0ddffd1dd1c9c04f94b868c37ff5fac97c30b97cff2d74fce3a358" +checksum = "5f89bb38646b4f81674e8f5c3fb81b562be1fd936d84320f3264486418519c79" dependencies = [ "bumpalo", "log", - "once_cell", "proc-macro2", "quote", - "syn 2.0.89", + "syn 2.0.90", "wasm-bindgen-shared", ] [[package]] name = "wasm-bindgen-futures" -version = "0.4.45" +version = "0.4.49" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cc7ec4f8827a71586374db3e87abdb5a2bb3a15afed140221307c3ec06b1f63b" +checksum = "38176d9b44ea84e9184eff0bc34cc167ed044f816accfe5922e54d84cf48eca2" dependencies = [ "cfg-if", "js-sys", + "once_cell", "wasm-bindgen", "web-sys", ] [[package]] name = "wasm-bindgen-macro" -version = "0.2.95" +version = "0.2.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e79384be7f8f5a9dd5d7167216f022090cf1f9ec128e6e6a482a2cb5c5422c56" +checksum = "2cc6181fd9a7492eef6fef1f33961e3695e4579b9872a6f7c83aee556666d4fe" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -2103,28 +2104,28 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.95" +version = "0.2.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "26c6ab57572f7a24a4985830b120de1594465e5d500f24afe89e16b4e833ef68" +checksum = "30d7a95b763d3c45903ed6c81f156801839e5ee968bb07e534c44df0fcd330c2" dependencies = [ "proc-macro2", "quote", - "syn 2.0.89", + "syn 2.0.90", "wasm-bindgen-backend", "wasm-bindgen-shared", ] [[package]] name = "wasm-bindgen-shared" -version = "0.2.95" +version = "0.2.99" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "65fc09f10666a9f147042251e0dda9c18f166ff7de300607007e96bdebc1068d" +checksum = "943aab3fdaaa029a6e0271b35ea10b72b943135afe9bffca82384098ad0e06a6" [[package]] name = "web-sys" -version = "0.3.72" +version = "0.3.76" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f6488b90108c040df0fe62fa815cbdee25124641df01814dd7282749234c6112" +checksum = "04dd7223427d52553d3702c004d3b2fe07c148165faa56313cb00211e31c12bc" dependencies = [ "js-sys", "wasm-bindgen", @@ -2152,7 +2153,7 @@ version = "0.1.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cf221c93e13a30d793f7645a0e7762c55d169dbb0a49671918a2319d289b10bb" dependencies = [ - "windows-sys 0.59.0", + "windows-sys", ] [[package]] @@ -2161,15 +2162,6 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" -[[package]] -name = "windows-sys" -version = "0.52.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" -dependencies = [ - "windows-targets", -] - [[package]] name = "windows-sys" version = "0.59.0" @@ -2245,9 +2237,9 @@ checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" [[package]] name = "xml-rs" -version = "0.8.23" +version = "0.8.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "af310deaae937e48a26602b730250b4949e125f468f11e6990be3e5304ddd96f" +checksum = "ea8b391c9a790b496184c29f7f93b9ed5b16abb306c05415b68bcc16e4d06432" [[package]] name = "yew" @@ -2320,5 +2312,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.89", + "syn 2.0.90", ] diff --git a/aris/src/expr.rs b/aris/src/expr.rs index 21f57a99..20bc162f 100644 --- a/aris/src/expr.rs +++ b/aris/src/expr.rs @@ -441,6 +441,10 @@ impl Expr { pub fn apply(func: Expr, args: &[Expr]) -> Expr { Expr::Apply { func: Box::new(func), args: args.to_vec() } } + /// Helper for constructing `Not` nodes + pub fn not_place_holder() -> Expr { + Expr::Not { operand: Box::new(Expr::var("_")) } + } /// Construct an error message placeholder for an implication pub fn impl_place_holder() -> Expr { Expr::implies(Expr::var("_"), Expr::var("_")) @@ -454,11 +458,11 @@ impl Expr { Expr::Assoc { op, exprs: exprs.to_vec() } } /// Construct an error message placeholder for an associative operator - pub fn assocplaceholder(op: Op) -> Expr { + pub fn assoc_place_holder(op: Op) -> Expr { Expr::assoc(op, &[Expr::var("_"), Expr::var("_"), Expr::var("...")]) } /// Construct an error message placeholder for a quantifier - pub fn quant_placeholder(kind: QuantKind) -> Expr { + pub fn quant_place_holder(kind: QuantKind) -> Expr { Expr::Quant { kind, name: "_".to_owned(), body: Box::new(Expr::var("_")) } } /// Helper for constructing `Forall` nodes @@ -1139,26 +1143,29 @@ impl Expr { } /// Collects unique expressions and identifies complements globally + /// Removes complements from the unique expressions set when found fn collect_unique_exprs_complement(expr: &Expr, op: Op, unique_exprs: &mut HashSet) -> bool { match expr { - Expr::Assoc { op: expr_op, exprs } if *expr_op == op => exprs.iter().any(|sub_expr| Expr::collect_unique_exprs_complement(sub_expr, op, unique_exprs)), + Expr::Assoc { op: expr_op, exprs } if *expr_op == op => exprs.iter().fold(false, |found_complement, sub_expr| Expr::collect_unique_exprs_complement(sub_expr, op, unique_exprs) || found_complement), Expr::Not { operand } => { - // Check if the negation of the operand already exists in the set if let Expr::Quant { kind: QuantKind::Forall, .. } = **operand { if operand.is_universal_tautology() { return true; } } if unique_exprs.contains(&**operand) { - true // Complement found + unique_exprs.remove(&**operand); + true } else { unique_exprs.insert(expr.clone()); false } } _ => { - if unique_exprs.contains(&Expr::Not { operand: Box::new(expr.clone()) }) { - true // Complement found + let negated = Expr::Not { operand: Box::new(expr.clone()) }; + if unique_exprs.contains(&negated) { + unique_exprs.remove(&negated); + true } else { unique_exprs.insert(expr.clone()); false @@ -1170,6 +1177,7 @@ impl Expr { /// Reduce an expression over complement, that is: /// A & ~A -> ⊥ /// A | ~A -> ⊤ + /// Removes complements and preserves non-complement terms pub fn normalize_complement(self) -> Expr { match self { Expr::Assoc { op, exprs } if op == Op::And || op == Op::Or => { @@ -1178,13 +1186,19 @@ impl Expr { if has_complement { match op { - Op::And => Expr::Contra, + Op::And => { + let remaining_terms: Vec = unique_exprs.into_iter().collect(); + if remaining_terms.is_empty() { + Expr::Contra + } else { + Expr::Assoc { op, exprs: vec![Expr::Contra].into_iter().chain(remaining_terms).collect() } + } + } Op::Or => Expr::Taut, _ => unreachable!(), } } else { let unique_exprs: Vec = unique_exprs.into_iter().map(|e| e.normalize_complement()).collect(); - if unique_exprs.len() == 1 { unique_exprs.into_iter().next().unwrap() } else { diff --git a/aris/src/proofs/java_shallow_proof.rs b/aris/src/proofs/java_shallow_proof.rs index f2dc2654..5448d30f 100644 --- a/aris/src/proofs/java_shallow_proof.rs +++ b/aris/src/proofs/java_shallow_proof.rs @@ -28,7 +28,7 @@ impl Proof for JavaShallowProof { Some(r.clone()) } fn lookup_step(&self, r: &Self::JustificationReference) -> Option, Self::SubproofReference>> { - Some(Justification(r.clone(), RuleM::Reit, vec![], vec![])) + Some(Justification(r.clone(), RuleM::Reiteration, vec![], vec![])) } fn lookup_subproof(&self, r: &Self::SubproofReference) -> Option { Some(r.clone()) diff --git a/aris/src/proofs/lined_proof.rs b/aris/src/proofs/lined_proof.rs index 5cbcf11a..9a94a186 100644 --- a/aris/src/proofs/lined_proof.rs +++ b/aris/src/proofs/lined_proof.rs @@ -117,13 +117,13 @@ where let line: Option> = self.lines.get(i).cloned(); match line { None => { - let r = if is_premise { Inl(self.proof.add_premise(const_true)) } else { Inr(Inl(self.proof.add_step(Justification(const_true, RuleM::Reit, vec![], vec![])))) }; + let r = if is_premise { Inl(self.proof.add_premise(const_true)) } else { Inr(Inl(self.proof.add_step(Justification(const_true, RuleM::Reiteration, vec![], vec![])))) }; self.lines.push(Line { raw_expr: "".into(), is_premise, reference: r, subreference: None }); } Some(line) => { let r = match (is_premise, line.reference.clone()) { (true, Inl(pr)) => Inl(self.proof.add_premise_relative(const_true, &pr, true)), - (false, Inr(Inl(jr))) => Inr(Inl(self.proof.add_step_relative(Justification(const_true, RuleM::Reit, vec![], vec![]), &Coproduct::inject(jr), true))), + (false, Inr(Inl(jr))) => Inr(Inl(self.proof.add_step_relative(Justification(const_true, RuleM::Reiteration, vec![], vec![]), &Coproduct::inject(jr), true))), (_, Inr(Inr(void))) => match void {}, (b, r) => panic!("LinedProof::add_line, is_premise was {b}, but the line reference was {r:?}"), }; diff --git a/aris/src/proofs/proof_tests.rs b/aris/src/proofs/proof_tests.rs index 959d6f68..8532d448 100644 --- a/aris/src/proofs/proof_tests.rs +++ b/aris/src/proofs/proof_tests.rs @@ -62,14 +62,17 @@ macro_rules! generate_tests { macro_rules! enumerate_subproofless_tests { ($x:ty, $y:ident) => { generate_tests! { $x, $y; - test_andelim, test_contelim, test_orintro, test_reit, test_andintro, + test_andelim, test_contelim, test_orintro, test_reiteration, test_andintro, test_contradictionintro, test_notelim, test_impelim, test_commutation_bool, test_commutation_bicon, test_association_bool, test_association_bicon, - test_demorgan, test_idempotence, test_doublenegation, - test_distribution, test_complement, test_identity, test_annihilation, - test_inverse, test_absorption, test_reduction, test_adjacency, test_resolution, - test_tautcon, test_empty_rule, test_modus_tollens, test_hypothetical_syllogism, - test_disjunctive_syllogism, test_constructive_dilemma, test_halfdemorgan, + test_demorgan, test_idempotence, test_doublenegation, test_distribution, + test_complement, test_identity, test_annihilation, test_inverse, test_absorption, + test_reduction, test_adjacency, test_resolution, test_tautcon, test_empty_rule, + test_modus_tollens, test_hypothetical_syllogism, test_disjunctive_syllogism, + test_constructive_dilemma, test_destructive_dilemma, test_halfdemorgan, + test_strengthen_antecedent, test_weaken_consequent, test_con_intro_negation, + test_con_elim_negation, test_bicon_intro, test_bicon_intro_negation, + test_bicon_elim, test_bicon_elim_negation, test_exclusion, test_excluded_middle, test_weak_induction, test_strong_induction, test_bicon_contraposition, } @@ -112,7 +115,7 @@ where let r4 = prf.add_subproof(); prf.with_mut_subproof(&r4, |sub| { sub.add_premise(p("C")); - sub.add_step(Justification(p("A & B"), RuleM::Reit, vec![i(r3.clone())], vec![])); + sub.add_step(Justification(p("A & B"), RuleM::Reiteration, vec![i(r3.clone())], vec![])); }); let r5 = prf.add_step(Justification(p("C -> (A & B)"), RuleM::ImpIntro, vec![], vec![r4.clone()])); assert_eq!(prf.lookup_premise(&r1), Some(p("A"))); @@ -163,13 +166,13 @@ pub fn test_orintro() -> (P, Vec>, Vec>) { (prf, vec![i(r2)], vec![i(r3), i(r4)]) } -pub fn test_reit() -> (P, Vec>, Vec>) { +pub fn test_reiteration() -> (P, Vec>, Vec>) { use self::coproduct_inject as i; use crate::parser::parse_unwrap as p; let mut prf = P::new(); let r1 = prf.add_premise(p("A")); - let r2 = prf.add_step(Justification(p("A"), RuleM::Reit, vec![i(r1.clone())], vec![])); - let r3 = prf.add_step(Justification(p("B"), RuleM::Reit, vec![i(r1)], vec![])); + let r2 = prf.add_step(Justification(p("A"), RuleM::Reiteration, vec![i(r1.clone())], vec![])); + let r3 = prf.add_step(Justification(p("B"), RuleM::Reiteration, vec![i(r1)], vec![])); (prf, vec![i(r2)], vec![i(r3)]) } @@ -286,7 +289,7 @@ where let r4 = prf .with_mut_subproof(&r5, |sub1| { let _r3 = sub1.add_premise(p("A")); - let r4 = sub1.add_step(Justification(p("B"), RuleM::Reit, vec![i(r2.clone())], vec![])); + let r4 = sub1.add_step(Justification(p("B"), RuleM::Reiteration, vec![i(r2.clone())], vec![])); println!("{sub1:?}"); r4 }) @@ -295,7 +298,7 @@ where let r7 = prf .with_mut_subproof(&r8, |sub2| { let _r6 = sub2.add_premise(p("A")); - let r7 = sub2.add_step(Justification(p("A"), RuleM::Reit, vec![i(r1.clone())], vec![])); + let r7 = sub2.add_step(Justification(p("A"), RuleM::Reiteration, vec![i(r1.clone())], vec![])); println!("{sub2:?}"); r7 }) @@ -329,17 +332,17 @@ pub fn test_orelim() -> (P, Vec>, Vec>) { let r4 = prf.add_subproof(); prf.with_mut_subproof(&r4, |sub1| { let _r2 = sub1.add_premise(p("A")); - let _r3 = sub1.add_step(Justification(p("C"), RuleM::Reit, vec![], vec![])); + let _r3 = sub1.add_step(Justification(p("C"), RuleM::Reiteration, vec![], vec![])); }); let r7 = prf.add_subproof(); prf.with_mut_subproof(&r7, |sub2| { let _r5 = sub2.add_premise(p("B")); - let _r6 = sub2.add_step(Justification(p("C"), RuleM::Reit, vec![], vec![])); + let _r6 = sub2.add_step(Justification(p("C"), RuleM::Reiteration, vec![], vec![])); }); let r10 = prf.add_subproof(); prf.with_mut_subproof(&r10, |sub3| { let _r8 = sub3.add_premise(p("B")); - let _r9 = sub3.add_step(Justification(p("D"), RuleM::Reit, vec![], vec![])); + let _r9 = sub3.add_step(Justification(p("D"), RuleM::Reiteration, vec![], vec![])); }); let r11 = prf.add_step(Justification(p("C"), RuleM::OrElim, vec![i(r1.clone())], vec![r4.clone(), r7.clone()])); let r12 = prf.add_step(Justification(p("D"), RuleM::OrElim, vec![i(r1.clone())], vec![r4.clone(), r7.clone()])); @@ -373,21 +376,21 @@ where let r14 = prf.add_subproof(); prf.with_mut_subproof(&r14, |sub2| { sub2.add_premise(p("A")); - sub2.add_step(Justification(p("B"), RuleM::Reit, vec![], vec![])); - sub2.add_step(Justification(p("C"), RuleM::Reit, vec![], vec![])); + sub2.add_step(Justification(p("B"), RuleM::Reiteration, vec![], vec![])); + sub2.add_step(Justification(p("C"), RuleM::Reiteration, vec![], vec![])); }); let r15 = prf.add_subproof(); prf.with_mut_subproof(&r15, |sub2| { sub2.add_premise(p("B")); - sub2.add_step(Justification(p("A"), RuleM::Reit, vec![], vec![])); - sub2.add_step(Justification(p("C"), RuleM::Reit, vec![], vec![])); + sub2.add_step(Justification(p("A"), RuleM::Reiteration, vec![], vec![])); + sub2.add_step(Justification(p("C"), RuleM::Reiteration, vec![], vec![])); }); let r16 = prf.add_step(Justification(p("A <-> B"), RuleM::BiconditionalIntro, vec![], vec![r14.clone(), r15.clone()])); let r17 = prf.add_step(Justification(p("A <-> C"), RuleM::BiconditionalIntro, vec![], vec![r14.clone(), r15.clone()])); let r18 = prf.add_subproof(); prf.with_mut_subproof(&r18, |sub2| { sub2.add_premise(p("P")); - sub2.add_step(Justification(p("Q"), RuleM::Reit, vec![], vec![])); + sub2.add_step(Justification(p("Q"), RuleM::Reiteration, vec![], vec![])); }); let r19 = prf.add_step(Justification(p("P <-> Q"), RuleM::BiconditionalIntro, vec![i(r3)], vec![r18.clone()])); (prf, vec![i(r7), i(r11), i(r16), i(r19)], vec![i(r8), i(r9), i(r12), i(r13), i(r17)]) @@ -419,21 +422,21 @@ where let r14 = prf.add_subproof(); prf.with_mut_subproof(&r14, |sub2| { sub2.add_premise(p("A")); - sub2.add_step(Justification(p("B"), RuleM::Reit, vec![], vec![])); - sub2.add_step(Justification(p("C"), RuleM::Reit, vec![], vec![])); + sub2.add_step(Justification(p("B"), RuleM::Reiteration, vec![], vec![])); + sub2.add_step(Justification(p("C"), RuleM::Reiteration, vec![], vec![])); }); let r15 = prf.add_subproof(); prf.with_mut_subproof(&r15, |sub2| { sub2.add_premise(p("B")); - sub2.add_step(Justification(p("A"), RuleM::Reit, vec![], vec![])); - sub2.add_step(Justification(p("C"), RuleM::Reit, vec![], vec![])); + sub2.add_step(Justification(p("A"), RuleM::Reiteration, vec![], vec![])); + sub2.add_step(Justification(p("C"), RuleM::Reiteration, vec![], vec![])); }); let r16 = prf.add_step(Justification(p("A === B"), RuleM::EquivalenceIntro, vec![], vec![r14.clone(), r15.clone()])); let r17 = prf.add_step(Justification(p("A === C"), RuleM::EquivalenceIntro, vec![], vec![r14.clone(), r15.clone()])); let r18 = prf.add_subproof(); prf.with_mut_subproof(&r18, |sub2| { sub2.add_premise(p("P")); - sub2.add_step(Justification(p("Q"), RuleM::Reit, vec![], vec![])); + sub2.add_step(Justification(p("Q"), RuleM::Reiteration, vec![], vec![])); }); let r19 = prf.add_step(Justification(p("P === Q"), RuleM::EquivalenceIntro, vec![i(r3)], vec![r18.clone()])); (prf, vec![i(r7), i(r8), i(r9), i(r11), i(r16), i(r19)], vec![i(r12), i(r13), i(r17)]) @@ -494,7 +497,7 @@ where let r10 = prf.add_subproof(); let r11 = prf .with_mut_subproof(&r10, |sub| { - let r11 = sub.add_step(Justification(p("r(c)"), RuleM::Reit, vec![i(r3.clone())], vec![])); + let r11 = sub.add_step(Justification(p("r(c)"), RuleM::Reiteration, vec![i(r3.clone())], vec![])); println!("contained {:?}", sub.contained_justifications(true)); println!("reachable {:?}", sub.transitive_dependencies(i(r11.clone()))); println!("reachable-contained {:?}", sub.transitive_dependencies(i(r11.clone())).difference(&sub.contained_justifications(true)).collect::>()); @@ -509,7 +512,7 @@ where let (r17, r18) = sub1 .with_mut_subproof(&r14, |sub2| { let r15 = sub2.add_subproof(); - let r17 = sub2.with_mut_subproof(&r15, |sub3| sub3.add_step(Justification(p("s(a, b)"), RuleM::Reit, vec![], vec![]))).unwrap(); + let r17 = sub2.with_mut_subproof(&r15, |sub3| sub3.add_step(Justification(p("s(a, b)"), RuleM::Reiteration, vec![], vec![]))).unwrap(); let r18 = sub2.add_step(Justification(p("forall y s(a, y)"), RuleM::ForallIntro, vec![], vec![r15])); (r17, r18) }) @@ -524,7 +527,7 @@ where .with_mut_subproof(&r20, |sub| { let r21 = sub.add_premise(p("a")); - sub.add_step(Justification(p("a"), RuleM::Reit, vec![i(r21)], vec![])) + sub.add_step(Justification(p("a"), RuleM::Reiteration, vec![i(r21)], vec![])) }) .unwrap(); let r23 = prf.add_step(Justification(p("forall x x"), RuleM::ForallIntro, vec![], vec![r20])); @@ -542,7 +545,7 @@ where let mut prf = P::new(); let r1 = prf.add_premise(p("p(a)")); - let r2 = prf.add_step(Justification(p("p(b) & p(b)"), RuleM::Reit, vec![], vec![])); + let r2 = prf.add_step(Justification(p("p(b) & p(b)"), RuleM::Reiteration, vec![], vec![])); let r3 = prf.add_step(Justification(p("exists x p(x)"), RuleM::ExistsIntro, vec![i(r1.clone())], vec![])); let r4 = prf.add_step(Justification(p("exists x p(a)"), RuleM::ExistsIntro, vec![i(r1.clone())], vec![])); let r5 = prf.add_step(Justification(p("exists x p(b)"), RuleM::ExistsIntro, vec![i(r1)], vec![])); @@ -809,6 +812,7 @@ pub fn test_complement() -> (P, Vec>, Vec>) { let r5 = prf.add_premise(p("~(forall A A) | (forall B B)")); let r6 = prf.add_premise(p("~(forall A A) & (forall B B)")); let r19 = prf.add_premise(p("(A -> A) & (B <-> B) & (C <-> ~C) & (~D <-> D)")); + let r32 = prf.add_premise(p("A & ~A & P")); let r7 = prf.add_step(Justification(p("_|_"), RuleM::Complement, vec![i(r1.clone())], vec![])); let r8 = prf.add_step(Justification(p("^|^"), RuleM::Complement, vec![i(r1)], vec![])); @@ -822,6 +826,8 @@ pub fn test_complement() -> (P, Vec>, Vec>) { let r16 = prf.add_step(Justification(p("^|^"), RuleM::Complement, vec![i(r5)], vec![])); let r17 = prf.add_step(Justification(p("_|_"), RuleM::Complement, vec![i(r6.clone())], vec![])); let r18 = prf.add_step(Justification(p("^|^"), RuleM::Complement, vec![i(r6)], vec![])); + let r33 = prf.add_step(Justification(p("_|_ & P"), RuleM::Complement, vec![i(r32.clone())], vec![])); + let r34 = prf.add_step(Justification(p("_|_ & P & X & F"), RuleM::Complement, vec![i(r32)], vec![])); let r20 = prf.add_step(Justification(p("^|^ & ^|^ & _|_ & _|_"), RuleM::ConditionalComplement, vec![i(r19.clone())], vec![])); let r21 = prf.add_step(Justification(p("^|^ & (B <-> B) & (C <-> ~C) & (~D <-> D)"), RuleM::ConditionalComplement, vec![i(r19.clone())], vec![])); @@ -837,7 +843,7 @@ pub fn test_complement() -> (P, Vec>, Vec>) { let r30 = prf.add_step(Justification(p("(A -> A) & (B <-> B) & (C <-> ~C) & _|_"), RuleM::BiconditionalComplement, vec![i(r19.clone())], vec![])); let r31 = prf.add_step(Justification(p("_|_ & _|_ & ^|^ & ^|^"), RuleM::BiconditionalComplement, vec![i(r19)], vec![])); - (prf, vec![i(r7), i(r9), i(r12), i(r14), i(r16), i(r17), i(r21), i(r28), i(r29), i(r30)], vec![i(r8), i(r10), i(r11), i(r13), i(r15), i(r18), i(r20), i(r22), i(r23), i(r24), i(r25), i(r26), i(r27), i(r31)]) + (prf, vec![i(r7), i(r9), i(r12), i(r14), i(r16), i(r17), i(r21), i(r28), i(r29), i(r30), i(r33)], vec![i(r8), i(r10), i(r11), i(r13), i(r15), i(r18), i(r20), i(r22), i(r23), i(r24), i(r25), i(r26), i(r27), i(r31), i(r34)]) } pub fn test_identity() -> (P, Vec>, Vec>) { @@ -1039,15 +1045,16 @@ pub fn test_resolution() -> (P, Vec>, Vec>) { let r1 = prf.add_step(Justification(p("a1 | a2 | b1 | b2"), RuleM::Resolution, vec![i(p1.clone()), i(p2.clone())], vec![])); let r2 = prf.add_step(Justification(p("a1 | a2"), RuleM::Resolution, vec![i(p1.clone()), i(p3.clone())], vec![])); let r3 = prf.add_step(Justification(p("_|_"), RuleM::Resolution, vec![i(p3.clone()), i(p4)], vec![])); - let r4 = prf.add_step(Justification(p("a1 & a2"), RuleM::Resolution, vec![i(p3.clone()), i(p6)], vec![])); + let r4 = prf.add_step(Justification(p("a1 & a2"), RuleM::Resolution, vec![i(p3.clone()), i(p6.clone())], vec![])); let r5 = prf.add_step(Justification(p("a1 | a2 | c | b1 | b2"), RuleM::Resolution, vec![i(p1.clone()), i(p2.clone())], vec![])); - let r6 = prf.add_step(Justification(p("a1 | a2 | b1"), RuleM::Resolution, vec![i(p1), i(p2)], vec![])); + let r6 = prf.add_step(Justification(p("a1 | a2 | b1"), RuleM::Resolution, vec![i(p1.clone()), i(p2.clone())], vec![])); let r7 = prf.add_step(Justification(p("a1 | a2"), RuleM::Resolution, vec![i(p5.clone()), i(p3.clone())], vec![])); - let r8 = prf.add_step(Justification(p("a1 | a2"), RuleM::Resolution, vec![i(p3), i(p5.clone())], vec![])); + let r8 = prf.add_step(Justification(p("a1 | a2"), RuleM::Resolution, vec![i(p3.clone()), i(p5.clone())], vec![])); let r9 = prf.add_step(Justification(p("a1 | a2"), RuleM::Resolution, vec![i(p5.clone()), i(p5)], vec![])); + let r10 = prf.add_step(Justification(p("a1 | a2 | b1 | b2 | z | d | e | f"), RuleM::Resolution, vec![i(p1.clone()), i(p2.clone())], vec![])); - (prf, vec![i(r1), i(r2), i(r3), i(r4)], vec![i(r5), i(r6), i(r7), i(r8), i(r9)]) + (prf, vec![i(r1), i(r2), i(r3), i(r4)], vec![i(r5), i(r6), i(r7), i(r8), i(r9), i(r10)]) } pub fn test_tautcon() -> (P, Vec>, Vec>) { @@ -1103,6 +1110,14 @@ pub fn test_modus_tollens() -> (P, Vec>, Vec>) { let r3 = prf.add_premise(p("P")); let r4 = prf.add_premise(p("~A")); let r5 = prf.add_premise(p("A -> A")); + + let r15 = prf.add_premise(p("P -> ~Q")); + let r16 = prf.add_premise(p("Q")); + let r19 = prf.add_premise(p("~P -> Q")); + let r20 = prf.add_premise(p("~Q")); + let r23 = prf.add_premise(p("~P -> ~Q")); + let r24 = prf.add_premise(p("Q")); + let r6 = prf.add_step(Justification(p("~P"), RuleM::ModusTollens, vec![i(r1.clone()), i(r2.clone())], vec![])); let r7 = prf.add_step(Justification(p("~P"), RuleM::ModusTollens, vec![i(r2.clone()), i(r1.clone())], vec![])); let r8 = prf.add_step(Justification(p("~B"), RuleM::ModusTollens, vec![i(r1.clone()), i(r2.clone())], vec![])); @@ -1112,7 +1127,15 @@ pub fn test_modus_tollens() -> (P, Vec>, Vec>) { let r12 = prf.add_step(Justification(p("Q"), RuleM::ModusTollens, vec![i(r2.clone()), i(r4.clone())], vec![])); let r13 = prf.add_step(Justification(p("~A"), RuleM::ModusTollens, vec![i(r4), i(r5)], vec![])); let r14 = prf.add_step(Justification(p("~P"), RuleM::ModusTollens, vec![i(r2), i(r1)], vec![])); - (prf, vec![i(r6), i(r7), i(r13), i(r14)], vec![i(r8), i(r9), i(r10), i(r11), i(r12)]) + + let r17 = prf.add_step(Justification(p("~P"), RuleM::ModusTollens, vec![i(r15.clone()), i(r16.clone())], vec![])); + let r18 = prf.add_step(Justification(p("~P"), RuleM::ModusTollens, vec![i(r16.clone()), i(r15.clone())], vec![])); + let r21 = prf.add_step(Justification(p("P"), RuleM::ModusTollens, vec![i(r19.clone()), i(r20.clone())], vec![])); + let r22 = prf.add_step(Justification(p("P"), RuleM::ModusTollens, vec![i(r20.clone()), i(r19.clone())], vec![])); + let r25 = prf.add_step(Justification(p("P"), RuleM::ModusTollens, vec![i(r23.clone()), i(r24.clone())], vec![])); + let r26 = prf.add_step(Justification(p("P"), RuleM::ModusTollens, vec![i(r24.clone()), i(r23.clone())], vec![])); + + (prf, vec![i(r6), i(r7), i(r13), i(r14), i(r17), i(r18), i(r21), i(r22), i(r25), i(r26)], vec![i(r8), i(r9), i(r10), i(r11), i(r12)]) } pub fn test_hypothetical_syllogism() -> (P, Vec>, Vec>) { @@ -1175,6 +1198,34 @@ pub fn test_constructive_dilemma() -> (P, Vec>, Vec> (prf, vec![i(r6), i(r7)], vec![i(r8), i(r9), i(r10), i(r11), i(r12), i(r13)]) } +pub fn test_destructive_dilemma() -> (P, Vec>, Vec>) { + use self::coproduct_inject as i; + use crate::parser::parse_unwrap as p; + let mut prf = P::new(); + let r1 = prf.add_premise(p("~R | ~S")); + let r2 = prf.add_premise(p("P -> R")); + let r3 = prf.add_premise(p("Q -> S")); + + let r4 = prf.add_step(Justification(p("~P | ~Q"), RuleM::DestructiveDilemma, vec![i(r1.clone()), i(r2.clone()), i(r3.clone())], vec![])); + let r5 = prf.add_step(Justification(p("~Q | ~P"), RuleM::DestructiveDilemma, vec![i(r1.clone()), i(r2.clone()), i(r3.clone())], vec![])); + let r6 = prf.add_step(Justification(p("~P | ~Q"), RuleM::DestructiveDilemma, vec![i(r1.clone()), i(r3.clone()), i(r2.clone())], vec![])); + let r7 = prf.add_step(Justification(p("~Q | ~P"), RuleM::DestructiveDilemma, vec![i(r1.clone()), i(r3.clone()), i(r2.clone())], vec![])); + let r8 = prf.add_step(Justification(p("~P | ~Q"), RuleM::DestructiveDilemma, vec![i(r2.clone()), i(r1.clone()), i(r3.clone())], vec![])); + let r9 = prf.add_step(Justification(p("~Q | ~P"), RuleM::DestructiveDilemma, vec![i(r2.clone()), i(r1.clone()), i(r3.clone())], vec![])); + let r10 = prf.add_step(Justification(p("~P | ~Q"), RuleM::DestructiveDilemma, vec![i(r2.clone()), i(r3.clone()), i(r1.clone())], vec![])); + let r11 = prf.add_step(Justification(p("~Q | ~P"), RuleM::DestructiveDilemma, vec![i(r2.clone()), i(r3.clone()), i(r1.clone())], vec![])); + let r12 = prf.add_step(Justification(p("~P | ~Q"), RuleM::DestructiveDilemma, vec![i(r3.clone()), i(r1.clone()), i(r2.clone())], vec![])); + let r13 = prf.add_step(Justification(p("~Q | ~P"), RuleM::DestructiveDilemma, vec![i(r3.clone()), i(r1.clone()), i(r2.clone())], vec![])); + let r14 = prf.add_step(Justification(p("~P | ~Q"), RuleM::DestructiveDilemma, vec![i(r3.clone()), i(r2.clone()), i(r1.clone())], vec![])); + let r15 = prf.add_step(Justification(p("~Q | ~P"), RuleM::DestructiveDilemma, vec![i(r3.clone()), i(r2.clone()), i(r1.clone())], vec![])); + + let r16 = prf.add_step(Justification(p("P | ~Q"), RuleM::DestructiveDilemma, vec![i(r1.clone()), i(r2.clone()), i(r3.clone())], vec![])); + let r17 = prf.add_step(Justification(p("Q | ~P"), RuleM::DestructiveDilemma, vec![i(r1.clone()), i(r2.clone()), i(r3.clone())], vec![])); + let r18 = prf.add_step(Justification(p("~P"), RuleM::DestructiveDilemma, vec![i(r1.clone()), i(r2.clone()), i(r3.clone())], vec![])); + + (prf, vec![i(r4), i(r5), i(r6), i(r7), i(r8), i(r9), i(r10), i(r11), i(r12), i(r13), i(r14), i(r15)], vec![i(r16), i(r17), i(r18)]) +} + pub fn test_halfdemorgan() -> (P, Vec>, Vec>) { use self::coproduct_inject as i; use crate::parser::parse_unwrap as p; @@ -1194,6 +1245,180 @@ pub fn test_halfdemorgan() -> (P, Vec>, Vec>) { (prf, vec![i(r4), i(r5), i(r6), i(r8), i(r9), i(r11)], vec![i(r7), i(r10)]) } +pub fn test_strengthen_antecedent() -> (P, Vec>, Vec>) { + use self::coproduct_inject as i; + use crate::parser::parse_unwrap as p; + let mut prf = P::new(); + let r1 = prf.add_premise(p("P -> R")); + let r2 = prf.add_premise(p("(P | Q) -> R")); + + let r3 = prf.add_step(Justification(p("(P & Q) -> R"), RuleM::StrengthenAntecedent, vec![i(r1.clone())], vec![])); + let r4 = prf.add_step(Justification(p("(Q & P) -> R"), RuleM::StrengthenAntecedent, vec![i(r1.clone())], vec![])); + let r5 = prf.add_step(Justification(p("P -> R"), RuleM::StrengthenAntecedent, vec![i(r2.clone())], vec![])); + let r6 = prf.add_step(Justification(p("Q -> R"), RuleM::StrengthenAntecedent, vec![i(r2.clone())], vec![])); + + let r7 = prf.add_step(Justification(p("Q -> R"), RuleM::StrengthenAntecedent, vec![i(r1.clone())], vec![])); + let r8 = prf.add_step(Justification(p("(P | Q | S) -> R"), RuleM::StrengthenAntecedent, vec![i(r2.clone())], vec![])); + let r9 = prf.add_step(Justification(p("S -> R"), RuleM::StrengthenAntecedent, vec![i(r2.clone())], vec![])); + + (prf, vec![i(r3), i(r4), i(r5), i(r6)], vec![i(r7), i(r8), i(r9)]) +} + +pub fn test_weaken_consequent() -> (P, Vec>, Vec>) { + use self::coproduct_inject as i; + use crate::parser::parse_unwrap as p; + let mut prf = P::new(); + let r1 = prf.add_premise(p("P -> (Q & R)")); + let r2 = prf.add_premise(p("P -> Q")); + + let r3 = prf.add_step(Justification(p("P -> Q"), RuleM::WeakenConsequent, vec![i(r1.clone())], vec![])); + let r4 = prf.add_step(Justification(p("P -> R"), RuleM::WeakenConsequent, vec![i(r1.clone())], vec![])); + let r5 = prf.add_step(Justification(p("P -> (Q | R)"), RuleM::WeakenConsequent, vec![i(r2.clone())], vec![])); + let r6 = prf.add_step(Justification(p("P -> (R | Q)"), RuleM::WeakenConsequent, vec![i(r2.clone())], vec![])); + + let r7 = prf.add_step(Justification(p("R -> P"), RuleM::WeakenConsequent, vec![i(r1.clone())], vec![])); + let r8 = prf.add_step(Justification(p("P -> (Q & R)"), RuleM::WeakenConsequent, vec![i(r2.clone())], vec![])); + let r9 = prf.add_step(Justification(p("P -> (Z | R)"), RuleM::WeakenConsequent, vec![i(r2.clone())], vec![])); + + (prf, vec![i(r3), i(r4), i(r5), i(r6)], vec![i(r7), i(r8), i(r9)]) +} + +pub fn test_con_intro_negation() -> (P, Vec>, Vec>) { + use self::coproduct_inject as i; + use crate::parser::parse_unwrap as p; + let mut prf = P::new(); + let r1 = prf.add_premise(p("~P")); + let r2 = prf.add_premise(p("Q")); + + let r3 = prf.add_step(Justification(p("P -> Q"), RuleM::ConIntroNegation, vec![i(r1.clone())], vec![])); + let r4 = prf.add_step(Justification(p("P -> Q"), RuleM::ConIntroNegation, vec![i(r2.clone())], vec![])); + + let r5 = prf.add_step(Justification(p("~P -> Q"), RuleM::ConIntroNegation, vec![i(r1.clone())], vec![])); + let r6 = prf.add_step(Justification(p("P -> ~Q"), RuleM::ConIntroNegation, vec![i(r1.clone())], vec![])); + let r7 = prf.add_step(Justification(p("~P -> Q"), RuleM::ConIntroNegation, vec![i(r2.clone())], vec![])); + let r8 = prf.add_step(Justification(p("P -> ~Q"), RuleM::ConIntroNegation, vec![i(r2.clone())], vec![])); + + (prf, vec![i(r3), i(r4)], vec![i(r5), i(r6), i(r7), i(r8)]) +} +pub fn test_con_elim_negation() -> (P, Vec>, Vec>) { + use self::coproduct_inject as i; + use crate::parser::parse_unwrap as p; + let mut prf = P::new(); + let r1 = prf.add_premise(p("~(P -> Q)")); + + let r2 = prf.add_premise(p("P -> Q")); + + let r3 = prf.add_step(Justification(p("P"), RuleM::ConElimNegation, vec![i(r1.clone())], vec![])); + let r4 = prf.add_step(Justification(p("~Q"), RuleM::ConElimNegation, vec![i(r1.clone())], vec![])); + + let r5 = prf.add_step(Justification(p("~P"), RuleM::ConElimNegation, vec![i(r1.clone())], vec![])); + let r6 = prf.add_step(Justification(p("Q"), RuleM::ConElimNegation, vec![i(r1.clone())], vec![])); + + let r7 = prf.add_step(Justification(p("P"), RuleM::ConElimNegation, vec![i(r2.clone())], vec![])); + let r8 = prf.add_step(Justification(p("~Q"), RuleM::ConElimNegation, vec![i(r2.clone())], vec![])); + + (prf, vec![i(r3), i(r4)], vec![i(r5), i(r6), i(r7), i(r8)]) +} +pub fn test_bicon_intro() -> (P, Vec>, Vec>) { + use self::coproduct_inject as i; + use crate::parser::parse_unwrap as p; + let mut prf = P::new(); + let r1 = prf.add_premise(p("P")); + let r2 = prf.add_premise(p("Q")); + + let r3 = prf.add_premise(p("~P")); + let r4 = prf.add_premise(p("~Q")); + + let r5 = prf.add_step(Justification(p("P <-> Q"), RuleM::BiconIntro, vec![i(r1.clone()), i(r2.clone())], vec![])); + let r6 = prf.add_step(Justification(p("P <-> Q"), RuleM::BiconIntro, vec![i(r3.clone()), i(r4.clone())], vec![])); + let r7 = prf.add_step(Justification(p("~P <-> ~Q"), RuleM::BiconIntro, vec![i(r3.clone()), i(r4.clone())], vec![])); + + let r8 = prf.add_step(Justification(p("P <-> ~Q"), RuleM::BiconIntro, vec![i(r1.clone()), i(r2.clone())], vec![])); + let r9 = prf.add_step(Justification(p("~P <-> Q"), RuleM::BiconIntro, vec![i(r1.clone()), i(r2.clone())], vec![])); + let r10 = prf.add_step(Justification(p("P <-> ~Q"), RuleM::BiconIntro, vec![i(r3.clone()), i(r4.clone())], vec![])); + let r11 = prf.add_step(Justification(p("~P <-> Q"), RuleM::BiconIntro, vec![i(r3.clone()), i(r4.clone())], vec![])); + + (prf, vec![i(r5), i(r6), i(r7)], vec![i(r8), i(r9), i(r10), i(r11)]) +} +pub fn test_bicon_intro_negation() -> (P, Vec>, Vec>) { + use self::coproduct_inject as i; + use crate::parser::parse_unwrap as p; + let mut prf = P::new(); + let r1 = prf.add_premise(p("~P")); + let r2 = prf.add_premise(p("Q")); + + let r3 = prf.add_premise(p("P")); + let r4 = prf.add_premise(p("~Q")); + + let r5 = prf.add_step(Justification(p("~(P <-> Q)"), RuleM::BiconIntroNegation, vec![i(r1.clone()), i(r2.clone())], vec![])); + let r6 = prf.add_step(Justification(p("~(P <-> Q)"), RuleM::BiconIntroNegation, vec![i(r3.clone()), i(r4.clone())], vec![])); + + let r7 = prf.add_step(Justification(p("P <-> Q"), RuleM::BiconIntroNegation, vec![i(r1.clone()), i(r2.clone())], vec![])); + let r8 = prf.add_step(Justification(p("P <-> Q"), RuleM::BiconIntroNegation, vec![i(r3.clone()), i(r4.clone())], vec![])); + let r9 = prf.add_step(Justification(p("~(P <-> Q)"), RuleM::BiconIntroNegation, vec![i(r1.clone()), i(r4.clone())], vec![])); + let r10 = prf.add_step(Justification(p("~(P <-> Q)"), RuleM::BiconIntroNegation, vec![i(r2.clone()), i(r3.clone())], vec![])); + + (prf, vec![i(r5), i(r6)], vec![i(r7), i(r8), i(r9), i(r10)]) +} +pub fn test_bicon_elim() -> (P, Vec>, Vec>) { + use self::coproduct_inject as i; + use crate::parser::parse_unwrap as p; + let mut prf = P::new(); + let r1 = prf.add_premise(p("P <-> Q")); + let r2 = prf.add_premise(p("~P")); + let r3 = prf.add_premise(p("~Q")); + + let r4 = prf.add_step(Justification(p("~Q"), RuleM::BiconElim, vec![i(r1.clone()), i(r2.clone())], vec![])); + let r5 = prf.add_step(Justification(p("~P"), RuleM::BiconElim, vec![i(r1.clone()), i(r3.clone())], vec![])); + + let r6 = prf.add_step(Justification(p("Q"), RuleM::BiconElim, vec![i(r1.clone()), i(r2.clone())], vec![])); + let r7 = prf.add_step(Justification(p("P"), RuleM::BiconElim, vec![i(r1.clone()), i(r3.clone())], vec![])); + let r8 = prf.add_step(Justification(p("~Q"), RuleM::BiconElim, vec![i(r1.clone()), i(r3.clone())], vec![])); + let r9 = prf.add_step(Justification(p("~P"), RuleM::BiconElim, vec![i(r1.clone()), i(r2.clone())], vec![])); + + (prf, vec![i(r4), i(r5)], vec![i(r6), i(r7), i(r8), i(r9)]) +} +pub fn test_bicon_elim_negation() -> (P, Vec>, Vec>) { + use self::coproduct_inject as i; + use crate::parser::parse_unwrap as p; + let mut prf = P::new(); + let r1 = prf.add_premise(p("~(P <-> Q)")); + let r2 = prf.add_premise(p("P")); + let r3 = prf.add_premise(p("Q")); + + let r4 = prf.add_step(Justification(p("~Q"), RuleM::BiconElimNegation, vec![i(r1.clone()), i(r2.clone())], vec![])); + let r5 = prf.add_step(Justification(p("~P"), RuleM::BiconElimNegation, vec![i(r1.clone()), i(r3.clone())], vec![])); + + let r6 = prf.add_step(Justification(p("Q"), RuleM::BiconElimNegation, vec![i(r1.clone()), i(r2.clone())], vec![])); + let r7 = prf.add_step(Justification(p("P"), RuleM::BiconElimNegation, vec![i(r1.clone()), i(r3.clone())], vec![])); + let r8 = prf.add_step(Justification(p("~Q"), RuleM::BiconElimNegation, vec![i(r1.clone()), i(r3.clone())], vec![])); + let r9 = prf.add_step(Justification(p("~P"), RuleM::BiconElimNegation, vec![i(r1.clone()), i(r2.clone())], vec![])); + + (prf, vec![i(r4), i(r5)], vec![i(r6), i(r7), i(r8), i(r9)]) +} + +pub fn test_exclusion() -> (P, Vec>, Vec>) { + use self::coproduct_inject as i; + use crate::parser::parse_unwrap as p; + let mut prf = P::new(); + let r1 = prf.add_premise(p("~(P & Q)")); + let r2 = prf.add_premise(p("P")); + let r3 = prf.add_premise(p("Q")); + let r4 = prf.add_premise(p("~(P & ~Q)")); + let r5 = prf.add_premise(p("~(~P & Q)")); + + let r6 = prf.add_step(Justification(p("~Q"), RuleM::Exclusion, vec![i(r1.clone()), i(r2.clone())], vec![])); + let r7 = prf.add_step(Justification(p("~Q"), RuleM::Exclusion, vec![i(r2.clone()), i(r1.clone())], vec![])); + let r8 = prf.add_step(Justification(p("~P"), RuleM::Exclusion, vec![i(r1.clone()), i(r3.clone())], vec![])); + let r9 = prf.add_step(Justification(p("~P"), RuleM::Exclusion, vec![i(r3.clone()), i(r1.clone())], vec![])); + let r10 = prf.add_step(Justification(p("Q"), RuleM::Exclusion, vec![i(r4.clone()), i(r2.clone())], vec![])); + let r11 = prf.add_step(Justification(p("Q"), RuleM::Exclusion, vec![i(r2.clone()), i(r4.clone())], vec![])); + let r12 = prf.add_step(Justification(p("P"), RuleM::Exclusion, vec![i(r5.clone()), i(r3.clone())], vec![])); + let r13 = prf.add_step(Justification(p("P"), RuleM::Exclusion, vec![i(r3.clone()), i(r5.clone())], vec![])); + + (prf, vec![i(r6), i(r7), i(r8), i(r9), i(r10), i(r11), i(r12), i(r13)], vec![]) +} + pub fn test_excluded_middle() -> (P, Vec>, Vec>) { use self::coproduct_inject as i; use crate::parser::parse_unwrap as p; diff --git a/aris/src/proofs/xml_interop.rs b/aris/src/proofs/xml_interop.rs index 069137c3..692a970d 100644 --- a/aris/src/proofs/xml_interop.rs +++ b/aris/src/proofs/xml_interop.rs @@ -124,8 +124,8 @@ pub fn proof_from_xml(r: R) -> Result<(P, ProofMetaData), Str on_current_proof! { proof, { let p = proof.add_subproof(); subproofs.insert(seen_premises[0].clone(), p.clone()); lines_to_subs.insert(last_linenum.clone(), p) } } } rulename => { - let rule = RuleM::from_serialized_name(rulename).unwrap_or(RuleM::Reit); // TODO: explicit RuleM::NoSelectionMade? - //println!("{:?}", rule); + let rule = RuleM::from_serialized_name(rulename).unwrap_or(RuleM::Reiteration); // TODO: explicit RuleM::NoSelectionMade? + //println!("{:?}", rule); let deps = seen_premises.iter().filter_map(|x| line_refs.get(x)).cloned().collect::>(); let sdeps = seen_premises.iter().filter_map(|x| lines_to_subs.get(x)).cloned().collect::>(); //println!("{:?} {:?}", line_refs, subproofs); @@ -343,7 +343,7 @@ mod tests { let sub_lines = sub.lines(); let Justification(e1, r1, d1, s1) = prf.lookup_pj(&Coproduct::inject(*sub_lines[0].get::<

::JustificationReference, _>().unwrap())).unwrap().get::, _>().unwrap().clone(); assert_eq!(e1, Expr::var("A")); - assert_eq!(r1, RuleM::Reit); + assert_eq!(r1, RuleM::Reiteration); assert_eq!(d1.len(), 1); assert_eq!(s1.len(), 0); let Justification(e2, r2, d2, s2) = prf.lookup_pj(&Coproduct::inject(*lines[1].get::<

::JustificationReference, _>().unwrap())).unwrap().get::, _>().unwrap().clone(); diff --git a/aris/src/rules.rs b/aris/src/rules.rs index 89a618d2..44c6734b 100644 --- a/aris/src/rules.rs +++ b/aris/src/rules.rs @@ -74,7 +74,6 @@ use frunk_core::coproduct::Coproduct::Inr; use frunk_core::Coprod; use itertools::Itertools; use maplit::btreeset; -use maplit::hashset; use petgraph::algo::tarjan_scc; use petgraph::graphmap::DiGraphMap; use strum_macros::*; @@ -82,7 +81,6 @@ use strum_macros::*; #[allow(missing_docs)] #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub enum PrepositionalInference { - Reit, AndIntro, AndElim, OrIntro, @@ -108,6 +106,43 @@ pub enum PredicateInference { ExistsElim, } +#[allow(missing_docs)] +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum BooleanInference { + DisjunctiveSyllogism, + Exclusion, + ExcludedMiddle, + HalfDeMorgan, +} + +#[allow(missing_docs)] +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum ConditionalInference { + ModusTollens, + HypotheticalSyllogism, + ConstructiveDilemma, + DestructiveDilemma, + StrengthenAntecedent, + WeakenConsequent, + ConIntroNegation, + ConElimNegation, +} + +#[allow(missing_docs)] +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum BiconditionalInference { + BiconIntro, + BiconIntroNegation, + BiconElim, + BiconElimNegation, +} + +#[allow(missing_docs)] +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum QuantifierInference { + QuantInference, +} + #[allow(missing_docs)] #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub enum BooleanEquivalence { @@ -156,25 +191,6 @@ pub enum BiconditionalEquivalence { KnightsAndKnaves, } -#[allow(missing_docs)] -#[derive(Clone, Copy, Debug, PartialEq, Eq)] -pub enum RedundantPrepositionalInference { - ModusTollens, - HypotheticalSyllogism, - DisjunctiveSyllogism, - ExcludedMiddle, - ConstructiveDilemma, - HalfDeMorgan, - QuantifierInference, -} - -#[allow(missing_docs)] -#[derive(Clone, Copy, Debug, PartialEq, Eq)] -pub enum AutomationRelatedRules { - Resolution, - TruthFunctionalConsequence, -} - #[allow(missing_docs)] #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub enum QuantifierEquivalence { @@ -187,6 +203,14 @@ pub enum QuantifierEquivalence { PrenexLaws, } +#[allow(missing_docs)] +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Special { + Reiteration, + Resolution, + TruthFunctionalConsequence, +} + #[allow(missing_docs)] #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub enum Induction { @@ -211,7 +235,7 @@ pub struct EmptyRule; #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub struct SharedChecks(T); -pub type Rule = SharedChecks; +pub type Rule = SharedChecks; /// Conveniences for constructing rules of the appropriate type, primarily for testing. /// The non-standard naming conventions here are because a module is being used to pretend to be an enum. @@ -259,7 +283,6 @@ pub mod RuleM { // If the parens are omitted, $value:tt only captures SharedChecks, without the (...) // I haven't yet found a way to use macro_rules! to convert between expr and pat. declare_rules! { - [Reit, "REITERATION", (SharedChecks(Inl(PrepositionalInference::Reit)))], [AndIntro, "CONJUNCTION", (SharedChecks(Inl(PrepositionalInference::AndIntro)))], [AndElim, "SIMPLIFICATION", (SharedChecks(Inl(PrepositionalInference::AndElim)))], [OrIntro, "ADDITION", (SharedChecks(Inl(PrepositionalInference::OrIntro)))], @@ -280,65 +303,79 @@ pub mod RuleM { [ExistsIntro, "EXISTENTIAL_GENERALIZATION", (SharedChecks(Inr(Inl(PredicateInference::ExistsIntro))))], [ExistsElim, "EXISTENTIAL_INSTANTIATION", (SharedChecks(Inr(Inl(PredicateInference::ExistsElim))))], - [Association, "ASSOCIATION", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::Association)))))], - [Commutation, "COMMUTATION", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::Commutation)))))], - [Idempotence, "IDEMPOTENCE", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::Idempotence)))))], - [DeMorgan, "DE_MORGAN", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::DeMorgan)))))], - [Distribution, "DISTRIBUTION", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::Distribution)))))], - [DoubleNegation, "DOUBLENEGATION_EQUIV", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::DoubleNegation)))))], - [Complement, "COMPLEMENT", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::Complement)))))], - [Identity, "IDENTITY", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::Identity)))))], - [Annihilation, "ANNIHILATION", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::Annihilation)))))], - [Inverse, "INVERSE", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::Inverse)))))], - [Absorption, "ABSORPTION", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::Absorption)))))], - [Reduction, "REDUCTION", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::Reduction)))))], - [Adjacency, "ADJACENCY", (SharedChecks(Inr(Inr(Inl(BooleanEquivalence::Adjacency)))))], - - [Implication, "IMPLICATION", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalEquivalence::Implication))))))], - [Contraposition, "CONTRAPOSITION", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalEquivalence::Contraposition))))))], - [Exportation, "Exportation", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalEquivalence::Exportation))))))], - [ConditionalDistribution, "CONDITIONAL_DISTRIBUTION", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalDistribution))))))], - [ConditionalAbsorption, "CONDITIONAL_ABSORPTION", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalAbsorption))))))], - [ConditionalReduction, "CONDITIONAL_REDUCTION", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalReduction))))))], - [ConditionalIdempotence, "CONDITIONAL_IDEMPOTENCE", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalIdempotence))))))], - [ConditionalComplement, "CONDITIONAL_COMPLEMENT", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalComplement))))))], - [ConditionalIdentity, "CONDITIONAL_IDENTITY", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalIdentity))))))], - [ConditionalAnnihilation, "CONDITIONAL_ANNIHILATION", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalAnnihilation))))))], - - [BiEquivalence, "BICONDITIONAL_EQUIVALENCE", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiEquivalence)))))))], - [BiconditionalContraposition, "BICONDITIONAL_CONTRAPOSITION", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalContraposition)))))))], - [BiconditionalCommutation, "BICONDITIONAL_COMMUTATION", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalCommutation)))))))], - [BiconditionalAssociation, "BICONDITIONAL_ASSOCIATION", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalAssociation)))))))], - [BiconditionalReduction, "BICONDITIONAL_REDUCTION", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalReduction)))))))], - [BiconditionalComplement, "BICONDITIONAL_COMPLEMENT", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalComplement)))))))], - [BiconditionalIdentity, "BICONDITIONAL_IDENTITY", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalIdentity)))))))], - [BiconditionalNegation, "BICONDITIONAL_NEGATION", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalNegation)))))))], - [BiconditionalSubstitution, "BICONDITIONAL_SUBSTITUTION", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalSubstitution)))))))], - [KnightsAndKnaves, "KNIGHTS_AND_KNAVES", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::KnightsAndKnaves)))))))], - - [ModusTollens, "MODUS_TOLLENS", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::ModusTollens))))))))], - [HypotheticalSyllogism, "HYPOTHETICAL_SYLLOGISM", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::HypotheticalSyllogism))))))))], - [DisjunctiveSyllogism, "DISJUNCTIVE_SYLLOGISM", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::DisjunctiveSyllogism))))))))], - [ExcludedMiddle, "EXCLUDED_MIDDLE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::ExcludedMiddle))))))))], - [ConstructiveDilemma, "CONSTRUCTIVE_DILEMMA", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::ConstructiveDilemma))))))))], - [HalfDeMorgan, "HALF_DE_MORGAN", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::HalfDeMorgan))))))))], - [QuantifierInference, "QUANTIFIER_INFERENCE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(RedundantPrepositionalInference::QuantifierInference))))))))], - - [Resolution, "RESOLUTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(AutomationRelatedRules::Resolution)))))))))], - [TruthFunctionalConsequence, "TRUTHFUNCTIONAL_CONSEQUENCE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(AutomationRelatedRules::TruthFunctionalConsequence)))))))))], - - [QuantifierNegation, "QUANTIFIER_NEGATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::QuantifierNegation))))))))))], - [NullQuantification, "NULL_QUANTIFICATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::NullQuantification))))))))))], - [ReplacingBoundVars, "REPLACING_BOUND_VARS", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::ReplacingBoundVars))))))))))], - [SwappingQuantifiers, "SWAPPING_QUANTIFIERS", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::SwappingQuantifiers))))))))))], - [AristoteleanSquare, "ARISTOTELEAN_SQUARE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::AristoteleanSquare))))))))))], - [QuantifierDistribution, "QUANTIFIER_DISTRIBUTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::QuantifierDistribution))))))))))], - [PrenexLaws, "PRENEX_LAWS", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::PrenexLaws))))))))))], - - [WeakInduction, "WEAK_INDUCTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(Induction::Weak)))))))))))], - [StrongInduction, "STRONG_INDUCTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(Induction::Strong)))))))))))], - - [EmptyRule, "EMPTY_RULE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(super::EmptyRule))))))))))))] + [DisjunctiveSyllogism, "DISJUNCTIVE_SYLLOGISM", (SharedChecks(Inr(Inr(Inl(BooleanInference::DisjunctiveSyllogism)))))], + [Exclusion, "EXCLUSION", (SharedChecks(Inr(Inr(Inl(BooleanInference::Exclusion)))))], + [ExcludedMiddle, "EXCLUDED_MIDDLE", (SharedChecks(Inr(Inr(Inl(BooleanInference::ExcludedMiddle)))))], + [HalfDeMorgan, "HALF_DE_MORGAN", (SharedChecks(Inr(Inr(Inl(BooleanInference::HalfDeMorgan)))))], + + [ModusTollens, "MODUS_TOLLENS", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalInference::ModusTollens))))))], + [HypotheticalSyllogism, "HYPOTHETICAL_SYLLOGISM", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalInference::HypotheticalSyllogism))))))], + [ConstructiveDilemma, "CONSTRUCTIVE_DILEMMA", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalInference::ConstructiveDilemma))))))], + [DestructiveDilemma, "DESTRUCTIVE_DILEMMA", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalInference::DestructiveDilemma))))))], + [StrengthenAntecedent, "STRENGTHEN_ANTECEDENT", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalInference::StrengthenAntecedent))))))], + [WeakenConsequent, "WEAKEN_CONSEQUENT", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalInference::WeakenConsequent))))))], + [ConIntroNegation, "CON_INTRO_NEGATION", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalInference::ConIntroNegation))))))], + [ConElimNegation, "CON_ELIM_NEGATION", (SharedChecks(Inr(Inr(Inr(Inl(ConditionalInference::ConElimNegation))))))], + + [BiconIntro, "BICON_INTRO", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalInference::BiconIntro)))))))], + [BiconIntroNegation, "BICON_INTRO_NEGATION", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalInference::BiconIntroNegation)))))))], + [BiconElim, "BICON_ELIM", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalInference::BiconElim)))))))], + [BiconElimNegation, "BICON_ELIM_NEGATION", (SharedChecks(Inr(Inr(Inr(Inr(Inl(BiconditionalInference::BiconElimNegation)))))))], + + [QuantifierInference, "QUANTIFIER_INFERENCE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierInference::QuantInference))))))))], + + [Association, "ASSOCIATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::Association)))))))))], + [Commutation, "COMMUTATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::Commutation)))))))))], + [Idempotence, "IDEMPOTENCE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::Idempotence)))))))))], + [DeMorgan, "DE_MORGAN", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::DeMorgan)))))))))], + [Distribution, "DISTRIBUTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::Distribution)))))))))], + [DoubleNegation, "DOUBLENEGATION_EQUIV", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::DoubleNegation)))))))))], + [Complement, "COMPLEMENT", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::Complement)))))))))], + [Identity, "IDENTITY", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::Identity)))))))))], + [Annihilation, "ANNIHILATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::Annihilation)))))))))], + [Inverse, "INVERSE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::Inverse)))))))))], + [Absorption, "ABSORPTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::Absorption)))))))))], + [Reduction, "REDUCTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::Reduction)))))))))], + [Adjacency, "ADJACENCY", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BooleanEquivalence::Adjacency)))))))))], + + [Implication, "IMPLICATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(ConditionalEquivalence::Implication))))))))))], + [Contraposition, "CONTRAPOSITION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(ConditionalEquivalence::Contraposition))))))))))], + [Exportation, "Exportation", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(ConditionalEquivalence::Exportation))))))))))], + [ConditionalDistribution, "CONDITIONAL_DISTRIBUTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalDistribution))))))))))], + [ConditionalAbsorption, "CONDITIONAL_ABSORPTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalAbsorption))))))))))], + [ConditionalReduction, "CONDITIONAL_REDUCTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalReduction))))))))))], + [ConditionalIdempotence, "CONDITIONAL_IDEMPOTENCE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalIdempotence))))))))))], + [ConditionalComplement, "CONDITIONAL_COMPLEMENT", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalComplement))))))))))], + [ConditionalIdentity, "CONDITIONAL_IDENTITY", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalIdentity))))))))))], + [ConditionalAnnihilation, "CONDITIONAL_ANNIHILATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(ConditionalEquivalence::ConditionalAnnihilation))))))))))], + + [BiEquivalence, "BICONDITIONAL_EQUIVALENCE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiEquivalence)))))))))))], + [BiconditionalContraposition, "BICONDITIONAL_CONTRAPOSITION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalContraposition)))))))))))], + [BiconditionalCommutation, "BICONDITIONAL_COMMUTATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalCommutation)))))))))))], + [BiconditionalAssociation, "BICONDITIONAL_ASSOCIATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalAssociation)))))))))))], + [BiconditionalReduction, "BICONDITIONAL_REDUCTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalReduction)))))))))))], + [BiconditionalComplement, "BICONDITIONAL_COMPLEMENT", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalComplement)))))))))))], + [BiconditionalIdentity, "BICONDITIONAL_IDENTITY", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalIdentity)))))))))))], + [BiconditionalNegation, "BICONDITIONAL_NEGATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalNegation)))))))))))], + [BiconditionalSubstitution, "BICONDITIONAL_SUBSTITUTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::BiconditionalSubstitution)))))))))))], + [KnightsAndKnaves, "KNIGHTS_AND_KNAVES", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(BiconditionalEquivalence::KnightsAndKnaves)))))))))))], + + [QuantifierNegation, "QUANTIFIER_NEGATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::QuantifierNegation))))))))))))], + [NullQuantification, "NULL_QUANTIFICATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::NullQuantification))))))))))))], + [ReplacingBoundVars, "REPLACING_BOUND_VARS", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::ReplacingBoundVars))))))))))))], + [SwappingQuantifiers, "SWAPPING_QUANTIFIERS", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::SwappingQuantifiers))))))))))))], + [AristoteleanSquare, "ARISTOTELEAN_SQUARE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::AristoteleanSquare))))))))))))], + [QuantifierDistribution, "QUANTIFIER_DISTRIBUTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::QuantifierDistribution))))))))))))], + [PrenexLaws, "PRENEX_LAWS", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(QuantifierEquivalence::PrenexLaws))))))))))))], + + [Reiteration, "REITERATION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(Special::Reiteration)))))))))))))], + [Resolution, "RESOLUTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(Special::Resolution)))))))))))))], + [TruthFunctionalConsequence, "TRUTHFUNCTIONAL_CONSEQUENCE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(Special::TruthFunctionalConsequence)))))))))))))], + + [WeakInduction, "WEAK_INDUCTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(Induction::Weak))))))))))))))], + [StrongInduction, "STRONG_INDUCTION", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(Induction::Strong))))))))))))))], + + [EmptyRule, "EMPTY_RULE", (SharedChecks(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inr(Inl(super::EmptyRule)))))))))))))))] } } @@ -348,8 +385,14 @@ pub mod RuleM { pub enum RuleClassification { Introduction, Elimination, - #[strum(to_string = "Misc. Inference")] - MiscInference, + #[strum(to_string = "Boolean Inference")] + BooleanInference, + #[strum(to_string = "Conditional Inference")] + ConditionalInference, + #[strum(to_string = "Biconditional Inference")] + BiconditionalInference, + #[strum(to_string = "Quantifier Inference")] + QuantifierInference, #[strum(to_string = "Boolean Equivalence")] BooleanEquivalence, #[strum(to_string = "Conditional Equivalence")] @@ -358,6 +401,8 @@ pub enum RuleClassification { BiconditionalEquivalence, #[strum(to_string = "Quantifier Equivalence")] QuantifierEquivalence, + Special, + Induction, } impl RuleClassification { @@ -481,7 +526,6 @@ impl RuleT for PrepositionalInference { fn get_name(&self) -> String { use PrepositionalInference::*; match self { - Reit => "Reiteration", AndIntro => "∧ Introduction", AndElim => "∧ Elimination", OrIntro => "∨ Introduction", @@ -504,9 +548,6 @@ impl RuleT for PrepositionalInference { use RuleClassification::*; let mut ret = HashSet::new(); match self { - Reit => { - ret.insert(MiscInference); - } AndIntro | OrIntro | ImpIntro | NotIntro | ContradictionIntro | BiconditionalIntro | EquivalenceIntro => { ret.insert(Introduction); } @@ -519,7 +560,7 @@ impl RuleT for PrepositionalInference { fn num_deps(&self) -> Option { use PrepositionalInference::*; match self { - Reit | AndElim | OrIntro | OrElim | NotElim | ContradictionElim => Some(1), + AndElim | OrIntro | OrElim | NotElim | ContradictionElim => Some(1), ContradictionIntro | ImpElim | BiconditionalElim | EquivalenceElim => Some(2), NotIntro | ImpIntro => Some(0), AndIntro | BiconditionalIntro | EquivalenceIntro => None, // AndIntro can have arbitrarily many conjuncts in one application @@ -529,7 +570,7 @@ impl RuleT for PrepositionalInference { use PrepositionalInference::*; match self { NotIntro | ImpIntro => Some(1), - Reit | AndElim | OrIntro | NotElim | ContradictionElim | ContradictionIntro | ImpElim | AndIntro | BiconditionalElim | EquivalenceElim => Some(0), + AndElim | OrIntro | NotElim | ContradictionElim | ContradictionIntro | ImpElim | AndIntro | BiconditionalElim | EquivalenceElim => Some(0), OrElim | BiconditionalIntro | EquivalenceIntro => None, } } @@ -539,14 +580,6 @@ impl RuleT for PrepositionalInference { use PrepositionalInference::*; use ProofCheckError::*; match self { - Reit => { - let prem = p.lookup_expr_or_die(&deps[0])?; - if prem == conclusion { - Ok(()) - } else { - Err(DoesNotOccur(conclusion, prem)) - } - } AndIntro => { if deps.len() == 1 { let single_dep_expr = p.lookup_expr_or_die(&deps[0])?; @@ -570,7 +603,7 @@ impl RuleT for PrepositionalInference { } Ok(()) } else { - Err(ConclusionOfWrongForm(Expr::assocplaceholder(Op::And))) + Err(ConclusionOfWrongForm(Expr::assoc_place_holder(Op::And))) } } AndElim => { @@ -601,7 +634,7 @@ impl RuleT for PrepositionalInference { } } } else { - Err(DepDoesNotExist(Expr::assocplaceholder(Op::And), true)) + Err(DepDoesNotExist(Expr::assoc_place_holder(Op::And), true)) } } OrIntro => { @@ -618,7 +651,7 @@ impl RuleT for PrepositionalInference { } Ok(()) } else { - Err(ConclusionOfWrongForm(Expr::assocplaceholder(Op::Or))) + Err(ConclusionOfWrongForm(Expr::assoc_place_holder(Op::Or))) } } OrElim => { @@ -641,7 +674,7 @@ impl RuleT for PrepositionalInference { } Ok(()) } else { - Err(DepDoesNotExist(Expr::assocplaceholder(Op::Or), true)) + Err(DepDoesNotExist(Expr::assoc_place_holder(Op::Or), true)) } } ImpIntro => { @@ -771,7 +804,7 @@ impl RuleT for PrepositionalInference { AnyOrderResult::WrongOrder } }, - || DepDoesNotExist(Expr::assocplaceholder(Op::Bicon), true), + || DepDoesNotExist(Expr::assoc_place_holder(Op::Bicon), true), ) } EquivalenceIntro | BiconditionalIntro => { @@ -808,7 +841,7 @@ impl RuleT for PrepositionalInference { slab.entry(*right.clone()).or_insert_with(|| next()); g.add_edge(slab[left], slab[right], ()); } - _ => return Err(OneOf(btreeset![DepOfWrongForm(prem.clone(), Expr::assocplaceholder(oper)), DepOfWrongForm(prem.clone(), Expr::impl_place_holder()),])), + _ => return Err(OneOf(btreeset![DepOfWrongForm(prem.clone(), Expr::assoc_place_holder(oper)), DepOfWrongForm(prem.clone(), Expr::impl_place_holder()),])), } } for sproof in sproofs.iter() { @@ -847,7 +880,7 @@ impl RuleT for PrepositionalInference { } } } - Err(ConclusionOfWrongForm(Expr::assocplaceholder(oper))) + Err(ConclusionOfWrongForm(Expr::assoc_place_holder(oper))) } EquivalenceElim => { let prem1 = p.lookup_expr_or_die(&deps[0])?; @@ -869,7 +902,7 @@ impl RuleT for PrepositionalInference { AnyOrderResult::WrongOrder } }, - || DepDoesNotExist(Expr::assocplaceholder(Op::Equiv), true), + || DepDoesNotExist(Expr::assoc_place_holder(Op::Equiv), true), ) } } @@ -968,7 +1001,7 @@ impl RuleT for PredicateInference { } Err(Other(format!("Couldn't find a subproof line that unifies with the conclusion ({conclusion})."))) } else { - Err(ConclusionOfWrongForm(Expr::quant_placeholder(QuantKind::Forall))) + Err(ConclusionOfWrongForm(Expr::quant_place_holder(QuantKind::Forall))) } } ForallElim => { @@ -977,7 +1010,7 @@ impl RuleT for PredicateInference { unifies_wrt_var::

(body, &conclusion, name)?; Ok(()) } else { - Err(DepOfWrongForm(prem, Expr::quant_placeholder(QuantKind::Forall))) + Err(DepOfWrongForm(prem, Expr::quant_place_holder(QuantKind::Forall))) } } ExistsIntro => { @@ -986,7 +1019,7 @@ impl RuleT for PredicateInference { unifies_wrt_var::

(body, &prem, name)?; Ok(()) } else { - Err(ConclusionOfWrongForm(Expr::quant_placeholder(QuantKind::Exists))) + Err(ConclusionOfWrongForm(Expr::quant_place_holder(QuantKind::Exists))) } } ExistsElim => { @@ -1019,7 +1052,7 @@ impl RuleT for PredicateInference { return Err(Other(format!("Premise {subprem} doesn't unify with the body of dependency {prem}"))); } } else { - return Err(DepOfWrongForm(prem, Expr::quant_placeholder(QuantKind::Exists))); + return Err(DepOfWrongForm(prem, Expr::quant_place_holder(QuantKind::Exists))); } }; for (r, expr) in sproof.exprs().into_iter().map(|r| sproof.lookup_expr_or_die(&r).map(|e| (r, e))).collect::, _>>()? { @@ -1040,153 +1073,745 @@ impl RuleT for PredicateInference { } } -fn check_by_normalize_first_expr(p: &P, deps: Vec>, conclusion: Expr, commutative: bool, normalize_fn: F, restriction: &str) -> Result<(), ProofCheckError, P::SubproofReference>> -where - F: Fn(Expr) -> Expr, -{ - let mut premise = p.lookup_expr_or_die(&deps[0])?; - let mut conclusion_mut = conclusion; - if commutative { - premise = premise.sort_commutative_ops(restriction); - conclusion_mut = conclusion_mut.sort_commutative_ops(restriction); +impl RuleT for BooleanInference { + fn get_name(&self) -> String { + use BooleanInference::*; + match self { + DisjunctiveSyllogism => "Disjunctive Syllogism", + Exclusion => "Exclusion", + ExcludedMiddle => "Excluded Middle", + HalfDeMorgan => "Half DeMorgan", + } + .into() } - let mut p = normalize_fn(premise.clone()); - let mut q = normalize_fn(conclusion_mut); - if commutative { - p = p.sort_commutative_ops(restriction); - q = q.sort_commutative_ops(restriction); + fn get_classifications(&self) -> HashSet { + [RuleClassification::BooleanInference].iter().cloned().collect() } - if p == q { - Ok(()) - } else { - Err(ProofCheckError::Other(format!("{p} and {q} are not equal. {:?}", premise))) + fn num_deps(&self) -> Option { + use BooleanInference::*; + match self { + DisjunctiveSyllogism | Exclusion => Some(2), + ExcludedMiddle => Some(0), + HalfDeMorgan => Some(1), + } } -} - -fn check_by_normalize_first_expr_one_way(p: &P, deps: Vec>, conclusion: Expr, normalize_fn: F) -> Result<(), ProofCheckError, P::SubproofReference>> -where - F: Fn(Expr) -> Expr, -{ - let premise = p.lookup_expr_or_die(&deps[0])?; - let p = normalize_fn(premise.clone()); - if p == conclusion.clone() { - Ok(()) - } else { - Err(ProofCheckError::Other(format!("{p} and {conclusion} are not equal. {:?}", premise))) + fn num_subdeps(&self) -> Option { + Some(0) } -} + fn check(self, proof: &P, conclusion: Expr, deps: Vec>, sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { + use BooleanInference::*; + use ProofCheckError::*; -fn check_by_normalize_multiple_possibilities(p: &P, deps: Vec>, conclusion: Expr, normalize_fn: F) -> Result<(), ProofCheckError, P::SubproofReference>> -where - F: Fn(Expr) -> Vec, -{ - let premise = p.lookup_expr_or_die(&deps[0])?; + assert!(sdeps.is_empty()); + match self { + DisjunctiveSyllogism => { + let dep_0 = proof.lookup_expr_or_die(&deps[0])?; + let dep_1 = proof.lookup_expr_or_die(&deps[1])?; - // Generate all possible transformed premises and conclusions - let premise_possibilities = normalize_fn(premise); - let conclusion_possibilities = normalize_fn(conclusion); + let is_disjunctive_case = |disj, negation, conclusion| { + if let Expr::Assoc { op: Op::Or, exprs } = disj { + if exprs.len() == 2 { + let (p, q) = (&exprs[0], &exprs[1]); - // Check if any conclusion possibility matches a premise possibility - for premise_expr in premise_possibilities.iter() { - for conclusion_expr in conclusion_possibilities.iter() { - if premise_expr == conclusion_expr { - return Ok(()); // If a match is found, return success + match (p, q, negation, conclusion) { + // Case 1: P | Q, ~P concludes Q + (p_expr, q_expr, Expr::Not { operand }, conclusion) if p_expr == &*operand && q_expr == conclusion => true, + // Case 2: P | Q, ~Q concludes P + (p_expr, q_expr, Expr::Not { operand }, conclusion) if q_expr == &*operand && p_expr == conclusion => true, + // Case 3: ~P | Q, P concludes Q + (Expr::Not { operand }, q_expr, p_expr, conclusion) if **operand == p_expr && q_expr == conclusion => true, + // Case 4: P | ~Q, Q concludes P + (p_expr, Expr::Not { operand }, q_expr, conclusion) if **operand == q_expr && p_expr == conclusion => true, + _ => false, + } + } else { + false + } + } else { + false + } + }; + + // Check if dep_0 or dep_1 is the disjunction, and apply the disjunctive syllogism rule + if is_disjunctive_case(dep_0.clone(), dep_1.clone(), &conclusion) || is_disjunctive_case(dep_1, dep_0, &conclusion) { + Ok(()) + } else { + Err(ProofCheckError::Other("Conclusion does not logically follow from premises".to_string())) + } } - } - } + Exclusion => { + let dep_0 = proof.lookup_expr_or_die(&deps[0])?; + let dep_1 = proof.lookup_expr_or_die(&deps[1])?; - Err(ProofCheckError::Other("None of the possible normalized premises match the conclusion.".to_string())) -} + let is_exclusion_case = |neg_conj, premise, conclusion| { + if let Expr::Not { operand } = neg_conj { + if let Expr::Assoc { op: Op::And, exprs } = operand.as_ref() { + if exprs.len() == 2 { + let (p, q) = (&exprs[0], &exprs[1]); + + match (p, q, premise, conclusion) { + // Case 1: !(P & Q), P concludes ~Q + (p_expr, q_expr, premise_expr, Expr::Not { operand: concl_q }) if *p_expr == premise_expr && q_expr == &*concl_q => true, + // Case 2: !(P & Q), Q concludes ~P + (p_expr, q_expr, premise_expr, Expr::Not { operand: concl_p }) if *q_expr == premise_expr && p_expr == &*concl_p => true, + // Case 3: !(P & ~Q), P concludes Q + (p_expr, Expr::Not { operand: q_expr }, premise_expr, conclusion_expr) if *p_expr == premise_expr && **q_expr == conclusion_expr => true, + // Case 4: !(!P & Q), Q concludes P + (Expr::Not { operand: p_expr }, q_expr, premise_expr, conclusion_expr) if *q_expr == premise_expr && **p_expr == conclusion_expr => true, + _ => false, + } + } else { + false + } + } else { + false + } + } else { + false + } + }; -fn check_by_rewrite_rule_confl(p: &P, deps: Vec>, conclusion: Expr, commutative: bool, rule: &RewriteRule, restriction: &str) -> Result<(), ProofCheckError, P::SubproofReference>> { - check_by_normalize_first_expr(p, deps, conclusion, commutative, |e| rule.reduce(e), restriction) -} + if is_exclusion_case(dep_0.clone(), dep_1.clone(), conclusion.clone()) || is_exclusion_case(dep_1, dep_0, conclusion) { + Ok(()) + } else { + Err(ProofCheckError::Other("Conclusion does not logically follow from premises".to_string())) + } + } + ExcludedMiddle => { + // A | ~A + let wrong_form_err = ConclusionOfWrongForm(Expr::var("_") | !Expr::var("_")); + let operands = match conclusion { + Expr::Assoc { op: Op::Or, exprs } => exprs, + _ => return Err(wrong_form_err), + }; -// fn check_by_rewrite_rule_non_confl(p: &P, deps: Vec>, conclusion: Expr, commutative: bool, rule: &RewriteRule, restriction: &str) -> Result<(), ProofCheckError, P::SubproofReference>> { -// let premise = p.lookup_expr_or_die(&deps[0])?; -// let premise_set = rule.reduce_set(premise.clone()); -// let conclusion_set = rule.reduce_set(conclusion.clone()); -// let (premise_set, conclusion_set) = if commutative { -// let sort_ops = |set: HashSet| set.into_iter().map(|expr| expr.sort_commutative_ops(restriction)).collect(); -// (sort_ops(premise_set), sort_ops(conclusion_set)) -// } else { -// (premise_set, conclusion_set) -// }; -// // The premise and conclusion are equal if the set intersection is nonempty -// let is_eq = premise_set.intersection(&conclusion_set).next().is_some(); -// if is_eq { -// Ok(()) -// } else { -// Err(ProofCheckError::Other(format!("{premise} and {conclusion} are not equal."))) -// } -// } + let (a, not_a) = match operands.as_slice() { + [a, not_a] => (a, not_a), + _ => return Err(wrong_form_err), + }; -impl RuleT for BooleanEquivalence { + let not_a_0 = not_a.clone(); + let not_a_1 = !(a.clone()); + + if not_a_0 == not_a_1 { + Ok(()) + } else { + Err(DoesNotOccur(not_a_0, not_a_1)) + } + } + HalfDeMorgan => check_by_normalize_multiple_possibilities(proof, deps, conclusion, |e| e.normalize_halfdemorgans()), + } + } +} + +impl RuleT for ConditionalInference { fn get_name(&self) -> String { - use BooleanEquivalence::*; + use ConditionalInference::*; match self { - DeMorgan => "DeMorgan", - Association => "Association", - Commutation => "Commutation", - Idempotence => "Idempotence", - Distribution => "Distribution", - DoubleNegation => "Double Negation", - Complement => "Complement", - Identity => "Identity", - Annihilation => "Annihilation", - Inverse => "Inverse", - Absorption => "Absorption", - Reduction => "Reduction", - Adjacency => "Adjacency", + ModusTollens => "Modus Tollens", + HypotheticalSyllogism => "Hypothetical Syllogism", + ConstructiveDilemma => "Constructive Dilemma", + DestructiveDilemma => "Destructive Dilemma", + StrengthenAntecedent => "Strengthening the Antecedent", + WeakenConsequent => "Weakening the Consequent", + ConIntroNegation => "Conditional Introduction Negation", + ConElimNegation => "Conditional Elimination Negation", } .into() } fn get_classifications(&self) -> HashSet { - [RuleClassification::BooleanEquivalence].iter().cloned().collect() + [RuleClassification::ConditionalInference].iter().cloned().collect() } fn num_deps(&self) -> Option { - Some(1) - } // all equivalence rules rewrite a single statement - fn num_subdeps(&self) -> Option { - Some(0) - } - fn check(self, p: &P, conclusion: Expr, deps: Vec>, _sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { - use BooleanEquivalence::*; + use ConditionalInference::*; match self { - DeMorgan => check_by_normalize_first_expr(p, deps, conclusion, false, |e| e.normalize_demorgans(), "none"), - Association => check_by_normalize_first_expr(p, deps, conclusion, false, |e| e.combine_associative_ops("bool"), "bool"), - Commutation => check_by_normalize_first_expr(p, deps, conclusion, false, |e| e.sort_commutative_ops("bool"), "bool"), - Idempotence => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_idempotence(), "none"), - DoubleNegation => check_by_rewrite_rule_confl(p, deps, conclusion, false, &equivs::DOUBLE_NEGATION, "none"), - // Distribution and Reduction have outputs containing binops that need commutative sorting - // because we can't expect people to know the specific order of outputs that our definition - // of the rules uses - Distribution => check_by_rewrite_rule_confl(p, deps, conclusion, true, &equivs::DISTRIBUTION, "none"), - Complement => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_complement(), "none"), - Identity => check_by_rewrite_rule_confl(p, deps, conclusion, false, &equivs::IDENTITY, "none"), - Annihilation => check_by_rewrite_rule_confl(p, deps, conclusion, false, &equivs::ANNIHILATION, "none"), - Inverse => check_by_rewrite_rule_confl(p, deps, conclusion, false, &equivs::INVERSE, "none"), - Absorption => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_absorption(), "none"), - Reduction => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_reduction(), "none"), - Adjacency => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_adjacency(), "none"), + ModusTollens | HypotheticalSyllogism => Some(2), + ConstructiveDilemma | DestructiveDilemma => Some(3), + StrengthenAntecedent | WeakenConsequent | ConIntroNegation | ConElimNegation => Some(1), } } -} + fn num_subdeps(&self) -> Option { + Some(0) + } + fn check(self, proof: &P, conclusion: Expr, deps: Vec>, sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { + use ConditionalInference::*; + use ProofCheckError::*; -impl RuleT for ConditionalEquivalence { - fn get_name(&self) -> String { - use ConditionalEquivalence::*; + assert!(sdeps.is_empty()); match self { - Implication => "Implication", - Contraposition => "Contraposition", - Exportation => "Exportation", - ConditionalDistribution => "Conditional Distribution", - ConditionalAbsorption => "Conditional Absorption", - ConditionalReduction => "Conditional Reduction", - ConditionalIdempotence => "Conditional Idempotence", - ConditionalComplement => "Conditional Complement", - ConditionalIdentity => "Conditional Identity", - ConditionalAnnihilation => "Conditional Annihilation", + ModusTollens => { + let dep_0 = proof.lookup_expr_or_die(&deps[0])?; + let dep_1 = proof.lookup_expr_or_die(&deps[1])?; + + let is_modus_tollens_case = |implication, negation, conclusion| { + if let Expr::Impl { left, right } = implication { + match (left.as_ref(), right.as_ref(), negation, conclusion) { + // Case 1: P -> Q, ~Q concludes ~P + (p, q, Expr::Not { operand }, Expr::Not { operand: concl_p }) if q == &*operand && p == &*concl_p => true, + // Case 2: P -> ~Q, Q concludes ~P + (p, Expr::Not { operand: q }, neg_q, Expr::Not { operand: concl_p }) if **q == neg_q && p == &*concl_p => true, + // Case 3: ~P -> Q, ~Q concludes P + (Expr::Not { operand: p }, q, Expr::Not { operand: neg_q }, concl_p) if *q == *neg_q && **p == concl_p => true, + // Case 4: ~P -> ~Q, Q concludes P + (Expr::Not { operand: p }, Expr::Not { operand: q }, neg_q, concl_p) if **q == neg_q && **p == concl_p => true, + _ => false, + } + } else { + false + } + }; + + // Check if dep_0 or dep_1 is the implication, and apply the Modus Tollens rule + if is_modus_tollens_case(dep_0.clone(), dep_1.clone(), conclusion.clone()) || is_modus_tollens_case(dep_1, dep_0, conclusion) { + Ok(()) + } else { + Err(ProofCheckError::Other("Conclusion does not logically follow from premises".to_string())) + } + } + HypotheticalSyllogism => { + // P -> Q, Q -> R + // -------------- + // P -> R + let dep_0 = proof.lookup_expr_or_die(&deps[0])?; + let dep_1 = proof.lookup_expr_or_die(&deps[1])?; + either_order( + &dep_0, + &dep_1, + |dep_0, dep_1| { + if let (Expr::Impl { left: p_0, right: q_0 }, Expr::Impl { left: q_1, right: r_0 }, Expr::Impl { left: p_1, right: r_1 }) = (dep_0, dep_1, &conclusion) { + if p_0 != p_1 { + AnyOrderResult::Err(DoesNotOccur(*p_0.clone(), *p_1.clone())) + } else if q_0 != q_1 { + AnyOrderResult::Err(DoesNotOccur(*q_0.clone(), *q_1.clone())) + } else if r_0 != r_1 { + AnyOrderResult::Err(DoesNotOccur(*r_0.clone(), *r_1.clone())) + } else { + AnyOrderResult::Ok + } + } else { + AnyOrderResult::WrongOrder + } + }, + || DepDoesNotExist(Expr::impl_place_holder(), true), + ) + } + ConstructiveDilemma => { + // P -> Q, R -> S, P | R + // --------------------- + // Q | S + let deps = deps.into_iter().map(|dep| proof.lookup_expr_or_die(&dep)).collect::, _>>()?; + any_order( + &deps, + |deps| { + let (dep_0, dep_1, dep_2) = deps.iter().collect_tuple().unwrap(); + if let (Expr::Impl { left: p_0, right: q_0 }, Expr::Impl { left: r_0, right: s_0 }, Expr::Assoc { op: Op::Or, exprs: p_r }, Expr::Assoc { op: Op::Or, exprs: q_s }) = (dep_0, dep_1, dep_2, &conclusion) { + let p_0 = *p_0.clone(); + let q_0 = *q_0.clone(); + let r_0 = *r_0.clone(); + let s_0 = *s_0.clone(); + let dep_2 = (*dep_2).clone(); + let conclusion = conclusion.clone(); + + let (p_1, r_1) = match p_r.iter().collect_tuple() { + Some((p_1, r_1)) => (p_1, r_1), + None => return AnyOrderResult::Err(DoesNotOccur(p_0 | r_0, dep_2)), + }; + let (q_1, s_1) = match q_s.iter().collect_tuple() { + Some((q_1, s_1)) => (q_1, s_1), + None => return AnyOrderResult::Err(DoesNotOccur(q_0 | s_0, conclusion)), + }; + + let p_1 = p_1.clone(); + let q_1 = q_1.clone(); + let r_1 = r_1.clone(); + let s_1 = s_1.clone(); + + if p_0 != p_1 { + AnyOrderResult::Err(DoesNotOccur(p_0, p_1)) + } else if q_0 != q_1 { + AnyOrderResult::Err(DoesNotOccur(q_0, q_1)) + } else if r_0 != r_1 { + AnyOrderResult::Err(DoesNotOccur(r_0, r_1)) + } else if s_0 != s_1 { + AnyOrderResult::Err(DoesNotOccur(s_0, s_1)) + } else { + AnyOrderResult::Ok + } + } else { + AnyOrderResult::WrongOrder + } + }, + || OneOf(btreeset![DepDoesNotExist(Expr::impl_place_holder(), true), DepDoesNotExist(Expr::assoc_place_holder(Op::Or), true),]), + ) + } + DestructiveDilemma => { + // ~R | ~S, P -> R, Q -> S + // ----------------------- + // ~P | ~Q OR ~Q | ~P + let deps = deps.into_iter().map(|dep| proof.lookup_expr_or_die(&dep)).collect::, _>>()?; + any_order( + &deps, + |deps| { + let (dep_0, dep_1, dep_2) = deps.iter().collect_tuple().unwrap(); + if let (Expr::Assoc { op: Op::Or, exprs: neg_rs }, Expr::Impl { left: p_0, right: r_0 }, Expr::Impl { left: q_0, right: s_0 }, Expr::Assoc { op: Op::Or, exprs: neg_pq }) = (dep_0, dep_1, dep_2, &conclusion) { + let p_0 = *p_0.clone(); + let q_0 = *q_0.clone(); + let r_0 = *r_0.clone(); + let s_0 = *s_0.clone(); + let dep_0 = (*dep_0).clone(); + let conclusion = conclusion.clone(); + + let (neg_r, neg_s) = match neg_rs.iter().collect_tuple() { + Some((neg_r, neg_s)) => (neg_r, neg_s), + None => return AnyOrderResult::Err(DoesNotOccur(Expr::assoc_place_holder(Op::Or), dep_0)), + }; + + let neg_p_set = neg_pq.iter().collect::>(); + + let neg_r = neg_r.clone(); + let neg_s = neg_s.clone(); + + if let Expr::Not { operand: r_1 } = neg_r { + if r_0 != *r_1 { + return AnyOrderResult::Err(DoesNotOccur(r_0, *r_1)); + } + } else { + return AnyOrderResult::WrongOrder; + } + + if let Expr::Not { operand: s_1 } = neg_s { + if s_0 != *s_1 { + return AnyOrderResult::Err(DoesNotOccur(s_0, *s_1)); + } + } else { + return AnyOrderResult::WrongOrder; + } + + let expected_neg_p = Expr::Not { operand: Box::new(p_0.clone()) }; + let expected_neg_q = Expr::Not { operand: Box::new(q_0.clone()) }; + + if !neg_p_set.contains(&expected_neg_p) || !neg_p_set.contains(&expected_neg_q) { + return AnyOrderResult::Err(DoesNotOccur(Expr::assoc_place_holder(Op::Or), conclusion)); + } + + AnyOrderResult::Ok + } else { + AnyOrderResult::WrongOrder + } + }, + || OneOf(btreeset![DepDoesNotExist(Expr::assoc_place_holder(Op::Or), true), DepDoesNotExist(Expr::impl_place_holder(), true),]), + ) + } + StrengthenAntecedent => { + let dep_0 = proof.lookup_expr_or_die(&deps[0])?; + if let Expr::Impl { left, right } = dep_0.clone() { + // Case 1: Premise: P -> R, Conclusion: (P & Q) -> R or (Q & P) -> R + if let Expr::Impl { left: strengthened_left, right: strengthened_right } = conclusion.clone() { + if *right == *strengthened_right { + if let Expr::Assoc { op: Op::And, exprs } = strengthened_left.as_ref() { + if exprs.contains(&*left) { + return Ok(()); + } + } + } + } + + // Case 2: Premise: (P | Q) -> R, Conclusion: P -> R or Q -> R + if let Expr::Impl { left: conclusion_left, right: conclusion_right } = conclusion { + if *right == *conclusion_right { + if let Expr::Assoc { op: Op::Or, exprs } = left.as_ref() { + if exprs.contains(&*conclusion_left) { + return Ok(()); + } + } + } + } + } + + Err(ProofCheckError::Other("Conclusion does not follow from the Strengthening the Antecedent rule.".to_string())) + } + WeakenConsequent => { + let dep_0 = proof.lookup_expr_or_die(&deps[0])?; + if let Expr::Impl { left, right } = dep_0.clone() { + // Case 1 and 2: Premise: P -> (Q & R), Conclusion: P -> Q or P -> R + if let Expr::Impl { left: conclusion_left, right: conclusion_right } = conclusion.clone() { + if *left == *conclusion_left { + if let Expr::Assoc { op: Op::And, exprs } = right.as_ref() { + if exprs.contains(&*conclusion_right) { + return Ok(()); + } + } + } + } + + // Case 3 and 4: Premise: P -> Q, Conclusion: P -> (Q | R) or P -> (R | Q) + if let Expr::Impl { left: conclusion_left, right: conclusion_right } = conclusion { + if *left == *conclusion_left { + if let Expr::Assoc { op: Op::Or, exprs } = conclusion_right.as_ref() { + if exprs.contains(&*right) { + return Ok(()); + } + } + } + } + } + + Err(ProofCheckError::Other("Conclusion does not follow from the Weaken the Consequent rule.".to_string())) + } + ConIntroNegation => { + let premise = proof.lookup_expr_or_die(&deps[0])?; + + if let Expr::Impl { ref left, ref right } = conclusion { + // Case 1: Premise: ~P, Conclusion: P -> Q + if let Expr::Not { ref operand } = premise { + if **operand == **left && !matches!(**right, Expr::Not { .. }) { + return Ok(()); + } + } + + // Case 2: Premise: Q, Conclusion: P -> Q + if premise == **right && !matches!(**left, Expr::Not { .. }) { + return Ok(()); + } + } + + Err(ProofCheckError::Other("Conclusion does not follow from the Conditional Introduction Negation rule.".to_string())) + } + + ConElimNegation => { + let premise = proof.lookup_expr_or_die(&deps[0])?; + + if let Expr::Not { ref operand } = premise { + if let Expr::Impl { ref left, ref right } = **operand { + // Case 1: Premise: ~(P -> Q), Conclusion: P + if conclusion == **left { + return Ok(()); + } + + // Case 2: Premise: ~(P -> Q), Conclusion: ~Q + if conclusion == (Expr::Not { operand: Box::new(*right.clone()) }) { + return Ok(()); + } + } + } + + Err(ProofCheckError::Other("Conclusion does not follow from the Conditional Elimination Negation rule.".to_string())) + } + } + } +} + +impl RuleT for BiconditionalInference { + fn get_name(&self) -> String { + use BiconditionalInference::*; + match self { + BiconIntro => "Biconditional Introduction", + BiconIntroNegation => "Biconditional Introduction Negation", + BiconElim => "Biconditional Elimination", + BiconElimNegation => "Biconditional Elimination Negation", + } + .into() + } + fn get_classifications(&self) -> HashSet { + [RuleClassification::BiconditionalInference].iter().cloned().collect() + } + fn num_deps(&self) -> Option { + use BiconditionalInference::*; + match self { + BiconIntro | BiconIntroNegation | BiconElim | BiconElimNegation => Some(2), + } + } + fn num_subdeps(&self) -> Option { + Some(0) + } + fn check(self, proof: &P, conclusion: Expr, deps: Vec>, sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { + use crate::rules::ProofCheckError::*; + use BiconditionalInference::*; + + assert!(sdeps.is_empty()); + match self { + BiconIntro => { + let prem1 = proof.lookup_expr_or_die(&deps[0])?; + let prem2 = proof.lookup_expr_or_die(&deps[1])?; + + either_order( + &prem1, + &prem2, + |i, j| { + match (i, j) { + // Case 1: Both premises are variables (P and Q) + (Expr::Var { name: ref left }, Expr::Var { name: ref right }) => { + if conclusion == Expr::assoc(Op::Bicon, &[Expr::var(left), Expr::var(right)]) { + return AnyOrderResult::Ok; + } + } + // Case 2: Both premises are negations (~P and ~Q) + (Expr::Not { operand: ref left }, Expr::Not { operand: ref right }) => { + if conclusion == Expr::assoc(Op::Bicon, &[*left.clone(), *right.clone()]) || conclusion == Expr::assoc(Op::Bicon, &[Expr::Not { operand: left.clone() }, Expr::Not { operand: right.clone() }]) { + return AnyOrderResult::Ok; + } + } + _ => {} + } + + AnyOrderResult::Err(DoesNotOccur(conclusion.clone(), Expr::assoc_place_holder(Op::Bicon))) + }, + || DepDoesNotExist(Expr::assoc_place_holder(Op::Bicon), true), + ) + } + BiconIntroNegation => { + let prem1 = proof.lookup_expr_or_die(&deps[0])?; + let prem2 = proof.lookup_expr_or_die(&deps[1])?; + + either_order( + &prem1, + &prem2, + |i, j| { + match (i, j) { + // Case 1: Premises: ~P and Q, Conclusion: ~(P <-> Q) + (Expr::Not { operand: ref left }, Expr::Var { name: ref right }) => { + if conclusion == (Expr::Not { operand: Box::new(Expr::assoc(Op::Bicon, &[*left.clone(), Expr::var(right)])) }) { + return AnyOrderResult::Ok; + } + } + // Case 2: Premises are P and ~Q, Conclusion: ~(P <-> Q) + (Expr::Var { name: ref left }, Expr::Not { operand: ref right }) => { + if conclusion == (Expr::Not { operand: Box::new(Expr::assoc(Op::Bicon, &[Expr::var(left), *right.clone()])) }) { + return AnyOrderResult::Ok; + } + } + _ => {} + } + + AnyOrderResult::Err(DoesNotOccur(conclusion.clone(), Expr::not_place_holder())) + }, + || DepDoesNotExist(Expr::not_place_holder(), true), + ) + } + BiconElim => { + let prem1 = proof.lookup_expr_or_die(&deps[0])?; + let prem2 = proof.lookup_expr_or_die(&deps[1])?; + + either_order( + &prem1, + &prem2, + |i, j| { + if let Expr::Assoc { ref op, ref exprs } = i { + if *op == Op::Bicon && exprs.len() == 2 { + let left = &exprs[0]; + let right = &exprs[1]; + + if let Expr::Not { ref operand } = j { + if (**operand == *left && conclusion == Expr::Not { operand: Box::new(right.clone()) }) || (**operand == *right && conclusion == Expr::Not { operand: Box::new(left.clone()) }) { + return AnyOrderResult::Ok; + } else { + return AnyOrderResult::Err(DoesNotOccur(j.clone(), conclusion.clone())); + } + } + } + } + AnyOrderResult::WrongOrder + }, + || DepDoesNotExist(Expr::assoc_place_holder(Op::Bicon), true), + ) + } + BiconElimNegation => { + let prem1 = proof.lookup_expr_or_die(&deps[0])?; + let prem2 = proof.lookup_expr_or_die(&deps[1])?; + + either_order( + &prem1, + &prem2, + |i, j| { + if let Expr::Not { ref operand } = i { + if let Expr::Assoc { ref op, ref exprs } = **operand { + if *op == Op::Bicon && exprs.len() == 2 { + let left = &exprs[0]; + let right = &exprs[1]; + + if *left == *j { + if conclusion == (Expr::Not { operand: Box::new(right.clone()) }) { + return AnyOrderResult::Ok; + } else { + return AnyOrderResult::Err(DoesNotOccur(conclusion.clone(), right.clone())); + } + } + + if *right == *j { + if conclusion == (Expr::Not { operand: Box::new(left.clone()) }) { + return AnyOrderResult::Ok; + } else { + return AnyOrderResult::Err(DoesNotOccur(conclusion.clone(), left.clone())); + } + } + } + } + } + AnyOrderResult::WrongOrder + }, + || DepDoesNotExist(Expr::not_place_holder(), true), + ) + } + } + } +} + +impl RuleT for QuantifierInference { + fn get_name(&self) -> String { + use QuantifierInference::*; + match self { + QuantInference => "Quantifier Inference", + } + .into() + } + fn get_classifications(&self) -> HashSet { + [RuleClassification::QuantifierInference].iter().cloned().collect() + } + fn num_deps(&self) -> Option { + use QuantifierInference::*; + match self { + QuantInference => Some(1), + } + } + fn num_subdeps(&self) -> Option { + Some(0) + } + fn check(self, proof: &P, conclusion: Expr, deps: Vec>, sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { + use QuantifierInference::*; + + assert!(sdeps.is_empty()); + match self { + QuantInference => check_by_normalize_first_expr_one_way(proof, deps, conclusion, |e| e.quantifier_inference()), + } + } +} + +fn check_by_normalize_first_expr(p: &P, deps: Vec>, conclusion: Expr, commutative: bool, normalize_fn: F, restriction: &str) -> Result<(), ProofCheckError, P::SubproofReference>> +where + F: Fn(Expr) -> Expr, +{ + let mut premise = p.lookup_expr_or_die(&deps[0])?; + let mut conclusion_mut = conclusion; + if commutative { + premise = premise.sort_commutative_ops(restriction); + conclusion_mut = conclusion_mut.sort_commutative_ops(restriction); + } + let mut p = normalize_fn(premise.clone()); + let mut q = normalize_fn(conclusion_mut); + if commutative { + p = p.sort_commutative_ops(restriction); + q = q.sort_commutative_ops(restriction); + } + if p == q { + Ok(()) + } else { + Err(ProofCheckError::Other(format!("{p} and {q} are not equal. {:?}", premise))) + } +} + +fn check_by_normalize_first_expr_one_way(p: &P, deps: Vec>, conclusion: Expr, normalize_fn: F) -> Result<(), ProofCheckError, P::SubproofReference>> +where + F: Fn(Expr) -> Expr, +{ + let premise = p.lookup_expr_or_die(&deps[0])?; + let p = normalize_fn(premise.clone()); + if p == conclusion.clone() { + Ok(()) + } else { + Err(ProofCheckError::Other(format!("{p} and {conclusion} are not equal. {:?}", premise))) + } +} + +fn check_by_normalize_multiple_possibilities(p: &P, deps: Vec>, conclusion: Expr, normalize_fn: F) -> Result<(), ProofCheckError, P::SubproofReference>> +where + F: Fn(Expr) -> Vec, +{ + let premise = p.lookup_expr_or_die(&deps[0])?; + + let premise_possibilities = normalize_fn(premise); + let conclusion_possibilities = normalize_fn(conclusion); + + for premise_expr in premise_possibilities.iter() { + for conclusion_expr in conclusion_possibilities.iter() { + if premise_expr == conclusion_expr { + return Ok(()); + } + } + } + + Err(ProofCheckError::Other("None of the possible normalized premises match the conclusion.".to_string())) +} + +fn check_by_rewrite_rule_confl(p: &P, deps: Vec>, conclusion: Expr, commutative: bool, rule: &RewriteRule, restriction: &str) -> Result<(), ProofCheckError, P::SubproofReference>> { + check_by_normalize_first_expr(p, deps, conclusion, commutative, |e| rule.reduce(e), restriction) +} + +impl RuleT for BooleanEquivalence { + fn get_name(&self) -> String { + use BooleanEquivalence::*; + match self { + DeMorgan => "DeMorgan", + Association => "Association", + Commutation => "Commutation", + Idempotence => "Idempotence", + Distribution => "Distribution", + DoubleNegation => "Double Negation", + Complement => "Complement", + Identity => "Identity", + Annihilation => "Annihilation", + Inverse => "Inverse", + Absorption => "Absorption", + Reduction => "Reduction", + Adjacency => "Adjacency", + } + .into() + } + fn get_classifications(&self) -> HashSet { + [RuleClassification::BooleanEquivalence].iter().cloned().collect() + } + fn num_deps(&self) -> Option { + Some(1) + } // all equivalence rules rewrite a single statement + fn num_subdeps(&self) -> Option { + Some(0) + } + fn check(self, p: &P, conclusion: Expr, deps: Vec>, _sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { + use BooleanEquivalence::*; + match self { + DeMorgan => check_by_normalize_first_expr(p, deps, conclusion, false, |e| e.normalize_demorgans(), "none"), + Association => check_by_normalize_first_expr(p, deps, conclusion, false, |e| e.combine_associative_ops("bool"), "bool"), + Commutation => check_by_normalize_first_expr(p, deps, conclusion, false, |e| e.sort_commutative_ops("bool"), "bool"), + Idempotence => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_idempotence(), "none"), + DoubleNegation => check_by_rewrite_rule_confl(p, deps, conclusion, false, &equivs::DOUBLE_NEGATION, "none"), + // Distribution and Reduction have outputs containing binops that need commutative sorting + // because we can't expect people to know the specific order of outputs that our definition + // of the rules uses + Distribution => check_by_rewrite_rule_confl(p, deps, conclusion, true, &equivs::DISTRIBUTION, "none"), + Complement => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_complement(), "none"), + Identity => check_by_rewrite_rule_confl(p, deps, conclusion, false, &equivs::IDENTITY, "none"), + Annihilation => check_by_rewrite_rule_confl(p, deps, conclusion, false, &equivs::ANNIHILATION, "none"), + Inverse => check_by_rewrite_rule_confl(p, deps, conclusion, false, &equivs::INVERSE, "none"), + Absorption => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_absorption(), "none"), + Reduction => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_reduction(), "none"), + Adjacency => check_by_normalize_first_expr(p, deps, conclusion, true, |e| e.normalize_adjacency(), "none"), + } + } +} + +impl RuleT for ConditionalEquivalence { + fn get_name(&self) -> String { + use ConditionalEquivalence::*; + match self { + Implication => "Implication", + Contraposition => "Contraposition", + Exportation => "Exportation", + ConditionalDistribution => "Conditional Distribution", + ConditionalAbsorption => "Conditional Absorption", + ConditionalReduction => "Conditional Reduction", + ConditionalIdempotence => "Conditional Idempotence", + ConditionalComplement => "Conditional Complement", + ConditionalIdentity => "Conditional Identity", + ConditionalAnnihilation => "Conditional Annihilation", } .into() } @@ -1259,232 +1884,83 @@ impl RuleT for BiconditionalEquivalence { } } -impl RuleT for RedundantPrepositionalInference { +impl RuleT for QuantifierEquivalence { fn get_name(&self) -> String { - use RedundantPrepositionalInference::*; + use QuantifierEquivalence::*; match self { - ModusTollens => "Modus Tollens", - HypotheticalSyllogism => "Hypothetical Syllogism", - DisjunctiveSyllogism => "Disjunctive Syllogism", - ExcludedMiddle => "Excluded Middle", - ConstructiveDilemma => "Constructive Dilemma", - HalfDeMorgan => "Half DeMorgan", - QuantifierInference => "Quantifier Inference", + QuantifierNegation => "Quantifier Negation", + NullQuantification => "Null Quantification", + ReplacingBoundVars => "Replacing Bound Variables", + SwappingQuantifiers => "Swapping Quantifiers of Same Type", + AristoteleanSquare => "Aristotelean Square of Opposition", + QuantifierDistribution => "Quantifier Distribution", + PrenexLaws => "Prenex Laws", } .into() } fn get_classifications(&self) -> HashSet { - [RuleClassification::MiscInference].iter().cloned().collect() + [RuleClassification::QuantifierEquivalence].iter().cloned().collect() } fn num_deps(&self) -> Option { - use RedundantPrepositionalInference::*; - match self { - ModusTollens | HypotheticalSyllogism | DisjunctiveSyllogism => Some(2), - ExcludedMiddle => Some(0), - ConstructiveDilemma => Some(3), - HalfDeMorgan | QuantifierInference => Some(1), - } - } + Some(1) + } // all equivalence rules rewrite a single statement fn num_subdeps(&self) -> Option { Some(0) } - fn check(self, proof: &P, conclusion: Expr, deps: Vec>, sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { - use ProofCheckError::*; - use RedundantPrepositionalInference::*; - - assert!(sdeps.is_empty()); + fn check(self, p: &P, conclusion: Expr, deps: Vec>, _sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { + use QuantifierEquivalence::*; match self { - ModusTollens => { - // P -> Q, ~Q - // ---------- - // ~P - let dep_0 = proof.lookup_expr_or_die(&deps[0])?; - let dep_1 = proof.lookup_expr_or_die(&deps[1])?; - either_order( - &dep_0, - &dep_1, - |dep_0, dep_1| { - if let Expr::Impl { left: p, right: q } = dep_0 { - let not_p = !(*p.clone()); - let not_q = !(*q.clone()); - if not_q != *dep_1 { - AnyOrderResult::Err(DoesNotOccur(not_q, dep_1.clone())) - } else if not_p != conclusion { - AnyOrderResult::Err(DoesNotOccur(not_p, conclusion.clone())) - } else { - AnyOrderResult::Ok - } - } else { - AnyOrderResult::WrongOrder - } - }, - || DepDoesNotExist(Expr::impl_place_holder(), true), - ) - } - HypotheticalSyllogism => { - // P -> Q, Q -> R - // -------------- - // P -> R - let dep_0 = proof.lookup_expr_or_die(&deps[0])?; - let dep_1 = proof.lookup_expr_or_die(&deps[1])?; - either_order( - &dep_0, - &dep_1, - |dep_0, dep_1| { - if let (Expr::Impl { left: p_0, right: q_0 }, Expr::Impl { left: q_1, right: r_0 }, Expr::Impl { left: p_1, right: r_1 }) = (dep_0, dep_1, &conclusion) { - if p_0 != p_1 { - AnyOrderResult::Err(DoesNotOccur(*p_0.clone(), *p_1.clone())) - } else if q_0 != q_1 { - AnyOrderResult::Err(DoesNotOccur(*q_0.clone(), *q_1.clone())) - } else if r_0 != r_1 { - AnyOrderResult::Err(DoesNotOccur(*r_0.clone(), *r_1.clone())) - } else { - AnyOrderResult::Ok - } - } else { - AnyOrderResult::WrongOrder - } - }, - || DepDoesNotExist(Expr::impl_place_holder(), true), - ) - } - DisjunctiveSyllogism => { - let dep_0 = proof.lookup_expr_or_die(&deps[0])?; - let dep_1 = proof.lookup_expr_or_die(&deps[1])?; - - let is_disjunctive_case = |disj, negation, conclusion| { - if let Expr::Assoc { op: Op::Or, exprs } = disj { - if exprs.len() == 2 { - let (p, q) = (&exprs[0], &exprs[1]); - - match (p, q, negation, conclusion) { - // Case 1: P | Q, ~P concludes Q - (p_expr, q_expr, Expr::Not { operand }, conclusion) if p_expr == &*operand && q_expr == conclusion => true, - // Case 2: P | Q, ~Q concludes P - (p_expr, q_expr, Expr::Not { operand }, conclusion) if q_expr == &*operand && p_expr == conclusion => true, - // Case 3: ~P | Q, P concludes Q - (Expr::Not { operand }, q_expr, p_expr, conclusion) if **operand == p_expr && q_expr == conclusion => true, - // Case 4: P | ~Q, Q concludes P - (p_expr, Expr::Not { operand }, q_expr, conclusion) if **operand == q_expr && p_expr == conclusion => true, - _ => false, - } - } else { - false - } - } else { - false - } - }; - - // Check if dep_0 or dep_1 is the disjunction, and apply the disjunctive syllogism rule - if is_disjunctive_case(dep_0.clone(), dep_1.clone(), &conclusion) || is_disjunctive_case(dep_1, dep_0, &conclusion) { - Ok(()) - } else { - Err(ProofCheckError::Other("Conclusion does not logically follow from premises".to_string())) - } - } - ExcludedMiddle => { - // A | ~A - let wrong_form_err = ConclusionOfWrongForm(Expr::var("_") | !Expr::var("_")); - let operands = match conclusion { - Expr::Assoc { op: Op::Or, exprs } => exprs, - _ => return Err(wrong_form_err), - }; - - let (a, not_a) = match operands.as_slice() { - [a, not_a] => (a, not_a), - _ => return Err(wrong_form_err), - }; - - let not_a_0 = not_a.clone(); - let not_a_1 = !(a.clone()); - - if not_a_0 == not_a_1 { - Ok(()) - } else { - Err(DoesNotOccur(not_a_0, not_a_1)) - } - } - ConstructiveDilemma => { - // P -> Q, R -> S, P | R - // --------------------- - // Q | S - let deps = deps.into_iter().map(|dep| proof.lookup_expr_or_die(&dep)).collect::, _>>()?; - any_order( - &deps, - |deps| { - let (dep_0, dep_1, dep_2) = deps.iter().collect_tuple().unwrap(); - if let (Expr::Impl { left: p_0, right: q_0 }, Expr::Impl { left: r_0, right: s_0 }, Expr::Assoc { op: Op::Or, exprs: p_r }, Expr::Assoc { op: Op::Or, exprs: q_s }) = (dep_0, dep_1, dep_2, &conclusion) { - let p_0 = *p_0.clone(); - let q_0 = *q_0.clone(); - let r_0 = *r_0.clone(); - let s_0 = *s_0.clone(); - let dep_2 = (*dep_2).clone(); - let conclusion = conclusion.clone(); - - let (p_1, r_1) = match p_r.iter().collect_tuple() { - Some((p_1, r_1)) => (p_1, r_1), - None => return AnyOrderResult::Err(DoesNotOccur(p_0 | r_0, dep_2)), - }; - let (q_1, s_1) = match q_s.iter().collect_tuple() { - Some((q_1, s_1)) => (q_1, s_1), - None => return AnyOrderResult::Err(DoesNotOccur(q_0 | s_0, conclusion)), - }; - - let p_1 = p_1.clone(); - let q_1 = q_1.clone(); - let r_1 = r_1.clone(); - let s_1 = s_1.clone(); - - if p_0 != p_1 { - AnyOrderResult::Err(DoesNotOccur(p_0, p_1)) - } else if q_0 != q_1 { - AnyOrderResult::Err(DoesNotOccur(q_0, q_1)) - } else if r_0 != r_1 { - AnyOrderResult::Err(DoesNotOccur(r_0, r_1)) - } else if s_0 != s_1 { - AnyOrderResult::Err(DoesNotOccur(s_0, s_1)) - } else { - AnyOrderResult::Ok - } - } else { - AnyOrderResult::WrongOrder - } - }, - || OneOf(btreeset![DepDoesNotExist(Expr::impl_place_holder(), true), DepDoesNotExist(Expr::assocplaceholder(Op::Or), true),]), - ) - } - HalfDeMorgan => check_by_normalize_multiple_possibilities(proof, deps, conclusion, |e| e.normalize_halfdemorgans()), - QuantifierInference => check_by_normalize_first_expr_one_way(proof, deps, conclusion, |e| e.quantifier_inference()), + QuantifierNegation => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::negate_quantifiers, "none"), + NullQuantification => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::normalize_null_quantifiers, "none"), + ReplacingBoundVars => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::replacing_bound_vars, "none"), + SwappingQuantifiers => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::swap_quantifiers, "none"), + AristoteleanSquare => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::aristotelean_square, "none"), + QuantifierDistribution => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::quantifier_distribution, "none"), + PrenexLaws => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::normalize_prenex_laws, "none"), } } } -impl RuleT for AutomationRelatedRules { +impl RuleT for Special { fn get_name(&self) -> String { + use Special::*; match self { - AutomationRelatedRules::Resolution => "Resolution", - AutomationRelatedRules::TruthFunctionalConsequence => "Truth-Functional Consequence", + Reiteration => "Reiteration", + Resolution => "Resolution", + TruthFunctionalConsequence => "Truth-Functional Consequence", } .into() } fn get_classifications(&self) -> HashSet { - [RuleClassification::MiscInference].iter().cloned().collect() + [RuleClassification::Special].iter().cloned().collect() } fn num_deps(&self) -> Option { + use Special::*; match self { - AutomationRelatedRules::Resolution => Some(2), - AutomationRelatedRules::TruthFunctionalConsequence => None, + Reiteration => Some(1), + Resolution => Some(2), + TruthFunctionalConsequence => None, } } fn num_subdeps(&self) -> Option { + use Special::*; match self { - AutomationRelatedRules::Resolution | AutomationRelatedRules::TruthFunctionalConsequence => Some(0), + Reiteration | Resolution | TruthFunctionalConsequence => Some(0), } } fn check(self, p: &P, conclusion: Expr, deps: Vec>, _sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { + use crate::rules::ProofCheckError::DoesNotOccur; + use Special::*; match self { - AutomationRelatedRules::Resolution => { + Reiteration => { + let prem = p.lookup_expr_or_die(&deps[0])?; + if prem == conclusion { + Ok(()) + } else { + Err(DoesNotOccur(conclusion, prem)) + } + } + Resolution => { let prem0 = p.lookup_expr_or_die(&deps[0])?; let prem1 = p.lookup_expr_or_die(&deps[1])?; let mut premise_disjuncts = HashSet::new(); @@ -1492,8 +1968,14 @@ impl RuleT for AutomationRelatedRules { premise_disjuncts.extend(prem1.disjuncts()); let conclusion_disjuncts = conclusion.disjuncts().into_iter().collect::>(); let mut remainder = premise_disjuncts.difference(&conclusion_disjuncts).cloned().collect::>(); - //println!("resolution remainder of {:?} and {:?} is {:?}", premise_disjuncts, conclusion_disjuncts, remainder); remainder.sort(); + + // Ensure conclusion terms are in premises + if !conclusion_disjuncts.is_subset(&premise_disjuncts) { + return Err(ProofCheckError::Other(format!("Conclusion contains terms that are not in the premises: {:?}", conclusion_disjuncts.difference(&premise_disjuncts).collect::>()))); + } + + // Ensure remainder forms a contradiction match &remainder[..] { [e1, e2] => do_expressions_contradict::

(e1, e2), _ => { @@ -1506,7 +1988,7 @@ impl RuleT for AutomationRelatedRules { } } } - AutomationRelatedRules::TruthFunctionalConsequence => { + TruthFunctionalConsequence => { // Closure for making CNF conversion errors let cnf_error = || ProofCheckError::Other("Failed converting to CNF; the propositions for this rule should not use quantifiers, arithmetic, or application.".to_string()); @@ -1553,43 +2035,6 @@ impl RuleT for AutomationRelatedRules { } } -impl RuleT for QuantifierEquivalence { - fn get_name(&self) -> String { - use QuantifierEquivalence::*; - match self { - QuantifierNegation => "Quantifier Negation", - NullQuantification => "Null Quantification", - ReplacingBoundVars => "Replacing Bound Variables", - SwappingQuantifiers => "Swapping Quantifiers of Same Type", - AristoteleanSquare => "Aristotelean Square of Opposition", - QuantifierDistribution => "Quantifier Distribution", - PrenexLaws => "Prenex Laws", - } - .into() - } - fn get_classifications(&self) -> HashSet { - [RuleClassification::QuantifierEquivalence].iter().cloned().collect() - } - fn num_deps(&self) -> Option { - Some(1) - } // all equivalence rules rewrite a single statement - fn num_subdeps(&self) -> Option { - Some(0) - } - fn check(self, p: &P, conclusion: Expr, deps: Vec>, _sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { - use QuantifierEquivalence::*; - match self { - QuantifierNegation => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::negate_quantifiers, "none"), - NullQuantification => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::normalize_null_quantifiers, "none"), - ReplacingBoundVars => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::replacing_bound_vars, "none"), - SwappingQuantifiers => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::swap_quantifiers, "none"), - AristoteleanSquare => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::aristotelean_square, "none"), - QuantifierDistribution => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::quantifier_distribution, "none"), - PrenexLaws => check_by_normalize_first_expr(p, deps, conclusion, false, Expr::normalize_prenex_laws, "none"), - } - } -} - impl RuleT for Induction { fn get_name(&self) -> String { match self { @@ -1600,7 +2045,7 @@ impl RuleT for Induction { } fn get_classifications(&self) -> HashSet { - hashset![RuleClassification::MiscInference] + [RuleClassification::Induction].iter().cloned().collect() } fn num_deps(&self) -> Option { @@ -1618,7 +2063,7 @@ impl RuleT for Induction { // Check conclusion let (quantified_var, property) = match &conclusion { Expr::Quant { kind: QuantKind::Forall, name, body } => (name, &**body), - _ => return Err(ProofCheckError::ConclusionOfWrongForm(Expr::quant_placeholder(QuantKind::Forall))), + _ => return Err(ProofCheckError::ConclusionOfWrongForm(Expr::quant_place_holder(QuantKind::Forall))), }; match self { @@ -1639,7 +2084,7 @@ impl RuleT for Induction { let (induction_var, induction_impl) = if let Expr::Quant { kind: QuantKind::Forall, name, body } = inductive_case { (name, &**body) } else { - return AnyOrderResult::Err(ProofCheckError::DepOfWrongForm(inductive_case.clone(), Expr::quant_placeholder(QuantKind::Forall))); + return AnyOrderResult::Err(ProofCheckError::DepOfWrongForm(inductive_case.clone(), Expr::quant_place_holder(QuantKind::Forall))); }; if crate::expr::free_vars(&conclusion).contains(induction_var) { return AnyOrderResult::Err(ProofCheckError::Other(format!("Induction variable '{induction_var}' is a free variable in the conclusion"))); @@ -1667,7 +2112,7 @@ impl RuleT for Induction { // ---- // ∀ quantified_var, property(quantified_var) let prem = p.lookup_expr_or_die(&deps[0])?; - let (n, e) = if let Expr::Quant { kind: QuantKind::Forall, name, body } = prem { (name, *body) } else { return Err(ProofCheckError::DepOfWrongForm(prem, Expr::quant_placeholder(QuantKind::Forall))) }; + let (n, e) = if let Expr::Quant { kind: QuantKind::Forall, name, body } = prem { (name, *body) } else { return Err(ProofCheckError::DepOfWrongForm(prem, Expr::quant_place_holder(QuantKind::Forall))) }; let (e, property_n) = if let Expr::Impl { left, right } = e { (*left, *right) } else { return Err(ProofCheckError::DepOfWrongForm(e, Expr::impl_place_holder())) }; if crate::expr::free_vars(&conclusion).contains(&n) { return Err(ProofCheckError::Other(format!("Variable '{n}' is free in '{conclusion}'"))); @@ -1676,7 +2121,7 @@ impl RuleT for Induction { if property_n != expected_property_n { return Err(ProofCheckError::DepOfWrongForm(property_n, expected_property_n)); } - let (x, e) = if let Expr::Quant { kind: QuantKind::Forall, name, body } = e { (name, *body) } else { return Err(ProofCheckError::DepOfWrongForm(e, Expr::quant_placeholder(QuantKind::Forall))) }; + let (x, e) = if let Expr::Quant { kind: QuantKind::Forall, name, body } = e { (name, *body) } else { return Err(ProofCheckError::DepOfWrongForm(e, Expr::quant_place_holder(QuantKind::Forall))) }; let (x_lt_n, property_x) = if let Expr::Impl { left, right } = e { (*left, *right) } else { diff --git a/bindings/java/src/java_rule.rs b/bindings/java/src/java_rule.rs index f112cc22..1efb51c3 100644 --- a/bindings/java/src/java_rule.rs +++ b/bindings/java/src/java_rule.rs @@ -67,11 +67,16 @@ pub extern "system" fn Java_edu_rpi_aris_rules_Rule_getRuleType(env: JNIEnv, obj let ty = match classification { Introduction => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("INTRO")?])?, Elimination => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("ELIM")?])?, - BooleanEquivalence => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("BOOL_EQUIVALENCE")?])?, + BooleanInference => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("BOOLEAN_INFERENCE")?])?, + ConditionalInference => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("CONDITIONAL_INFERENCE")?])?, + BiconditionalInference => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("BICONDITIONAL_INFERENCE")?])?, + QuantifierInference => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("QUANTIFIER_INFERENCE")?])?, + BooleanEquivalence => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("BOOLEAN_EQUIVALENCE")?])?, ConditionalEquivalence => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("CONDITIONAL_EQUIVALENCE")?])?, BiconditionalEquivalence => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("BICONDITIONAL_EQUIVALENCE")?])?, QuantifierEquivalence => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("QUANTIFIER_EQUIVALENCE")?])?, - MiscInference => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("MISC_INFERENCE")?])?, + Special => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("SPECIAL")?])?, + Induction => env.call_static_method("java/lang/Enum", "valueOf", "(Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;", &[cls, jv("INDUCTION")?])?, }; env.set_object_array_element(types, i as _, ty.l()?)?; } diff --git a/web-app/src/components/proof_widget/mod.rs b/web-app/src/components/proof_widget/mod.rs index 3aea749d..dfb719c8 100644 --- a/web-app/src/components/proof_widget/mod.rs +++ b/web-app/src/components/proof_widget/mod.rs @@ -168,42 +168,46 @@ impl ProofWidget { fn render_rules_menu(&self, ctx: &Context, jref:

::JustificationReference, cur_rule_name: &str) -> Html { let equivalence_classes = [RuleClassification::BooleanEquivalence, RuleClassification::ConditionalEquivalence, RuleClassification::BiconditionalEquivalence, RuleClassification::QuantifierEquivalence]; - let render_rules = |rules: Vec| { - rules - .into_iter() - .map(|rule| { - let pjref = Coproduct::inject(jref); - let image_src = format!("{}/{}.png", if theme() == "dark" { "proofImages_dark" } else { "proofImages_light" }, rule.get_name()); - html! { - - } - }) - .collect::>() + let misc_inference_classes = [RuleClassification::BooleanInference, RuleClassification::ConditionalInference, RuleClassification::BiconditionalInference, RuleClassification::QuantifierInference]; + + let special_rule_names = ["Reiteration", "Resolution", "Truth-Functional Consequence"]; + + let render_rule_button = |rule: Rule| { + let pjref = Coproduct::inject(jref); + let image_src = format!("{}/{}.png", if theme() == "dark" { "proofImages_dark" } else { "proofImages_light" }, rule.get_name()); + html! { + + } }; - let render_class = |rule_class: RuleClassification| { - let rules = render_rules(rule_class.rules().collect()); + let render_rules_from_class = |class: RuleClassification| { html! {

-
{ rules }
+
+ { for class.rules().map(render_rule_button) } +
} }; - let equivalence_submenu = equivalence_classes.iter().map(|&class| render_class(class)).collect::>(); - let non_equivalence_menu = RuleClassification::iter().filter(|class| !equivalence_classes.contains(class)).map(render_class).collect::>(); + let special_rules = RuleClassification::iter().flat_map(|c| c.rules()).filter(|r| special_rule_names.contains(&r.get_name().as_str())).map(render_rule_button); + + let induction_category = RuleClassification::iter().find(|c| c.to_string() == "Induction").map(render_rules_from_class); + + let misc_inference_submenu = misc_inference_classes.iter().map(|&c| render_rules_from_class(c)); + + let equivalence_submenu = equivalence_classes.iter().map(|&c| render_rules_from_class(c)); + + let other_menus = RuleClassification::iter().filter(|c| !special_rule_names.contains(&c.to_string().as_str()) && c.to_string() != "Induction" && !equivalence_classes.contains(c) && !misc_inference_classes.contains(c) && c.to_string() != "Special").map(render_rules_from_class); html! {
@@ -211,11 +215,17 @@ impl ProofWidget { { cur_rule_name }
- { non_equivalence_menu } + { for other_menus } +
+ +
{ for misc_inference_submenu }
+
-
{ equivalence_submenu }
+
{ for equivalence_submenu }
+ { for special_rules } + { induction_category.unwrap_or_else(|| html! {}) }
} diff --git a/web-app/static/proofImages_dark/Biconditional Elimination Negation.png b/web-app/static/proofImages_dark/Biconditional Elimination Negation.png new file mode 100644 index 00000000..00fbbd20 Binary files /dev/null and b/web-app/static/proofImages_dark/Biconditional Elimination Negation.png differ diff --git a/web-app/static/proofImages_dark/Biconditional Elimination.png b/web-app/static/proofImages_dark/Biconditional Elimination.png new file mode 100644 index 00000000..b8d411f4 Binary files /dev/null and b/web-app/static/proofImages_dark/Biconditional Elimination.png differ diff --git a/web-app/static/proofImages_dark/Biconditional Introduction Negation.png b/web-app/static/proofImages_dark/Biconditional Introduction Negation.png new file mode 100644 index 00000000..26c24810 Binary files /dev/null and b/web-app/static/proofImages_dark/Biconditional Introduction Negation.png differ diff --git a/web-app/static/proofImages_dark/Biconditional Introduction.png b/web-app/static/proofImages_dark/Biconditional Introduction.png new file mode 100644 index 00000000..fc6f16e2 Binary files /dev/null and b/web-app/static/proofImages_dark/Biconditional Introduction.png differ diff --git a/web-app/static/proofImages_dark/Conditional Elimination Negation.png b/web-app/static/proofImages_dark/Conditional Elimination Negation.png new file mode 100644 index 00000000..a353e1a3 Binary files /dev/null and b/web-app/static/proofImages_dark/Conditional Elimination Negation.png differ diff --git a/web-app/static/proofImages_dark/Conditional Introduction Negation.png b/web-app/static/proofImages_dark/Conditional Introduction Negation.png new file mode 100644 index 00000000..c7e3a1a3 Binary files /dev/null and b/web-app/static/proofImages_dark/Conditional Introduction Negation.png differ diff --git a/web-app/static/proofImages_dark/Destructive Dilemma.png b/web-app/static/proofImages_dark/Destructive Dilemma.png new file mode 100644 index 00000000..dad2d1d7 Binary files /dev/null and b/web-app/static/proofImages_dark/Destructive Dilemma.png differ diff --git a/web-app/static/proofImages_dark/Disjunctive Syllogism.png b/web-app/static/proofImages_dark/Disjunctive Syllogism.png index 58533cc3..140109b6 100644 Binary files a/web-app/static/proofImages_dark/Disjunctive Syllogism.png and b/web-app/static/proofImages_dark/Disjunctive Syllogism.png differ diff --git a/web-app/static/proofImages_dark/Exclusion.png b/web-app/static/proofImages_dark/Exclusion.png new file mode 100644 index 00000000..8b10251c Binary files /dev/null and b/web-app/static/proofImages_dark/Exclusion.png differ diff --git a/web-app/static/proofImages_dark/Modus Tollens.png b/web-app/static/proofImages_dark/Modus Tollens.png index a8680c6e..bb9e37f3 100644 Binary files a/web-app/static/proofImages_dark/Modus Tollens.png and b/web-app/static/proofImages_dark/Modus Tollens.png differ diff --git a/web-app/static/proofImages_dark/Strengthening the Antecedent.png b/web-app/static/proofImages_dark/Strengthening the Antecedent.png new file mode 100644 index 00000000..83857d51 Binary files /dev/null and b/web-app/static/proofImages_dark/Strengthening the Antecedent.png differ diff --git a/web-app/static/proofImages_dark/Weakening the Consequent.png b/web-app/static/proofImages_dark/Weakening the Consequent.png new file mode 100644 index 00000000..a5395cfa Binary files /dev/null and b/web-app/static/proofImages_dark/Weakening the Consequent.png differ diff --git a/web-app/static/proofImages_light/Biconditional Elimination Negation.png b/web-app/static/proofImages_light/Biconditional Elimination Negation.png new file mode 100644 index 00000000..e81dcb93 Binary files /dev/null and b/web-app/static/proofImages_light/Biconditional Elimination Negation.png differ diff --git a/web-app/static/proofImages_light/Biconditional Elimination.png b/web-app/static/proofImages_light/Biconditional Elimination.png new file mode 100644 index 00000000..fdb64d97 Binary files /dev/null and b/web-app/static/proofImages_light/Biconditional Elimination.png differ diff --git a/web-app/static/proofImages_light/Biconditional Introduction Negation.png b/web-app/static/proofImages_light/Biconditional Introduction Negation.png new file mode 100644 index 00000000..fca79c16 Binary files /dev/null and b/web-app/static/proofImages_light/Biconditional Introduction Negation.png differ diff --git a/web-app/static/proofImages_light/Biconditional Introduction.png b/web-app/static/proofImages_light/Biconditional Introduction.png new file mode 100644 index 00000000..13f20a3b Binary files /dev/null and b/web-app/static/proofImages_light/Biconditional Introduction.png differ diff --git a/web-app/static/proofImages_light/Conditional Elimination Negation.png b/web-app/static/proofImages_light/Conditional Elimination Negation.png new file mode 100644 index 00000000..cd631773 Binary files /dev/null and b/web-app/static/proofImages_light/Conditional Elimination Negation.png differ diff --git a/web-app/static/proofImages_light/Conditional Introduction Negation.png b/web-app/static/proofImages_light/Conditional Introduction Negation.png new file mode 100644 index 00000000..1b4e743a Binary files /dev/null and b/web-app/static/proofImages_light/Conditional Introduction Negation.png differ diff --git a/web-app/static/proofImages_light/Destructive Dilemma.png b/web-app/static/proofImages_light/Destructive Dilemma.png new file mode 100644 index 00000000..6b09681d Binary files /dev/null and b/web-app/static/proofImages_light/Destructive Dilemma.png differ diff --git a/web-app/static/proofImages_light/Disjunctive Syllogism.png b/web-app/static/proofImages_light/Disjunctive Syllogism.png index 83414494..9d322dc3 100644 Binary files a/web-app/static/proofImages_light/Disjunctive Syllogism.png and b/web-app/static/proofImages_light/Disjunctive Syllogism.png differ diff --git a/web-app/static/proofImages_light/Exclusion.png b/web-app/static/proofImages_light/Exclusion.png new file mode 100644 index 00000000..b082c6de Binary files /dev/null and b/web-app/static/proofImages_light/Exclusion.png differ diff --git a/web-app/static/proofImages_light/Modus Tollens.png b/web-app/static/proofImages_light/Modus Tollens.png index a01cf582..161c0e06 100644 Binary files a/web-app/static/proofImages_light/Modus Tollens.png and b/web-app/static/proofImages_light/Modus Tollens.png differ diff --git a/web-app/static/proofImages_light/Strengthening the Antecedent.png b/web-app/static/proofImages_light/Strengthening the Antecedent.png new file mode 100644 index 00000000..b8a7511c Binary files /dev/null and b/web-app/static/proofImages_light/Strengthening the Antecedent.png differ diff --git a/web-app/static/proofImages_light/Weakening the Consequent.png b/web-app/static/proofImages_light/Weakening the Consequent.png new file mode 100644 index 00000000..f01f8ea1 Binary files /dev/null and b/web-app/static/proofImages_light/Weakening the Consequent.png differ