LP (the Larch Prover), Release 3.1a (95/04/27) logging to `/pro/oodb/specs/KOLA98/cnf-scripts.lplog' on 21 June 1998 18:38:12. LP0.1.2: LP0.1.3: % ****************************************************************************** LP0.1.4: % * * LP0.1.5: % * Script File: SIGMOD98_Scripts * LP0.1.6: % * -------------------------------------------------------------------------- * LP0.1.7: % * Scripts Author: Mitch Cherniack (mfc@cs.brandeis.edu) * LP0.1.8: % * Date: June, 1998 * LP0.1.9: % * * LP0.1.10: % * Present Address: Computer Science Department * LP0.1.11: % * Brandeis University * LP0.1.12: % * Waltham, MA 02254 * LP0.1.13: % * -------------------------------------------------------------------------- * LP0.1.14: % * * LP0.1.15: % * Proof Scripts Establishing Correctness of Rewrite Rules used in the paper, * LP0.1.16: % * [CZ98a]: * LP0.1.17: % * * LP0.1.18: % * [CZ98a] Changing the Rules: Transformations for Rule-Based Optimizers * LP0.1.19: % * Mitch Cherniack and Stan Zdonik, In Proceedings of the 1998 ACM * LP0.1.20: % * SIGMOD International Conference on Management of Data, Seattle, * LP0.1.21: % * WA, June, 1998. * LP0.1.22: % * * LP0.1.23: % * For an up-to-date version of [CZ98a], see: * LP0.1.24: % * ftp://wilma.cs.brown.edu/u/mfc/sigmod98.ps.Z * LP0.1.25: % * * LP0.1.26: % * * LP0.1.27: % * Instructions: * LP0.1.28: % * * LP0.1.29: % * Requires Version 3.1a of the LP Theorem Prover, available from * LP0.1.30: % * MIT, Laboratory of Computer Science. For software and documentation on * LP0.1.31: % * LP see: * LP0.1.32: % * * LP0.1.33: % * http://www.sds.lcs.mit.edu/spd/larch/LP/overview.html * LP0.1.34: % * * LP0.1.35: % * With LP installed in $path, run this theorem prover script by typing * LP0.1.36: % * * LP0.1.37: % * $path/lp -c SIGMOD98_Scripts * LP0.1.38: % * * LP0.1.39: % ****************************************************************************** LP0.1.40: LP0.1.41: % Section 1: CNF LP0.1.42: % LP0.1.43: % Proof Scripts for COKO Transformations, LP0.1.44: % LP0.1.45: % TRANSFORMATION CNFNE LP0.1.46: % USES LP0.1.47: % CNFAux LP0.1.48: % BEGIN LP0.1.49: % BU {CNFAux} LP0.1.50: % END LP0.1.51: % LP0.1.52: % TRANSFORMATION CNFAux LP0.1.53: % USES LP0.1.54: % dist1: p | (q & r) --> (p | q) & (p | r), LP0.1.55: % dist2: (p & q) | r --> (p | r) & (q | r) LP0.1.56: % BEGIN LP0.1.57: % {dist1 || dist2} -> LP0.1.58: % GIVEN p & q DO {CNFAux (p); CNFAux (q)} LP0.1.59: % END LP0.1.60: % LP0.1.61: % TRANSFORMATION CNF LP0.1.62: % USES LP0.1.63: % CNFNE, LP0.1.64: % involution: ~ (~ (p)) --> p, LP0.1.65: % deMorgan1: ~ (p & q) --> ~ (p) | ~ (q), LP0.1.66: % deMorgan2: ~ (p | q) --> ~ (p) & ~ (q) LP0.1.67: % BEGIN LP0.1.68: % TD {involution || deMorgan1 || deMorgan2}; LP0.1.69: % BU {involution}; LP0.1.70: % CNFNE LP0.1.71: % END LP0.1.72: % LP0.1.73: % In [CZ98a], CNFNE is called CNF, and CNF (above) is not LP0.1.74: % described. LP0.1.75: LP0.1.76: clear LP0.1.77: set order manual The ordering-method is now `manual'. LP0.1.78: exec-silently CNF_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/CNF_Aux_Axioms.lp'. LP0.1.79: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.80: order formulas The system now contains 5 rewrite rules. The rewriting system is guaranteed to terminate. All equations have been oriented into rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.81: make immune formulas LP0.1.82: LP0.1.83: declare variables p, q, r: pred [T] .. LP0.1.84: LP0.1.85: LP0.1.86: % L1: Rules Used in CNFAux LP0.1.87: % ------------------------ LP0.1.88: LP0.1.89: set name dist1 The name-prefix is now `dist1'. LP0.1.90: prove (p & q) | r = (p | r) & (q | r) Attempting to prove conjecture dist1.1: (p & q) | r = (p | r) & (q | r) Suspending proof of conjecture dist1.1 LP0.1.91: LP0.1.92: resume by <=> Creating subgoals for proof of <=> New constants: pc, xc, rc, qc => hypothesis: dist1ImpliesHyp.1: (pc ? xc \/ rc ? xc) /\ (qc ? xc \/ rc ? xc) => subgoal: (pc ? xc /\ qc ? xc) \/ rc ? xc <= hypothesis: dist1ImpliesHyp.2: (pc ? xc /\ qc ? xc) \/ rc ? xc <= subgoal: (pc ? xc \/ rc ? xc) /\ (qc ? xc \/ rc ? xc) Attempting to prove level 2 subgoal 1 for proof of <=> Added hypothesis dist1ImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula dist1ImpliesHyp.1 to yield the following formulas, which imply dist1ImpliesHyp.1. dist1ImpliesHyp.1.1: pc ? xc \/ rc ? xc dist1ImpliesHyp.1.2: qc ? xc \/ rc ? xc The system now contains 7 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 2 subgoal 1 for proof of <=> LP0.1.93: LP0.1.94: % => LP0.1.95: resume by cases (rc ? xc) Creating subgoals for proof by cases Case hypotheses: dist1CaseHyp.1.1: rc ? xc dist1CaseHyp.1.2: ~(rc ? xc) Same subgoal for all cases: (pc ? xc /\ qc ? xc) \/ rc ? xc Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis dist1CaseHyp.1.1 to the system. Level 3 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis dist1CaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal 1 for proof of <=> [] Proved by cases rc ? xc. Attempting to prove level 2 subgoal 2 for proof of <=> Added hypothesis dist1ImpliesHyp.2 to the system. The system now contains 6 rewrite rules. The rewriting system is guaranteed to terminate. Suspending proof of level 2 subgoal 2 for proof of <=>: (pc ? xc \/ rc ? xc) /\ (qc ? xc \/ rc ? xc) LP0.1.96: LP0.1.97: % <= LP0.1.98: resume by cases (rc ? xc) Creating subgoals for proof by cases Case hypotheses: dist1CaseHyp.1.1: rc ? xc dist1CaseHyp.1.2: ~(rc ? xc) Same subgoal for all cases: (pc ? xc \/ rc ? xc) /\ (qc ? xc \/ rc ? xc) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis dist1CaseHyp.1.1 to the system. Level 3 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis dist1CaseHyp.1.2 to the system. Deduction rule lp_and_is_true has been applied to formula dist1ImpliesHyp.2 to yield the following formulas, which imply dist1ImpliesHyp.2. dist1ImpliesHyp.2.1: pc ? xc dist1ImpliesHyp.2.2: qc ? xc Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal 2 for proof of <=> [] Proved by cases rc ? xc. Conjecture dist1.1: (p & q) | r = (p | r) & (q | r) [] Proved <=>. LP0.1.99: LP0.1.100: qed All conjectures have been proved. LP0.1.101: LP0.1.102: set name dist2 The name-prefix is now `dist2'. LP0.1.103: prove r | (p & q) = (p | r) & (q | r) Attempting to prove conjecture dist2.1: r | (p & q) = (p | r) & (q | r) Conjecture dist2.1 [] Proved by normalization. Deleted formula dist2.1, which reduced to `true'. LP0.1.104: qed All conjectures have been proved. LP0.1.105: LP0.1.106: LP0.1.107: % L1: Rules Used in CNF LP0.1.108: % --------------------- LP0.1.109: LP0.1.110: set name involution The name-prefix is now `involution'. LP0.1.111: prove ~ (~ (p)) = p Attempting to prove conjecture involution.1: ~ ~p = p Conjecture involution.1 [] Proved by normalization. Deleted formula involution.1, which reduced to `true'. LP0.1.112: qed All conjectures have been proved. LP0.1.113: LP0.1.114: set name deMorgan1 The name-prefix is now `deMorgan1'. LP0.1.115: prove ~ (p & q) = (~ (p)) | (~ (q)) Attempting to prove conjecture deMorgan1.1: ~(p & q) = (~p) | (~q) Suspending proof of conjecture deMorgan1.1 LP0.1.116: LP0.1.117: resume by <=> Creating subgoals for proof of <=> New constants: pc, xc, qc => hypothesis: deMorgan1ImpliesHyp.1: ~(pc ? xc) \/ ~(qc ? xc) => subgoal: ~(pc ? xc /\ qc ? xc) <= hypothesis: deMorgan1ImpliesHyp.2: ~(pc ? xc /\ qc ? xc) <= subgoal: ~(pc ? xc) \/ ~(qc ? xc) Attempting to prove level 2 subgoal 1 for proof of <=> Added hypothesis deMorgan1ImpliesHyp.1 to the system. The system now contains 7 rewrite rules. The rewriting system is NOT guaranteed to terminate. Suspending proof of level 2 subgoal 1 for proof of <=> LP0.1.118: LP0.1.119: % => LP0.1.120: resume by cases ~ (pc ? xc) Creating subgoals for proof by cases Case hypotheses: deMorgan1CaseHyp.1.1: ~(pc ? xc) deMorgan1CaseHyp.1.2: ~(~(pc ? xc)) Same subgoal for all cases: ~(pc ? xc /\ qc ? xc) Attempting to prove level 3 subgoal for case 1 (out of 2) Added hypothesis deMorgan1CaseHyp.1.1 to the system. Level 3 subgoal for case 1 (out of 2) [] Proved by normalization. Attempting to prove level 3 subgoal for case 2 (out of 2) Added hypothesis deMorgan1CaseHyp.1.2 to the system. Level 3 subgoal for case 2 (out of 2) [] Proved by normalization. Level 2 subgoal 1 for proof of <=> [] Proved by cases ~(pc ? xc). Attempting to prove level 2 subgoal 2 for proof of <=> Added hypothesis deMorgan1ImpliesHyp.2 to the system. Suspending proof of level 2 subgoal 2 for proof of <=> LP0.1.121: LP0.1.122: % <= LP0.1.123: resume by contradiction Creating subgoals for proof by contradiction Hypothesis: deMorgan1ContraHyp.1: ~(~(pc ? xc) \/ ~(qc ? xc)) Only subgoal: false Attempting to prove level 3 subgoal for proof by contradiction Added hypothesis deMorgan1ContraHyp.1 to the system. Deduction rule lp_or_is_false has been applied to formula deMorgan1ContraHyp.1 to yield the following formulas, which imply deMorgan1ContraHyp.1. deMorgan1ContraHyp.1.1: ~(~(pc ? xc)) deMorgan1ContraHyp.1.2: ~(~(qc ? xc)) Formula deMorgan1ImpliesHyp.2, false, is inconsistent. Level 3 subgoal for proof by contradiction [] Proved by detecting an inconsistency. Level 2 subgoal 2 for proof of <=>: ~(pc ? xc) \/ ~(qc ? xc) [] Proved by contradiction. Conjecture deMorgan1.1: ~(p & q) = (~p) | (~q) [] Proved <=>. LP0.1.124: LP0.1.125: qed All conjectures have been proved. LP0.1.126: LP0.1.127: set name deMorgan2 The name-prefix is now `deMorgan2'. LP0.1.128: prove ~ (p | q) = (~ (p)) & (~ (q)) Attempting to prove conjecture deMorgan2.1: ~(p | q) = (~p) & (~q) Suspending proof of conjecture deMorgan2.1 LP0.1.129: resume by <=> Creating subgoals for proof of <=> New constants: pc, xc, qc => hypothesis: deMorgan2ImpliesHyp.1: ~(pc ? xc) /\ ~(qc ? xc) => subgoal: ~(pc ? xc \/ qc ? xc) <= hypothesis: deMorgan2ImpliesHyp.2: ~(pc ? xc \/ qc ? xc) <= subgoal: ~(pc ? xc) /\ ~(qc ? xc) Attempting to prove level 2 subgoal 1 for proof of <=> Added hypothesis deMorgan2ImpliesHyp.1 to the system. Deduction rule lp_and_is_true has been applied to formula deMorgan2ImpliesHyp.1 to yield the following formulas, which imply deMorgan2ImpliesHyp.1. deMorgan2ImpliesHyp.1.1: ~(pc ? xc) deMorgan2ImpliesHyp.1.2: ~(qc ? xc) Level 2 subgoal 1 for proof of <=> [] Proved by normalization. Attempting to prove level 2 subgoal 2 for proof of <=> Added hypothesis deMorgan2ImpliesHyp.2 to the system. Deduction rule lp_or_is_false has been applied to formula deMorgan2ImpliesHyp.2 to yield the following formulas, which imply deMorgan2ImpliesHyp.2. deMorgan2ImpliesHyp.2.1: ~(pc ? xc) deMorgan2ImpliesHyp.2.2: ~(qc ? xc) Level 2 subgoal 2 for proof of <=> [] Proved by normalization. Conjecture deMorgan2.1 [] Proved <=>. The system now contains 8 rewrite rules. The rewriting system is NOT guaranteed to terminate. LP0.1.130: qed All conjectures have been proved. LP0.1.131: LP0.1.132: quit End of input from file `/pro/oodb/specs/KOLA98/cnf-scripts.lp'. End of input from file `command line arguments'.