to cover
non-basic aspects of HOL theorem proving that are not used in HOL Zero
(e.g. rewriting, subgoal package, meson), although maybe I could
produce a general HOL version if there is enough interest.
Mark Adams
GLOSSARY.gz
Description: GNU Zip compressed data
with unintentional meaning.
Mark Adams
on 28/10/10 2:10 PM, liliminga lilimi...@126.com wrote:
Hello,
When I read realTheory, I see the REAL_INV_0 theorem. Its content is inv 0
= 0,
according to my understanding, it means that the reciprocal of real_0
is real_0. But it is contradictory
Yes you do need a C compiler to install Poly/ML from source. GCC is
perfectly suitable. For Mac OS X, this is not installed by default, but is
available on the Install CD that comes bundled with your Mac, in the Xcode
directory.
Mark.
on 15/2/11 7:50 AM, waqar ahmed w.ahme...@googlemail.com
, etc. I did, however, attempt to give informal
English explanations of the logical core's definitions and axioms in
source code comments, but this didn't stretch to falsity and logical
negation (but I would like it to!).
Mark.
On Wed, 23 Feb 2011 13:40:54 +, Russell Wallace
) = a /\
(y:'2) = b)
But note that HOL Zero only supports a very basic style of interactive
proof, and doesn't come with the advanced automated and interactive
facilities that the other HOL systems have.
Mark Adams.
I'm a new user of hol-light and I find the following thing strange :
# BETA_CONV
output faithfully
represents that internal representation, so as not to mislead the user.
This is the pertinent question when it comes to theorem prover
trustworthiness (other than the logical soundness of internal deductions and
the architecture of the inference kernel).
Mark
problems in large projects,
misreading ambiguous output that I subconsciously assumed meant the
obvious.
Mark
--
Achieve unprecedented app performance and reliability
What every C/C++ and Fortran developer should know.
Learn
a display option to display the types of all printed variables.
Mark.
on 13/10/11 9:57 AM, Jonathan von Schroeder jonathan.von_schroe...@dfki.de
wrote:
Hi Czeray,
thanks for the clarification. Looking at src/HOL/Import/* I couldn't
really
figure out how to invoke the automatic generation myself. Can
that there was a similar posting a few months ago:
http://sourceforge.net/mailarchive/message.php?msg_id=28674314
Hope this helps,
Mark.
on 14/3/12 9:23 AM, Adam Golding adamgold...@adamgolding.com wrote:
My Situation:
Windows 7 64-bit Ultimate
Cygwin (with the Cygwin version of OCaml 3.12.1)
Since
the
same problem as me. I recommend Camlp5 version 5.15. Old versions are
available towards the bottom of the Camlp5 page:
http://cristal.inria.fr/~ddr/camlp5/
This works for me with the latest HOL Light SVN download.
Mark.
on 14/3/12 5:19 PM, Adam Golding adamgold...@adamgolding.com
don't bother giving myself $100).
Makarius wrote:
Mark Adams occasionally promotes an even more aggressive
scenario for HOL Zero where he wants to admit potentially
malicious users, an army of paid proof-workers who want to
cheat. (I am not really following him here, we are not that
far yet
it n + 2^31 arguments (on a 32-bit platform). This is
a bit of a rough edge, but of somewhat academic interest, and I
don't think it implies a soundness problem (you could imagine
allowing type constructors with the same name but different
arities). Still, maybe Mark Adams will find a flaw
this is not a route to unsoundness. Phew!
But I still get a fundamental sense of unease that types can be constructed
that are not well-formed (i.e. where the arities are wrong), so I'll adapt
HOL Zero to stop this.
John Harrison wrote:
Mark wrote:
I always thought that this would be impossible
ago. I don't know about other countries.
Of course this sort of thing would still be very useful to undergrad courses
around the world.
Mark.
on 24/5/12 1:56 AM, Cris Perdue c...@perdues.com wrote:
Reading Freek Wiedijk's paper Formal Proofs: Getting
Startedhttp://www.ams.org/notices/200811
is particularly useful for those wishing learn from the
hundreds of packaged-up proofs that come with the HOL Light release.
Mark
--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security
. But you still have the
problem that you can't parse in term quotations involving the new constant -
they would always require syntax constructors.
Mark.
on 27/6/12 8:10 AM, Bill Richter rich...@math.northwestern.edu wrote:
parse_as_infix(seg_less,(12, right));;
let SegmentOrdering_DEF
How does the HOL4 parser deal with the associated potential ambiguities?
E.g. ``x -b- y`` getting parsed as infix -b- applied to ``x`` and ``y``,
as opposed to (say) infix - applied to ``x - b`` and ``y``?
Mark.
on 27/6/12 11:22 AM, Michael Norrish michael.norr...@nicta.com.au wrote:
On 27/06
trustworthiness issues) in the theorem prover, to prove a fallacy, or to
appear to prove a fallacy.
Mark.
on 6/7/12 7:45 AM, Bill Richter rich...@math.northwestern.edu wrote:
My question is: What kind of proof is miz3 saying I have? Recall that
my long-term purpose is to teach a rigorous
,
where he asked expert users of various theorem provers, including HOL Light,
Mizar, Coq and Isabelle/HOL Isar, to formalise a classic textbook proof.
http://www.cs.ru.nl/~freek/demos/index.html
Regards,
Mark.
on 7/7/12 12:59 AM, Cris Perdue c...@perdues.com wrote:
Mark and all,
Yay! That's
wholeheartedly
agree with all of his principles in section 2.
Mark.
--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers
hopefully.
The platform actually predates HOL Zero by about two years. Part of the
motivation for building HOL Zero was producing a clear example of the
platform.
Mark.
on 12/7/12 2:48 AM, Cris Perdue c...@perdues.com wrote:
Hello Mark and All,
I noticed Mark's publication Introducing HOL Zero
it's perfectly
good)? I disagree with both, but it's difficult for me to defend my
position without an actual implementation of my system to back me up.
Mark.
on 12/7/12 8:11 AM, Ramana Kumar ramana.ku...@gmail.com wrote:
On Wed, Jul 11, 2012 at 8:38 PM, Mark m...@proof-technologies.com
wrote
Hi Peter,
Thanks for the interest. Porting to HOL4 is very feasible. Especially if
someone could fund me to do this!
Mark.
on 27/7/12 3:18 PM, Peter Vincent Homeier palan...@trustworthytools.com
wrote:
Hello, Mark.
Are you interested in porting this technology to the HOL4 system?
Peter
middle is derived like it is in HOL Light. HOL4's formulation
of the HOL logic is much the same as in the early systems, but does away
with a different axiom (IMP_ANTISYM_AX), proving this using excluded middle.
I wonder whether HOL Zero's or HOL4's formulations could be further
minimalised...
Mark
in the representation of set abstractions, but the
representation is quite complicated and also involves a few other things,
and presumably it is these other things that MESON is not so good at.
Hope this helps.
Mark.
on 12/8/12 3:45 AM, Bill Richter rich...@math.northwestern.edu wrote:
I made real
some formal mathematical logic that is not HOL
Mark.
--
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
:
http://www.proof-technologies.com/misc/Glossary.txt
Mark.
on 13/8/12 5:18 AM, Bill Richter rich...@math.northwestern.edu wrote:
Thanks, Michael! I will treat the Logic Manual as a true description of
the
HOL in HOL Light, and I will try harder to read it. I have a lot of
trouble
of the
point of using Camlp4/Camlp5 to change the OCaml lexical syntax).
Mark.
on 16/8/12 10:21 PM, Vincent Aravantinos vincent.aravanti...@gmail.com
wrote:
Hi list,
is there a good reason for not using Ocaml modules in HOL Light?
This would yield a better name management, and shorter and more
enumeration (i.e. [ a; b; c ])
Note that this is just my own informal list, derived from observed
behaviour, and there might be errors in it. Please someone say if they find
an error!
Mark.
on 6/12/12 5:14 AM, Bill Richter rich...@math.northwestern.edu wrote:
I'm trying to learn HOL Light
are mandatory - so `a,b,c` in HOL Light is `(a,b,c)` in HOL
Zero.
Mark.
--
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency
Oops, my Low-tech solution B doesn't require an adapted HOL Light term
quotation parser.
Mark.
on 17/4/13 10:08 AM, Mark m...@proof-technologies.com wrote:
Hi Bill,
(I'm joining this conversation late, so apologies if I've got the wrong
end
of the stick here, but ...)
If you want to do
to true data structures (which are quite unreadable
for large terms).
Mark.
--
Try New Relic Now We'll Send You this Cool Shirt
New Relic is the only SaaS-based application performance monitoring service
that delivers
this printed out:
Exception: whatever
So this doesn't stop Exception getting printed out at the start, but you
have control over everything else after that. There is probably also a way
to stop Exception getting printed, but I just don't know enough about
OCaml to do this.
Mark.
on 26/7/13 1:48 PM
Hi Bill,
Thanks, Mark! That sounds like a good tip, but can you be more specific?
I
produce error message with this function
let PrintErrorFail s =
open_box 0; print_string s; close_box (); print_newline (); fail();;
But I only want to change the OCaml exception printer for my
?
No it doesn't. You need HOL-Omega for that. This and many other aspects of
HOL are covered in my glossary.
Mark.
--
Get your SQL database under version control now!
Version control is standard for application code
difficult to find good documentation
about. I've only got a partial understanding, which is good enough for my
purposes in Tactician.
Mark.
--
Get your SQL database under version control now!
Version control is standard
is not opened.
Yes, but 'print_string' and 'print_newline' are in *both* modules:
Pervasives and Format. All the other formatting stuff is not in Pervasives.
Mark.
--
Get your SQL database under version control now!
Version
not..) be more
understandable. Download the HOL Zero source distribution from:
http://www.proof-technologies.com/holzero/
Best,
Mark.
on 15/5/15 11:22 PM, Robert White ai.robert.wangsh...@gmail.com wrote:
Dear Sir/Madam,
I wonder if you could explain a bit of the last step of the proof of law
I forgot to say that the theorem is 'excluded_middle_thm' and its proof is
in file 'src/boolclass.ml'.
Mark.
on 18/5/15 5:17 PM, Mark m...@proof-technologies.com wrote:
Hello Robert,
If you're interested in the proof itself, rather than how in how the HOL
Light one works, then there's also
type is intended for "x", and so gives it a unique
type variable, which your printer would show as:
`x:?1143114`
whereas if you entered `x:A`, then the type of "x" is determined, and
your printer would print as:
`x:A`
Mark.
On 16/05/2016 07:38, Asad Ahmed wrote:
> Hi ev
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
or linking in some assembler code.
Thanks, Mark
--
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency, and focus
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 m...@proof-technologies.com wrote:
Hi Rob,
Yes, you not only need a sufficiently recent version of Camlp5 for your
version
package proof)?
Mark.
on 7/1/14 5:04 PM, Rob Arthan r...@lemma-one.com wrote:
Bill,
On 4 Jan 2014, at 05:17, Bill Richter wrote:
...
On 7 Jan 2014, at 16:22, Rob Arthan wrote:
I think we will just have to agree differ about this. Let me just make
two
comments:
Something very odd happened
BOOL_CASES_AX (using the Beeson-like
proof) instead of IMP_ANTISYM_AX (whereas HOL Light derives both). So it's
axiomatisation is between that of HOL4 and HOL Light, but somewhat closer to
HOL4's classic axiomatisation that HOL Light's.
Best,
Mark.
The source code comments explain a of what
and primitive
inference rules.
Best,
Mark.
--
Learn Graph Databases - Download FREE O'Reilly Book
Graph Databases is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders
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 m...@proof-technologies.com wrote:
... In HOL Light's axiomatisation, the only such entities are the 'bool'
and
'fun' type constants
constants 'bool' and 'fun'
are declared similarly in fusion.ml in the line that sets
'the_type_constants' (approx line 114).
Mark.
--
Learn Graph Databases - Download FREE O'Reilly Book
Graph Databases is the definitive new
.
Mark.
on 17/9/14 1:14 PM, Nela Cicmil nela.cic...@dpag.ox.ac.uk wrote:
@ Mark: I used the svn download command only this week so probably it has
the most recent version of HOL Light. On svn download, I get the output
Checked out revision 198, and the CHANGES document inside the hol_light
), and should of course be
written as this:
(\a. abs (rep a)) = \a. a
P = (\r. rep (abs r) = r)
Mark.
on 16/10/14 5:19 PM, Ramana Kumar ramana.ku...@cl.cam.ac.uk wrote:
Hi all,
There has been an interesting discussion on the OpenTheory mailing list
recently regarding how to simplify
session? Are you starting the session from scratch, or rebuilding HOL Light
on top of an existing session that had HOL Light already built?
Are you using a very recent download of HOL Light? Do you know the SVN
release number, or roughly the date you downloaded?
Mark.
on 28/5/15 7:13 PM, Robert
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 <ada.k...@qq.com>
Just to be clear, Tactician (only for HOL Light at the moment) goes between
the three styles:
- g and e
- prove with THEN/THENL/etc
- Flyspeck's 'prove_by_refinement', which is a hybrid of the above two
Mark.
on 18/11/15 8:54 AM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
>
t when you enter the
following into the ML session:
fst (1,2);
to result in
val it = 1: int
you are not doing theorem proving, you are just doing functional
programming.
Hope this makes sense.
Mark.
On 22/06/2016 09:24, Ramana Kumar wrote:
> FST is a function in logic, not in ML.
>
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 Mess
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 06/16/2016 01:45 PM
be wrong here), there is no way of getting the
HOL type system to let you express this associativity property about
'horz_conct1'. If you want to express these kinds of properties, I
think you need to define your function in a different way, not using
types like this.
Mark.
On 02/07/2016 10:30
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
problems
for the parser;
(3) Variables overloaded with constants would not get parsed properly.
But I suppose you are assuming that the original term was successfully
parsed in by HOL Light's parser. If so, then only (1) is a problem.
Mark.
But other if you are not concerned about type
of a given variable, where 'x' is the variable
name:
assoc x (map dest_var (frees th));;
Mark.
On 07/01/2018 17:36, Konrad Slind wrote:
Hi Michael,
What I think is happening is that each quoted element is being
parsed separately.
This means that the type of the x in `x` is a type
understand that, historically, it is this disadvantage of
harder proofs that was the reason for making ``0/0=0`` in HOL. It's
much easier for automated routines if they don't have to consider side
conditions.
Mark.
On 15/02/2019 08:56, Chun Tian (binghe) wrote:
Thanks to all kindly answers.
Even I
aware) by a parser generator.
http://www.proof-technologies.com/holzero/
Mark.
On 09/11/2019 15:48, Petros Papapanagiotou wrote:
Hi Brando,
The HOL4 description manual has quite a bit of information, a lot of
which is shared with HOL Light:
http://sourceforge.net/projects/hol/files/hol
, but
this would not be easy to get working as well as it does for HOL Light,
because it plays about with the innards of OCaml and equivalent tweaking
of PolyML would be required.
Mark.
On 07/08/2020 10:02, Freek Wiedijk wrote:
Dear Mario,
Hello. In HOL4 is there a way to generate something like
15 in total)
with a bit of extra work, but this is nowhere near the 100x speedup you
envisage. Would that meet your requirements? May I ask what the
application is?
Mark.
On 25/01/2021 13:40, D. J. Bernstein wrote:
I have another newbie question regarding HOL Light; again happy to hear
about other HOL
to appoint a qualified and
highly motivated researcher to work as a Research Associate. This 36 month
post is funded by two grants led by Professor Mark Batty (
m.j.ba...@kent.ac.uk): Transparent pointer safety: Rust to Lua to OS
Components from Innovate UK and Safe and secure COncurrent programming
65 matches
Mail list logo
