Thanks Ramana and Konrad both for the helpful and stimulating comments!
Both of your references look quite worthwhile and I will definitely be
looking at them in some detail.
Cheers,
Cris
On Tue, Apr 24, 2012 at 8:01 AM, Konrad Slind <[email protected]>wrote:
> You can also check out
>
> src/bool/boolScript.sml
>
> in the HOL4 distribution where quite a few theorems are proved
> about the connectives and quantifiers. Those are forward proofs
> since tactics don't yet exist at that stage of system build. So they
> should be easy to adapt to your framework. One example:
>
> (*
> ------------------------------------------------------------------------- *)
> (* Skolemization: |- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x)
> *)
> (*
> ------------------------------------------------------------------------- *)
>
>
> val SKOLEM_THM = save_thm("SKOLEM_THM",
> let val P = Term`P:'a -> 'b -> bool`
> val x = Term`x:'a`
> val y = Term`y:'b`
> val f = Term`f:'a->'b`
> val tm1 = Term`!x. ?y. ^P x y`
> val tm2 = Term `?f. !x. ^P x (f x)`
> val tm4 = Term`\x. @y. ^P x y`
> val tm5 = Term`(\x. @y. ^P x y) x`
> val th1 = ASSUME tm1
> val th2 = ASSUME tm2
> val th3 = SPEC x th1
> val th4 = INST_TYPE [alpha |-> beta] SELECT_AX
> val th5 = SPEC y (SPEC (Term`\y. ^P x y`) th4)
> val th6 = BETA_CONV (fst(dest_imp(concl th5)))
> val th7 = BETA_CONV (snd(dest_imp(concl th5)))
> val th8 = MK_COMB (MK_COMB (REFL (Term`$==>`),th6),th7)
> val th9 = EQ_MP th8 th5
> val th10 = MP th9 (ASSUME(fst(dest_imp(concl th9))))
> val th11 = CHOOSE (y,th3) th10
> val th12 = SYM (BETA_CONV tm5)
> val th13 = SUBST [Term`v:'b` |-> th12] (Term`^P x v`) th11
> val th14 = DISCH tm1 (EXISTS (tm2,tm4) (GEN x th13))
> val th15 = ASSUME (Term`!x. ^P x (f x)`)
> val th16 = SPEC x th15
> val th17 = GEN x (EXISTS(Term`?y. ^P x y`,Term`f (x:'a):'b`) th16)
> val th18 = DISCH tm2 (CHOOSE (f,th2) th17)
> val th19 = MP (MP (SPEC tm1 (SPEC tm2 IMP_ANTISYM_AX)) th18) th14
> in
> GEN P (SYM th19)
> end);
>
> Konrad.
>
>
> On Tue, Apr 24, 2012 at 1:26 AM, Ramana Kumar <[email protected]> wrote:
> > You might want to consider implementing import/export of OpenTheory
> proofs
> > (http://www.gilith.com/research/opentheory/) to get access to some
> larger
> > existing proofs. It would be interesting to see how they would look in
> the
> > web interface.
> >
> > On Mon, Apr 23, 2012 at 3:32 AM, Cris Perdue <[email protected]> wrote:
> >>
> >> I would like to announce the Prooftoys visual proof assistant, a work in
> >> progress, and invite experimental use of it, available at
> >> http://prooftoys.org/.
> >>
> >> The Prooftoys logic is very close to Peter Andrews' Q0, including
> >> essentially the same axioms and the same single fundamental rule of
> >> inference, Rule R, which allows replacement of a term by an equal term.
> The
> >> implementation builds up numerous derived rules of inference, which are
> >> available in the same way as theorems and the primitive rule of
> inference
> >> through the web-based user interface.
> >>
> >> Prooftoys and its user interface normally run entirely within the user's
> >> web browser for interactivity and immediate access. It includes an
> >> interactive proof editor, with ability to save and restore proofs to
> textual
> >> format. It supports inference in the style of natural deduction, using
> >> hypotheses.
> >>
> >> The system aims to make higher-order logic more accessible conceptually
> >> and easier to use as a tool, bringing more people to understand and use
> it.
> >>
> >> The implementation is very much a work in progress in all dimensions,
> but
> >> has been working well for experimental interactive use. It has a set of
> >> axioms for real numbers and some rather primitive derived rules of
> inference
> >> so it is possible to experiment with real numbers.
> >>
> >> More information is available on the Prooftoys web site.
> >>
> >> Best regards,
> >> Cris Perdue
> >>
> >>
> >>
> >>
> ------------------------------------------------------------------------------
> >> For Developers, A Lot Can Happen In A Second.
> >> Boundary is the first to Know...and Tell You.
> >> Monitor Your Applications in Ultra-Fine Resolution. Try it FREE!
> >> http://p.sf.net/sfu/Boundary-d2dvs2
> >>
> >> _______________________________________________
> >> hol-info mailing list
> >> [email protected]
> >> https://lists.sourceforge.net/lists/listinfo/hol-info
> >>
> >
> >
> >
> ------------------------------------------------------------------------------
> > Live Security Virtual Conference
> > Exclusive live event will cover all the ways today's security and
> > threat landscape has changed and how IT managers can respond. Discussions
> > will include endpoint security, mobile security and the latest in malware
> > threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> > _______________________________________________
> > hol-info mailing list
> > [email protected]
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
