Terminology note: Zeman's orignally coined term was "semisubstitutivity", which I find difficult to pronounce, and therefore to type. I personally prefer "semi-substitivity".

The best example of the use of semi-substitivity is the Rezus single axiom for BCIW logic. Since I used this as an example in a letter to the Association for Automated Reasoning (AAR) newsletter, I'm just going to repeat the original version of that letter here. (The editor found it too long, and an edited version was produced, referencing the text here for more detail.)

I was holed up on vacation in Hamilton, Montana having an uneventful time biking and hiking during the day, and working on J. J. Zeman's semisubstitutivity in the evenings. I had just gone on record telling a few people that, while it was a very interesting topic, semi-substitivity really didn't have any practical use in automated theorem proving.

Then, what to my wondering eyes should appear but the June AAR newsletter. And in it Larry Wos gave a challenge that proved me wrong. In the column, Larry posed a two part challenge, the one part being to generate a computer proof that the Rezus single axiom for BCIW logic was a theorem of BCIW. [The problem being that it is huge, and that causes problems for many automated theorem provers.] The other part of the challenge, in typical Larry Wos style, was to show a general method of proving such complex expressions from simple axioms.

I think that it should be noted that Dr. Bob Veroff, Dr. Larry Wos, and probably others have already published computer proofs that the Rezus axiom is a theorem of BCIW, so my just having such a proof is nothing particularly new or interesting. And, in fact, hand generated proofs existed long before the computer generated ones.

I have, however, enclosed with my proof a new technique for attacking large expressions of this sort. And I have enclosed both a "native" semi-substitivity proof that was generated using this technique, and that proof reduced to a more traditional Condensed Detachment proof. My technique is not the general method asked for, but it is a novel (and extremely effective in this case) technique for attacking large expressions. The new technique produces a semi-substitivity proof of the expression given, and that proof can be easily (mechanically) converted to a more traditional proof.

Just using semisubstitivity as the inference rule isn't actually particularly interesting. Semi-substitivity has MUCH worse fanout at any given step than a standard Condensed Detachment, or a typical Modus Ponens and Uniform Substitution proof. Without some trick to reduce the search space it would be a much worse approach than the traditional methods.

So, I hear you think, "What is the trick here?".

I'm afraid that the trick does depend on semi-substitivity, which is probably unfamiliar to most of the readers of the newsletter. I refer you to my web page on the topic for a quick introduction:

http://www.cc.utah.edu/~nahaj/logic/concepts/semi/index.html

The short explaination is that if one had something of the form (p > q) and
of the form (q > p) in most reasonable logics, one would have license to
replace p by q, or q by p, anywhere in any theorem [Substitution of
equivalents] without compromising validity. A subtly obvious question is
whether having *JUST* the conditional (p > q), instead of the bi-conditional
equivalence, buys you anything. The surprising answer is yes. **For logics**
such as BCIW, **with just implication** and no other operators, it buys you
something very clean. In BCIW, for example, if you have (p > q), there are
positions in any expression where p (if it exists) can be replaced by q without
compromising validity. This surprising fact is joined by the less obvious and
more surprising fact that in all other positions in the expression q (if it
exists) can be replaced by p. [Proofs on the web page.]

So semi-substitivity licenses you to do strategic surgery inside of theorems, which makes dealing with large expressions somewhat more tractable. But the problem of doing mechanical search with it is as bad, or worse, than with traditional methods.

OK, we now have enough tedious background to explain the actual trick.

Given a theorem of the form (p > q) and an alleged theorem that you are
working on, semi-substitivity licenses either (depending on the position in the
theorem) replacement of p by q, or of q by p, without compromising validity.
(This assumes that all the operators that dominate the position obey
semi-substivity, which is trivially true for BCIW since it has only one
operator, and it obeys the rule.)
But what can you say about replacements in the *opposite* direction than those
licensed replacements, other than that they do NOT necessarily preserve
validity? What CAN be said is that those replacements can be undone by a
validity preserving licensed replacement. So, *** **and here is the
trick** ***, any sequence of ONLY replacements in the **opposite** directon
of the licensed directions, from an given expression to a ***known
valid*** theorem (such as an axiom), can be run in the reverse (licensed)
direction to produce a validity preserving proof from the axiom to the original
starting point. And reduction of the given alleged theorem to an axiom can be
very very simple and clean.

