interesting sufficient conditions for when it does.
Best,
Andrei
*From:* Rob Arthan
*Sent:* 23 October 2016 12:23
*To:* Ondřej Kunčar
*Cc:* Ken Kubota; Prof. Andrew M. Pitts; Prof. Thomas F. Melham;
cl-isabelle-us.
While history of these matters is topical, I thought I might describe
the origin of this facility and the practical rationale for
conservativity at that time.
My memory is not completely reliable, so there might be something here
which I have misremembered but I think the main features will be g
certainly be Rob,
but I naturally prefer Arthan/Jones or some other joint attribution,
because I still think
of ProofPower as "my baby", in contexts where the entire team cannot be
credited.
But this isn't one of them so here, for the record is the list of
contributors:
Mark Ada
I have built PolyML 5.4 on Ubuntu 12.04 without problems.
To get the g++ compiler:
sudo apt-get install g++
is good.
Roger Jones
--
Free Next-Gen Firewall Hardware Offer
Buy your Sophos next-gen firewall before the end
On Thursday 09 Aug 2012 11:06, Michael Norrish wrote:
> 2) we need to/should accept the definitional principle
> that allows (closed) existential theorems to justify
> signature extension with constants, recognising that
> this doesn't assume AC
Is this a cue for reopening the discussion about
I see now that my sketch proof of "completeness" for Rob
Arthan's proposed new "new_specification" cannot be turned
into a rigorous proof.
When withness are obtained using the choice function, they
may fail the fourth of his specified constraints on the
witnesses. They will do so in just the
On Sunday 29 Apr 2012 11:11, Rob Arthan wrote:
> > The question I was asking was rather more mundane.
> > Given that we know what it means to say that some
> > proposition P is conservative over a given theory in
> > HOL (in the proof theoretic sense), the question is
> > "is there any proposition
On Saturday 28 Apr 2012 13:14, Rob Arthan wrote:
> On 28 Apr 2012, at 09:53, Roger Bishop Jones wrote:
> > Is the revised new_specification "complete"?
> > i.e. are there any conservative extensions which cannot
> > be achieved by it?
> > (an argument for t
Is the revised new_specification "complete"?
i.e. are there any conservative extensions which cannot be
achieved by it?
(an argument for this would strengthen the case)
In the context of the revised new_specification how do we
stand in relation to conservative introduction of type
constr
Though there is some cultural aversion to the use of axioms
in the HOL community, there is in fact no reason why a HOL
theorem prover cannot be used in a way which corresponds
closely to the axiomatic method of Euclid (made more
rigorous).
The most direct way to do this is to start a new theor
On Monday 16 May 2011 07:52, Mark wrote:
> ? [rbj]
> > Surely the ideal would be to avoid having ambiguous
> > names by renaming as necessary?
>
> I would think so, yes. But I'm talking about the pretty
> printer:
of course, I mistook the issue at stake.
> given any internal representation of
On Sunday 15 May 2011 15:08, Mark wrote:
> In fact HOL Zero is the only HOL system with a pretty
> printer specially designed to avoid all possible
> confusing results like that. For this situation, it
> returns Rob's "ideal output":
>
> # beta_conv `(\x. ?y. x = a /\ y = b) y`;;
> val it : t
I tried to install ckpt for use with hol-light and find that
it will not build on recent versions of Linux because one of
the headers it depends on is no longer available (page.h).
ckpt is no longer maintained, so there does not seem to be
any prospect of a fix.
Does anyone know a way round thi
On Wednesday 20 January 2010 16:02:10 Roger Bishop Jones wrote:
> On Tuesday 19 January 2010 18:07:32 Lockwood Morris wrote:
> > The only relevant information I have come across is Stewart Shapiro's
> > statement, in Foundations without Foundationalism, that in set theory
Further to my last message on this topic, I did discover the place in Shapiro
where he talks about this (5.1.3 p107).
On Tuesday 19 January 2010 18:07:32 Lockwood Morris wrote:
> The only relevant information I have come across is Stewart Shapiro's
> statement, in Foundations without Foundation
On Tuesday 19 January 2010 18:7:32 Lockwood Morris wrote:
> Does anyone know if it is possible to prove the well-ordering theorem in
> HOL for an arbitrary type? That is, using the terminology of
> relationTheory,
>
> ?R:'a->'a->bool. WF R /\ StrongLinearOrder R .
There is a proof in Proof
On Thursday 17 September 2009 01:56:41 Behzad Akbarpour wrote:
>I have a huge definition of an RTL design function (more that 6000 lines of
>HOL code), and I'm trying to load and compile it in HOL, but I couldn't
>succeed.
...
> Do you have any idea how to solve this problem?
Back in 1988 we ver
17 matches
Mail list logo
