(I have tried to send this twice already without apparent success. Apologizing in advance for any duplication.) Below are the correct URL's for the proofs...
Dear members, I have included three new, very brief proofs illustrating a set theoretic interpretation of the classical syllogism in the latest version of the...
Dear members, I have been working on possible enhancements to DC Proof that I hope will make it easier to create recursive definitions of sets and functions....
Effective Immediately New Release of DC Proof, dated 2006-10-24 Includes: 1. Fixed bug in Universal Generalization module that would, on rare occasions, result...
Hi Dan, here's what I proved so far in constructing the add function. By the way, I think it's remarkable that the function used in the construction is...
Hi Dan, here's the 'commutativity' proof of the add function-- I'm not quite sure if 'symmetric function' is the correct term for it. Regards, Thomas [Download...
Hi, recently I noticed that 'delete all references' also deletes statements even if they don't reference the line being deleted. (How) can I prevent that? I...
Hi Dan, I hope these proofs are of interest to you :-). The 'details' of the proof are contained in 6 separate files: - 'addcancelable_short' extends...
Effectively immediately New release of DC Proof 1.0 includes: 1. Change to User Reference Guide. Added note to section on Substitution Rule: "Please note that...
Hi list, there's something odd about substitution: Suppose you have r=c+a+b and x=a+b then substituting x in the 1st equation is impossible; whereas it works...
Hi Thomas, Heading in the direction you've suggested: x<y =>x+x<y+x =>x+y<y+y x+y=y+x =>x+x<y+y This requires a<b=>a+c<b+c, a+b=b+a, a<b & b<c => a<c And if...
Hi folks, I'd like to prove for all natural numbers a,b that a +a=b+b implies a=b. My ideas so far: Having shown that a<b, a=b, b<a are mutually exclusive, it...
Hi Dan, here's a fragment of a proof. Applying the uspec/espec rule to line 94, I get the warning: "x will depend on: x1, x2, y1, y2." Note that none of these...
Hi list, looking at the proof regarding addition of natural numbers, it was stated that the subset rule had been used-- in particular the set s being...
Effective Immedidately New Release of DC Proof 1.0 dated 2006-08-14 includes: 1. Minor changes to Tutorial in User Documentation. No changes to functionality. ...
Effective Immediately New release of DC Proof 1.0 dated 2005-06-20 includes: 1. Change to Delete All References (F3) that will, in some cases, reduce the...
Effective: July 8, 2004 5:50 PM EST New Release of DC Proof 1.0 Includes: 1. Revised and expanded Tutorial 2. New Samples subdirectory with more sample proofs...
Effectively Immediately New release of DC Proof 1.0 dated 2006-03-10 includes: 1. In insert mode, after Undoing a change, cursor now properly reset at insert...
Effective Immediately New Release of DC Proof 1.0 includes: 1. Warning on Premise Rule that lists existential variables (those introduced by Existential...
Effective immediately. New release of DC Proof 1.0 including: 1. Fixed bug in Existential Generalization (E Gen) Rule that, in some cases, failed to detect if...
Here are the axioms for the real numbers that users of DC Proof may find useful for doing proofs in real analysis (calculus). I will include it in the Samples...
Dear members, Here is another, considerably simpler approach to working with real numbers in DC Proof. Rather than constructing the reals starting with Peano's...
Effectively Immediately New release of DC Proof 1.0 dated 2006-02-15 includes: 1. Fixed bug in Subset Rule that could lead to invalid proofs as a result of...
Effective immediately... New release of DC Proof 1.0 dated 2005-8-8 includes: 1. Improved graphics (screen shots) in tutorial and user guide. 2. Larger fonts...
Dear members, I received the following proof from Mark Hurd. Using the new SUM shortcut, he proved that x + x^2 + x^3 + ... + x^k = x*((x^k-1)/(x-1)) for x>1 ...
Effective immeidately... New version of DC Proof 1.0 dated 2005-08-5 includes 1. New shortcuts for SUM and PROD operators (on Numbers menu) 2. Minor bug fixes,...
Dear Members, Following is a proof using the SUM operator for an arbritary number of constants: http://www.dcproof.com/SUMconstants.proof (DC Proof format) ...
Hi, Thanks for the suggestions. Below, you will find some suggestions to help you achieve at least some of the functionality you are looking for, using the...
Hi Dan, The problem with your proof is that it uses Contra, which is effectively the thing being proved. I agree that CASES should work. NB a workaround: if...
Having problems with message search?