The slickest example I'm aware of is the Rezus theorem that Larry offered: [I'm going to use polish notation here because infix notation of expressions of this large size is totally unreadable (at least to me).] The alleged theorem we want to prove is (in Polish Notation):

CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10CCCv11v12CCv12v13Cv11v13v14v14v15v15CCv16CCCv17v17CCv18v18CCv19v19CCv20v20Cv16v21v21v22v22

And to make the explanation readable, I'll first exhibit an annotated version of a graph of the expression. The annotation is:

Symbol #: direction licensed, position, graphic

positions are given as strings of "A"'s (for Antecedent) and "C"'s (for Consequent). So, for example, "CCA" means the Consequent of the Consequent of the Antecedent.

># : sym direction position diagram. 1: C + .- C | 2: C - A .- C | | 3: C + AA | .- C | | | 4: x - AAA | | .- x | | | 5: C + CAA | | .- C | | | 6: C - ACAA | | .- C | | | | 7: C + AACAA | | | .- C | | | | | 8: y - AAACAA | | | | .- y | | | | | 9: y + CAACAA | | | | .- y | | | | 10: C - CACAA | | | .- C | | | | 11: C + ACACAA | | | .- C | | | | | 12: z - AACACAA | | | | .- z | | | | | 13: z + CACACAA | | | | .- z | | | | 14: C - CCACAA | | | .- C | | | | 15: C + ACCACAA | | | .- C | | | | | 16: u - AACCACAA | | | | .- u | | | | | 17: u + CACCACAA | | | | .- u | | | | 18: C - CCCACAA | | | .- C | | | | 19: C + ACCCACAA | | | .- C | | | | | 20: v - AACCCACAA | | | | .- v | | | | | 21: v + CACCCACAA | | | | .- v | | | | 22: C - CCCCACAA | | | .- C | | | | 23: x + ACCCCACAA | | | .- x | | | | 24: w - CCCCCACAA | | | .- w | | | 25: w + CCAA | | .- w | | 26: C - CA | .- C | | 27: C + ACA | .- C | | | 28: C - AACA | | .- C | | | | 29: C + AAACA | | | .- C | | | | | 30: C - AAAACA | | | | .- C | | | | | | 31: v6 + AAAAACA | | | | | .- v6 | | | | | | 32: v7 - CAAAACA | | | | | .- v7 | | | | | 33: C + CAAACA | | | | .- C | | | | | 34: C - ACAAACA | | | | .- C | | | | | | 35: v7 + AACAAACA | | | | | .- v7 | | | | | | 36: v8 - CACAAACA | | | | | .- v8 | | | | | 37: C + CCAAACA | | | | .- C | | | | | 38: v6 - ACCAAACA | | | | .- v6 | | | | | 39: v8 + CCCAAACA | | | | .- v8 | | | | 40: C - CAACA | | | .- C | | | | 41: C + ACAACA | | | .- C | | | | | 42: C - AACAACA | | | | .- C | | | | | | 43: C + AAACAACA | | | | | .- C | | | | | | | 44: C - AAAACAACA | | | | | | .- C | | | | | | | | 45: v9 + AAAAACAACA | | | | | | | .- v9 | | | | | | | | 46: C - CAAAACAACA | | | | | | | .- C | | | | | | | | 47: v9 + ACAAAACAACA | | | | | | | .- v9 | | | | | | | | 48: v10 - CCAAAACAACA | | | | | | | .- v10 | | | | | | | 49: C + CAAACAACA | | | | | | .- C | | | | | | | 50: v9 - ACAAACAACA | | | | | | .- v9 | | | | | | | 51: v10 + CCAAACAACA | | | | | | .- v10 | | | | | | 52: C - CAACAACA | | | | | .- C | | | | | | 53: C + ACAACAACA | | | | | .- C | | | | | | | 54: C - AACAACAACA | | | | | | .- C | | | | | | | | 55: v11 + AAACAACAACA | | | | | | | .- v11 | | | | | | | | 56: v12 - CAACAACAACA | | | | | | | .- v12 | | | | | | | 57: C + CACAACAACA | | | | | | .- C | | | | | | | 58: C - ACACAACAACA | | | | | | .- C | | | | | | | | 59: v12 + AACACAACAACA | | | | | | | .- v12 | | | | | | | | 60: v13 - CACACAACAACA | | | | | | | .- v13 | | | | | | | 61: C + CCACAACAACA | | | | | | .- C | | | | | | | 62: v11 - ACCACAACAACA | | | | | | .- v11 | | | | | | | 63: v13 + CCCACAACAACA | | | | | | .- v13 | | | | | | 64: v14 - CCAACAACA | | | | | .- v14 | | | | | 65: v14 + CACAACA | | | | .- v14 | | | | 66: v15 - CCAACA | | | .- v15 | | | 67: v15 + CACA | | .- v15 | | 68: C - CCA | .- C | | 69: C + ACCA | .- C | | | 70: v16 - AACCA | | .- v16 | | | 71: C + CACCA | | .- C | | | 72: C - ACACCA | | .- C | | | | 73: C + AACACCA | | | .- C | | | | | 74: v17 - AAACACCA | | | | .- v17 | | | | | 75: v17 + CAACACCA | | | | .- v17 | | | | 76: C - CACACCA | | | .- C | | | | 77: C + ACACACCA | | | .- C | | | | | 78: v18 - AACACACCA | | | | .- v18 | | | | | 79: v18 + CACACACCA | | | | .- v18 | | | | 80: C - CCACACCA | | | .- C | | | | 81: C + ACCACACCA | | | .- C | | | | | 82: v19 - AACCACACCA | | | | .- v19 | | | | | 83: v19 + CACCACACCA | | | | .- v19 | | | | 84: C - CCCACACCA | | | .- C | | | | 85: C + ACCCACACCA | | | .- C | | | | | 86: v20 - AACCCACACCA | | | | .- v20 | | | | | 87: v20 + CACCCACACCA | | | | .- v20 | | | | 88: C - CCCCACACCA | | | .- C | | | | 89: v16 + ACCCCACACCA | | | .- v16 | | | | 90: v21 - CCCCCACACCA | | | .- v21 | | | 91: v21 + CCACCA | | .- v21 | | 92: v22 - CCCA | .- v22 | 93: v22 + C .- v22

