John, I realized my miz3 Hilbert axiom formalization may not have been
rigorous, or captured Hilbert's axiom, as I had no notion of line
other than the datatype new_type_abbrev("line",`:point->bool`);;
saying a line is a subset of our model of Hilbert's axiom. That's
possibly buggy, because there
Tom Ridge and I formed two teams of one each using HOL4 and ProofPower-HOL
(respectively) in the first VSTTE competition which was a slightly smaller
scale affair at the previous VSTTE (it was a rather open-ended 2 hours during
the conference rather than 48 hours strictly timed several weeks bef
Sounds like a bug. Can you send me sources?
Thanks,
Konrad.
On Wed, Jun 6, 2012 at 1:30 PM, Ramana Kumar wrote:
> On Wed, Jun 6, 2012 at 7:20 PM, Konrad Slind wrote:
>>
>> Note that Datatype.build_tyinfos is only guaranteed to work on
>> types that Hol_datatype produces. Does your datatype hav
On Wed, Jun 6, 2012 at 7:20 PM, Konrad Slind wrote:
> Note that Datatype.build_tyinfos is only guaranteed to work on
> types that Hol_datatype produces. Does your datatype have
> some other features?
Yes, recursion through the range of a finite map.
It wasn't _too_ difficult to prove what look
Note that Datatype.build_tyinfos is only guaranteed to work on
types that Hol_datatype produces. Does your datatype have
some other features? In any case, what happens with
gen_datatype_info?
Thanks,
Konrad.
On Wed, Jun 6, 2012 at 12:33 PM, Ramana Kumar wrote:
> Dear Konrad,
> Thanks a lot for
On Wed, Jun 6, 2012 at 6:33 PM, Ramana Kumar wrote:
> > Cv1_Axiom;
> val it =
>|- ∀f0 f1 f2 f3 f4 f5 f6 f7.
> ∃fn0 fn1 fn2.
>(∀l. fn0 (CLitv l) = f0 l) ∧
>(∀m vs. fn0 (CConv m vs) = f1 m vs (fn1 vs)) ∧
>(∀env xs b. fn0 (CClosure env xs b) = f2 env xs b (fn2 env))
Dear Konrad,
Thanks a lot for your reply.
I'm going to take this discussion onto the mailing list rather than the
issue tracker.
Further comments and questions below.
On Wed, Jun 6, 2012 at 6:09 PM, Konrad Slind <
reply+i-4768236-445b46219fa700ba592ca0826c0c435b3111c21c-181...@reply.github.com
> w
On Wed, Jun 6, 2012 at 1:51 PM, Rob Arthan wrote:
> Tom Ridge and I formed two teams of one each using HOL4 and ProofPower-HOL
> (respectively) in the first VSTTE competition which was a slightly smaller
> scale affair at the previous VSTTE (it was a rather open-ended 2 hours
> during the confere
Dear HOL users
Would anyone be interested in entering a team using HOL4 or HOL Light to
the "Verified Software: Theories, Tools and Experiments" competition next
year (2013)?
Information about the last competition is here:
https://sites.google.com/site/vstte2012/.
Winning teams used ACL2, KIV, Daf
*** Early registration ends June 20 ***
== CALL FOR PARTICIPATION
==
24th International Conference on Computer Aided Verification (CAV 2012)
July 7-13, 2012 Berkeley, California, USA
Program Chairs: Madhusudan Parathasarathy and Sanjit A. Seshia
10 matches
Mail list logo
