Ah! Of course! Thank you again! I think I got it now. For completeness sake, in case anyone else is pursuing this line of learning ProofPower, I have a link here to the working version with those pieces in place. I do think there is a lot of potential for using this tool to teach Discrete Math. Sample predicate calculus proof <https://www.dropbox.com/s/7kd7dsd2erg0hi1/pred_calc.png?dl=0>
On Tue, Mar 17, 2015 at 1:45 PM, Rob Arthan <[email protected]> wrote: > David, > > The proof isn’t complete, as you will see if you look at the output when > you execute the lines that bind L6 and L7. You have just bound L6 to a term > not a theorem. You have bound L7 to the the applicatio of %forall%_intro to > L6, which does not give you a theorem (but rather a function from theorems > that will always fail, because %forall%_intro requires its first argument > to be (something akin to) a variable). The last line of your proof should > be something like: > > val L6 = %forall%_intro %<%x%>% L5; > > Regards, > > Rob. > > > On 17 Mar 2015, at 13:45, David Topham <[email protected]> wrote: > > > > That makes sense, but the "proof" is completed, so what can I apply it > to? i > > .e. The goal of the proof is just to derive L7. Perhaps put it the form > of a conditional? ...conjunction of premises model the conclusion? > > > > On Mar 17, 2015 5:02 AM, "Rob Arthan" <[email protected]> wrote: > > David, > > > > Your value L7 is a function (type THM -> THM) not a theorem (type THM). > > You need to apply it to another theorem to get a new theorem. > > ] > > Regards, > > > > Rob. > > > > On Tue, March 17, 2015 12:59 am, David Topham wrote: > > > Thank you so much Rob! That works! If you don't mind another > question: > > > I > > > had gotten format_thm to work without quantifiers, but with the > quantifier > > > I get an exception. (attached). I don't see anything about format_thm > in > > > user029.pdf (the main HOL reference). -Dave > > > > > > On Mon, Mar 16, 2015 at 2:51 PM, Rob Arthan <[email protected]> wrote: > > > > > > > > >> David, > > >> > > >> > > >>> On 16 Mar 2015, at 04:22, David Topham <[email protected]> wrote: > > >>> > > >>> > > >>> With my recent success learning to encode Propositional Calculus > > >>> using > > >> ProofPower (for my Discrete Math course), I have pressed on to > > >> Predicate > > >> Calculus. > > >> > > >>> > > >>> So far, I have figured out the basics, but stuck on quantifiers from > > >>> > > >> what I intuitively thought might work. Attached is my error message > > >> trying to quantify a negation. > > >> > > >> ProofPower syntax needs a bullet between the bound variables and the > > >> predicate in a quantification. You have to write: > > >> > > >> ∀ xâ¦? ¬ P(x) > > >> > > >> rather than: > > >> > > >> ∀ x ¬ P(x) > > >> > > >> This follows what is now common practice in logical languages used in > > >> CS > > >> and reflects a decision to make quantifiers have lower precedence than > > >> the propositional operators, so that the scope of a quantifier extends > > >> as far to the right as possible (as opposed to traditional > mathematical > > >> logic practice which requires brackets around the matrix of a > > >> quantification if the matrix is not a literal). So the brackets > around > > >> the implication in: > > >> > > >> ∀ xâ¦? (¬ P(x) ⇒ Q(x)) > > >> > > >> are unnecessary. (I think of the bullet as being like a big version of > > >> Russell & Whitehead’s convention of using a dot to adjust the > > >> precedence of a connective.) Unfortunately, this is probably at odds > > >> with the conventions you have been using in your course. > > >> > > >> Regards, > > >> > > >> > > >> Rob. > > >> > > >> > > >> > > > > > > > > >
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