The axioms of the system are:

- B: CCpqCCrpCrq
- C: CCpCqrCqCpr
- I: Cpp
- W: CCpCpqCpq

Or in possibly more familiar notation:

- B: (p > q) > ((r > p) > (r > q))
- C: (p > (q > r)) > (q > (p > r))
- I: p > p
- W: ( p > (p > q) ) > (p > q)

In order to avoid making this a truly ugly example, I'll introduce some
template lemmas^{1} to make this short
and sweet. And I'll work from the right to the left so that any
unprocessed part of the expression is still numbered as above, and I
don't have to reconstruct the diagram
above after each replacement.

The template lemmas are all of the form

(( {axiom or theorem} > s) > s)

Each is trivially (4 or less steps from the axioms) provable from the axioms:

B' simplify: CCCCpqCCqrCprss # Note that this is not based on B, it is # based on B'. I simplify: CCCppqq W simplify: CCCCpCpqCpqrr MP simplify: CCCpCCpqqrr

Scanning from the right to the left in the expression, the first place we match a template is at symbol 84, where we match I simplify. In this position the reverse (q replaced by p) is licensed, so the unlicensed (p replaced by q) will be used: [*** Since, oddly enough, All replacements in this proof occur at negative positions, I'm not going to keep repeating this part]

84: CCCppqq, p/v20, q/Cv16v21, applied at CCCACACCA CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10CCCv11v12CCv12v13Cv11v13v14v14v15v15CCv16CCCv17v17CCv18v18CCv19v19Cv16v21v21v22v22

Continuing our right to left scan, the next place we match a template is at symbol 80, where we match I simplify

80: CCCppqq, p/v19, q/Cv16v21, applied CCCACACCA CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10CCCv11v12CCv12v13Cv11v13v14v14v15v15CCv16CCCv17v17CCv18v18Cv16v21v21v22v22

And then we match at symbol 76 with I simplify

76: CCCppqq, p/v18, q/Cv16v21, applied at CACACCA CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10CCCv11v12CCv12v13Cv11v13v14v14v15v15CCv16CCCv17v17Cv16v21v21v22v22

At symbol 72 we match I simplify

72: CCCppqq, p/v17, q/Cv16v21, applied at ACACCA CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10CCCv11v12CCv12v13Cv11v13v14v14v15v15CCv16CCv16v21v21v22v22

At symbol 68 we match W simplify

68: CCCCpCpqCpqrr, p/v16, q/v21, r/v22, applied at CCA CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10CCCv11v12CCv12v13Cv11v13v14v14v15v15v22v22

At symbol 52 we match B' simplify

52: CCCCpqCCqrCprss, p/v11, q/v12, r/v13, s/v14 CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCCCCv9Cv9v10Cv9v10v14v14v15v15v22v22

At symbol 42 we match W simplify

42: CCCCpCpqCpqrr, p/v9, q/v10, r/v14, applied at AACAACA CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8CCv14v14v15v15v22v22

At symbol 40 we match I simplify

40: CCCppqq, p/v14, q/v15, applied at CAACA CCCxCCCyyCCzzCCuuCCvvCxwwCCCCCv6v7CCv7v8Cv6v8v15v15v22v22

At symbol 28 we match B' simplify

28: CCCCpqCCqrCprss, p/v6, q/v7, r/v8, s/v15, applied at AACA CCCxCCCyyCCzzCCuuCCvvCxwwCCv15v15v22v22

At symbol 26 we match I simplify

26: CCCppqq, p/v15, q/v22, applied at CA CCCxCCCyyCCzzCCuuCCvvCxwwv22v22

At symbol 18 we match I simplify

18: CCppqq, p/v q/Cxw, applied at CCCCACAA CCCxCCCyyCCzzCCuuCxwwv22v22

At symbol 14 we match I simplify

14: CCCppqq, p/u, q/Cxw, applied at CCACAA CCCxCCCyyCCzzCxwwv22v22

At symbol 10 we match I simplify

10: CCCppqq, p/z, q/Cxw, applied at CACAA CCCxCCCyyCxwwv22v22

At symbol 6 we match I simplify

6: CCCppqq, p/y, q/Cxw, applied at ACAA CCCxCCxwwv22v22

At symbol 3 we match MP simplify

3: CCCpCCpqqrr, p/x, q/w, r/v22, applied at AA Cv22v22

And this is just the axiom I.

1: Cv22v22, v22/p

Since the reduction, in only the directions opposite to the licenced directions has produced an axiom, we can now read off the proper (licensed direction) semi-substitivity proof of the theorem from the I axiom. (Just do the steps in the reverse order, reversing the substitutions.)

The only obvious hand wave I've done here was in choosing to use template lemmas and in the choice of which ones. (I originally had one for each of B, B', C, I, MP, and W, but just omitted the one that didn't get used.) In general, finding the reductions is generally not as clean as it is in Rezus style single axioms for systems, but I think this does give the rough idea. A process that would have worked to find the templates, and works a little more generally, is to collect all theorems a short distance from the axioms, and note whether or not they reduce in either the forward or reverse direction. Then walk the expression looking for instances of those that reduce in each position.

**ASIDE:** Few semi-substitivity proofs are likely to be this clean, but I
think this example does show that the technique has promise. In my playing
with the technique, it seems to have many properties of rewriting systems, but
with restrictions on where the rewrites can occur. I personally expect, but
have not pursued, that there is an analog of the Knuth-Bendix algorithm that
can be worked out for semi-substitivity. It might make an interesting project
for someone looking for something fun to play with.

For some odd reason :), theorem proving programs are usually not set up to handle semi-substitivity as a rule of inference. Fortunately these proof steps can be mechanically converted to a more traditional proof. The semi-substitivity transformations for a given position can be easily written (and the proof mechanically generated from the position, or one can allow a traditional theorem prover to prove them). The template lemmas are a trivial few steps away from the axioms, and substituting them into the semi-substitivity theorems is obviously trivial.

