Hi Dan,
So, in a nutshell, you've got N proof scripts in HOL Light that you want
to fit together as one coherent proof in a single session, but that
would take far too much processing to do so in practice. So you want to
execute these in N parallel HOL Light sessions, recording the
kernel-le
Hi Mario,
Yes, as Freek says, Tactician would do the sort of thing you need, but
is only for HOL Light. It works on the vast majority of tactic proofs
as they are typically written in HOL Light, say perhaps 1 in every 1,000
proof script lines might trip it up. It could be ported to HOL4, but
And for HOL Zero there is Appendix C of the User Manual that gives a
formal grammar of the HOL Zero concrete syntax. Again, this is fairly
similar to HOL Light's and HOL4's, but there are numerous small
differences. Note that the formal grammar hasn't actually been checked
(as far as I'm awar
I think there is definitely an advantage in keeping ``x/y`` undefined
(even granted that it will always be possible to prove ``?y. x/0 = y``),
namely that it means that your proofs are much more likely to directly
translate to other formalisms of real numbers where '/' is not total.
Of course
Hi,
I don't know of any function in HOL Light (although I'm don't know about
most recent versions).
To write your own, a simple approach would be to print primitive term
syntax, with all constants and variables annotated with their type, and
to put parentheses around everything at every leve
try the black box method myself (I won't be using this very
often and the accuracy is not quite important).
I saw a directory Proofrecording in the root directory of HOL Light.
There's also anther implementation of dependency tracking as part of
anther project here [1] These might b
Hi Yaqing,
I could enhance my Tactician tool to do this sort of thing. In fact, a
new release is long overdue, so I'll try to find the time to do this
soon (but am too busy in the next few weeks).
But you say you're looking for a quick patch. One approach would be to
apply the original con
Hi Michael,
Yes, Konrad's right about how types are determined in term quotations,
and I too don't know of an INST in HOL Light that unifies the types of
its arguments.
To get a listing of the types of the free variables in 'th', you can do:
map dest_var (frees th);;
or to return the type
implementations that have this property of Pollack-consistency.
It's good to see that these properties are being taken seriously.
In the case of R0, this even holds for full proofs, and the
property of faithfulness is also implemented:
"Generally, definitions once introduced cannot
k in correspondingly
wrongly (so, for example, print & parse "true" as "false" and vice
versa).
Mark.
On 13/02/2017 15:38, Ken Kubota wrote:
> Dear List Members,
>
> Through Mark Adams' paper "HOL Zero's Solutions for
> Pollack-Inconsistency&quo
billion primitive
inference steps. Another intended role is a pedagogical example of a
basic HOL system, with a simple coding style and lots of code comments
explaining what is going on, which also helps trustworthiness.
Mark Adams.
On 22/10/2016 03:41, Ken Kubota wrote:
> … I have now ad
Hello Abid,
The term quotation fails type checking simply because the types of LHS
and RHS of the equality are different:
`:real^((N,P)finite_sum,Q)finite_sum^M` (with type vars N, P, Q, M)
`:real^(N,(P,Q)finite_sum)finite_sum^M` (with type vars N, P, Q, M)
As I understand it (I may be
It's a bit confusing. The expressions you enter in the session are not
actually in HOL - they are in the functional programming language ML.
This is the language used to implement HOL4. You are in an ML toplevel
(also called "read-eval-print loop" or "REPL"), with HOL4 already
incorporated. ML
').
So I think you should get what you intend by transforming it to
something logically equivalent, i.e. change "A ==> B ==> C" to "A /\ B
==> C". The error messages could be much better here.
Mark.
On 17/06/2016 10:51, Heiko Becker wrote:
> Hello,
> On
Hi Heiko,
That's strange, your corrected version goes through fine on my computer.
Do you still get the same problem if you restart HOL Light and enter
the corrected script? What version of HOL Light are you using?
Mark.
On 16/06/2016 10:01, Heiko Becker wrote:
> Forwarded Message --
For HOL Light I've got a tool called Tactician that would be ideal for that:
http://www.proof-technologies.com/tactician/
but it doesn't work for HOL4. One day I hope to port it, but that's
unlikely to be done in the near future.
Mark.
on 27/11/15 8:20 AM, Ada wrote:
> Hey guys,
>
> I am
)
>>
>> Of course in Flyspeck many (most?) proofs are the other
>> way around, where there is just a list of tactics that is
>> processed like you would successively "e" them interactively.
>> I think Mark Adams tactician is exa
Hi Petros/Joe,
I must admit that I'm not particularly familiar with any of these Emacs/etc
modes for HOL Light and HOL4, although I have seen Proof General, and
ProofTree that interacts with it. How do these other facilities compare?
> Tactician is more general and gives you a full breakdown of
Hi Robert,
Could you provide more information about the circumstances when it fails?
Specifically, which versions of OCaml and Camlp5 are you using? Execute the
following in a terminal window:
ocaml -version
camlp5 -v
Does this error arise when building HOL Light from source in an OCaml
se
Seems a good idea to me. Given ETA_AX, it's easy to show equivalence with
current HOL Light, and it's always better to have closed formulae coming out
of definition commands.
One small point: the formulae as written in the linked message do not have
the intended syntactic form (due to bracketing)
_
> From: marco.magg...@gmail.com [marco.magg...@gmail.com] on behalf of Marco
> Maggesi [magg...@math.unifi.it]
> Sent: 17 September 2014 08:15
> To: Mark Adams
> Cc: Nela Cicmil; hol-info@lists.sourceforge.net
> Subject: Re: [Hol-info] advice on installing Ocaml
, Alexey Solovyev, Hoang Le Truong,
and the Flyspeck Team
August 10, 2014
CREDITS
Project Director: Thomas Hales
Project Managers: Ta Thi Hoai An, Mark Adams
HOL Light libraries and support: John Harrison,
Isabelle Tame Graph Classification: Gertrud Bauer, Tobias Nipkow,
Chief Programmer:
Hi Nela,
There have been various problems over the years, but I get no problems with
recent versions of HOL Light (downloaded since May 2014, including SVN
version 197 downloaded in mid-August) with OCaml 4.01.0 and Camlp5 6.11
running on Fedora 17.
Do you know the HOL Light SVN version (or other
Hi Bill,
on 21/3/14 4:28 PM, Bill Richter wrote:
> ... BTW where is the constant = defined in HOL Light? I see now that
> the line in bool.ml override_interface ("<=>",`(=):bool->bool->bool`);;
> just means that <=> is being defined as a synonym for = in this special
> case. In general = has t
I should have said '@' instead of '?' here. The constant '?' is actually
defined in these axiomatisations (using '@').
Mark.
on 21/3/14 9:10 AM, Mark Adams wrote:
> ... In HOL Light's axiomatisation, the only such entities are the 'bool&
Hi Bill,
on 21/3/14 6:19 AM, Bill Richter wrote:
> ...
>
> T = ((λxbool . x) = (λxbool . x))
>
> So it looks to me that HOL Light is defining Tom's primitive = in terms of
> the Ocaml =. Is that correct? And maybe that just means that the HOL
Light
> primitive = is "represented" in Ocaml as th
Hi Bill,
Have you tried looking at the HOL Zero source code? I think you will find
it illustrative for your purposes. It has a simple core like HOL Light, but
the source code explains more of what is going on. In file 'corethy.ml' I
try to motivate the axioms and constant definitions used in th
Ah yes, point taken.
on 8/1/14 10:13 AM, Rob Arthan wrote:
> Mark,
>
> On 8 Jan 2014, at 03:22, Mark Adams wrote:
>
>> Not wanting to be too picky here (because I very much agree with the
> thrust
>> of what Rob is saying), but isn't ProofPower term quotation par
Not wanting to be too picky here (because I very much agree with the thrust
of what Rob is saying), but isn't ProofPower term quotation parsing
sensitive to the subgoal package state (specifically, free variables in term
quotations pick up the types of existing free variables in the subgoal
package
Oops. That last email contains an error in the detail. The HOL Light
adaption of 'plexer.ml' and 'pa_o.ml' is called 'pa_j.ml'.
Mark.
on 15/10/13 2:29 PM, Mark Adams wrote:
> Hi Rob,
>
> Yes, you not only need a sufficiently recent version of Camlp5 for
Hi Rob,
Yes, you not only need a sufficiently recent version of Camlp5 for your
version of OCaml, you also need to create a sufficiently recent
adapted-for-HOL-Light version of pa_j.ml (adapted from Camlp5 source code
files etc/). You are right that you can work out what adaptions to do by
diffin
to suggestions for
improvement and/or debate about appropriate choice of
names/descriptions/scope.
Mark Adams
--
Benefiting from Server Virtualization: Beyond Initial Workload
Consolidation -- Increasing the use of
32 matches
Mail list logo
