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'.