Doing the above in my theorem prover (shotgun) yields the traditional proof that follows: (The variable names are different, since my program canonicalizes variables in theorems in a slightly different manner than Larry's does... But the results are the same theorem...) Shotgun has done some optimizations on the proof in places where it saw a shortening of the direct translation of the above.

# ----------------- Proof: -------------------- # Produced Tue Jul 13 02:37:52 2010 # by the "shotgun" program, version 2010-01-07 0.01.007 # -- Rules -- # Condensed detachment for ">" # From |- p and |- Cpq, produce the most general possible |- q. # # --- Wish List --- =wishlist "CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1CCu1CCCv1v1CCw1w1CCx1x1CCy1y1Cu1z1z1p2p2" "BCIW REZUS" # --- Axioms --- 1: =axiom "CCpqCCrpCrq" "B" 2: =axiom "CCpCqrCqCpr" "C" 3: # Rezus 3 =axiom "Cpp" "I" 4: =axiom "CCpCpqCpq" "W" # --- Theorems --- # Modus Ponens 5: CpCCpqq # Condensed detachment, inference line 2 with line 3 # Rezus 6 6: CCCpCCpqqrr # Condensed detachment, inference line 5 with line 5 # I simplify 7: CCCppqq # Condensed detachment, inference line 5 with line 3 # B' 8: CCpqCCqrCpr # Condensed detachment, inference line 2 with line 1 9: CCCCpqCprsCCqrs # Condensed detachment, inference line 8 with line 1 # Semi - CA 10: CCpqCCCrqsCCrps # Condensed detachment, inference line 9 with line 8 11: CCCCpqCrqsCCrps # Condensed detachment, inference line 8 with line 8 # Semi - ACA 12: CCpqCCCrCpstCCrCqst # Condensed detachment, inference line 11 with line 10 13: CCpCqrCpCCrsCqs # Condensed detachment, inference line 1 with line 8 14: CCpqCCCCrCqstuCCCrCpstu # Condensed detachment, inference line 13 with line 12 15: CCCCpCqrstCCCpCCCuuqrst # Condensed detachment, inference line 14 with line 7 # Rezus 10 16: CCCpCCCqqCprrss # Condensed detachment, inference line 15 with line 6 # Rezus 14 17: CCCpCCCqqCCrrCpsstt # Condensed detachment, inference line 15 with line 16 # Rezus 18 18: CCCpCCCqqCCrrCCssCpttuu # Condensed detachment, inference line 15 with line 17 # Rezus 26 19: CCCpCCCqqCCrrCCssCCttCpuuvv # Condensed detachment, inference line 15 with line 18 20: CCCpqrCCpCCssqr # Condensed detachment, inference line 10 with line 7 # Rezus 28 21: CCCpCCCqqCCrrCCssCCttCpuuCCvvww # Condensed detachment, inference line 20 with line 19 # B' Simplify 22: CCCCpqCCqrCprss # Condensed detachment, inference line 5 with line 8 23: CCpqCCCrCCqstuCCrCCpstu # Condensed detachment, inference line 11 with line 12 24: CCCpCCqrstCCpCCCCCuvCCvwCuwqrst # Condensed detachment, inference line 23 with line 22 # Rezus 40 25: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxyyzz # Condensed detachment, inference line 24 with line 21 26: CCCpCCCqrstuCCpCCCqCCvvrstu # Condensed detachment, inference line 12 with line 20 # Rezus 42 27: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCyyzzp1p1 # Condensed detachment, inference line 26 with line 25 28: CCCCpCpqCpqrr # Condensed detachment, inference line 5 with line 4 29: CCpqCCCrCCCsqtuvCCrCCCsptuv # Condensed detachment, inference line 9 with line 23 30: CCpqCCCrCCCsCptuvwCCrCCCsCqtuvw # Condensed detachment, inference line 11 with line 29 31: CCpqCCCrCCCsCCqtuvwxCCrCCCsCCptuvwx # Condensed detachment, inference line 11 with line 30 32: CCCpCCCqCCrstuvwCCpCCCqCCCCCxCxyCxyrstuvw # Condensed detachment, inference line 31 with line 28 # Rezus 52 33: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzp1p1q1q1r1r1 # Condensed detachment, inference line 32 with line 27 34: CCpqCCCrCCCsCCCtquvwxyCCrCCCsCCCtpuvwxy # Condensed detachment, inference line 9 with line 31 35: CCCpCCCqCCCrstuvwxCCpCCCqCCCrCCCyzCCzp1Cyp1stuvwx # Condensed detachment, inference line 34 with line 22 # Rezus 68 36: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1u1u1 # Condensed detachment, inference line 35 with line 33 37: CCpqCCCrCsqtCCrCspt # Condensed detachment, inference line 9 with line 10 38: CCCpCqrsCCpCqCCtCCtuurs # Condensed detachment, inference line 37 with line 6 # Rezus 72 39: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1CCu1CCu1v1v1w1w1 # Condensed detachment, inference line 38 with line 36 40: CCpqCCCrCsCptuCCrCsCqtu # Condensed detachment, inference line 11 with line 37 41: CCpqCCCrCsCCtpuvCCrCsCCtquv # Condensed detachment, inference line 9 with line 40 42: CCpqCCCrCsCCtCquvwCCrCsCCtCpuvw # Condensed detachment, inference line 11 with line 41 43: CCCpCqCCrCstuvCCpCqCCrCCCwwstuv # Condensed detachment, inference line 42 with line 7 # Rezus 76 44: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1CCu1CCCv1v1Cu1w1w1x1x1 # Condensed detachment, inference line 43 with line 39 # Rezus 80 45: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1CCu1CCCv1v1CCw1w1Cu1x1x1y1y1 # Condensed detachment, inference line 43 with line 44 # Rezus 84 46: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1CCu1CCCv1v1CCw1w1CCx1x1Cu1y1y1z1z1 # Condensed detachment, inference line 43 with line 45 # Wish list theorem: BCIW REZUS 47: CCCpCCCqqCCrrCCssCCttCpuuCCCCCvwCCwxCvxCCCCCyCyzCyzCCCp1q1CCq1r1Cp1r1s1s1t1t1CCu1CCCv1v1CCw1w1CCx1x1CCy1y1Cu1z1z1p2p2 # Condensed detachment, inference line 43 with line 46 # Final proof had 47 lines (43 steps) # ------------------ End proof --------------

1: The question has been asked, "How did you choose those helper theorems? I went out a few inference steps and checked how many times they each appeared in parts of the Rezus formula, and tried the most popular. Looking at the result, I added MP by hand, and ran it and it worked.

This page is a copy of
http://www.cc.utah.edu/~nahaj/logic/concepts/semi/example.html,
Please bookmark that instead.

© Copyright 2010, 2011 by John Halleck, All Rights Reserved.

This page was last modified on February 9th, 2011