Effective Immediately New Release of DC Proof 1.0 Dated 2006-02-22 Includes: 1. Fixed bug in Subset Rule that would sometimes insert brackets improperly....
Effective Immediately New Release of DC Proof 1.0 includes: 1. Warning on Premise Rule that lists existential variables (those introduced by Existential...
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 dated 2006-03-20 includes: 1. Added Reset button to Substitution Form. 2. When closing a Premise Block...
Effective Immediately New release of DC Proof 1.0 dated 2006-05-26 Includes: 1. Improved warning message for the Premise Rule indicating any relevant...
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. ...
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...
Thomas, Thanks for bringing this to my attention! The proof in question (at the DC Proof website) was written with an old version of DC Proof. Currently,...
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 Thomas, You will get that message sometimes when you do Existential Specification. It is for informational purposes only to help you understand warnings...
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 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 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, The usual order precedence for algebraic operators is built into DC Proof. In this case r=c+a+b is interpreted as r=(c+a)+b, the left- most +...
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 Dan, I hope these proofs are of interest to you :-). The 'details' of the proof are contained in 6 separate files: - 'addcancelable_short' extends...
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...
... (How) ... thought ... I ... proof ... In addition to all direct references to a selected line of proof, the Delete All References command will also delete...
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 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...
... for ... definition ... Thomas, I like your straightfoward construction of the add function(lines 18 - 27). It is much superior to the one I posted here...
Hi Dan, ... Thanks for the flowers ;-). But in fact it's your construction of Sep. 13. The main reason for removing the condition "(a,b,c) e n3" was to ease...
... (lines ... Sep. ... to ... [snip] My proof of Sep 13 was based on a construction of the set of functions of two variables mapping NxN -> N, and then taking...
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...
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....
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...
(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...
Having problems with message search?
Fill out this form to ensure your group is one of the first to be migrated to the new message search system.
