.
Best,
Vincent Aravantinos
--
Senior researcher - Model-based engineering tools
fortiss · An-Institut Technische Universität München
Guerickestraße 25
80805 München
Germany
Tel.: +49 (89) 3603522 33
Fax: +49 (89) 3603522 50
E-Mail: aravanti...@fortiss.org<mailto:aravanti...@fortiss.
).
--
Vincent Aravantinos
Analysis and Design of Dependable Systems
fortiss GmbH www.fortiss.org/en
Guerickestrasse 25 | 80805 Munich | Germany
Le 24 oct. 2014 à 18:16, Cvetan Dunchev dunc...@encs.concordia.ca a écrit :
Dear colleagues and friends,
I would like to inform you about
Hi,
indeed.
You can write simpler though: `real_integral (:real) f `.
Regards,
V.
--
Vincent Aravantinos
Analysis and Design of Dependable Systems
fortiss GmbH www.fortiss.org/en
Guerickestrasse 25 | 80805 Munich | Germany
- Original Message -
Dear All,
I would like to know
; REAL_ADD_SYM; REAL_LET_TRANS;
DIST_TRIANGLE_ALT]);;
Yes that is its disadvantage: that's the price you pay for getting more
intelligence from HOL Light :-)
--
Dr Vincent Aravantinos
Analysis and Design of Dependable Systems
fortiss GmbH www.fortiss.org/en
T +49 (0)89 360 35 22 33
On 14.02.2014 01:42, Michael Norrish wrote:
On 13/02/14 04:46, Vincent Aravantinos wrote:
Then considering leaving the goal unchanged, well it is a matter of taste...
I
know it is the standard to leave the goal unchanged. But I personally met
many
buggy situations that I hardly detected
; REAL_SUB_LT; REAL_LET_TRANS; ...]
DIST_TRIANGLE
Unfortunately this particular case is way too complex that
TARGET_REWRITE_TAC can handle... :-(
But it still demonstrates the motivation behind TARGET_REWRITE_TAC.
Cheers,
V.
--
Dr Vincent Aravantinos
Analysis and Design of Dependable Systems
fortiss
the tactic to be able to solve this goal, no?
And if it can't then would it not be better to leave the goal
unchanged rather than to raise an exception?
On Mon, Feb 10, 2014 at 10:31 PM, Vincent Aravantinos
vincent.aravanti...@fortiss.org
mailto:vincent.aravanti...@fortiss.org wrote:
Solved
not yet found a non-trivial example on which it does not
appear to go into an infinite loop. But I haven't looked far yet.
Cheers,
Ramana
On Tue, Jul 30, 2013 at 1:33 PM, Vincent Aravantinos
vincent.aravanti...@gmail.com mailto:vincent.aravanti...@gmail.com
wrote:
Hi Ramana,
I
So indeed, the goal is solved immediatly in HOL Light... Gonna work on
it :-/
Le 10/02/2014 18:39, Vincent Aravantinos a écrit :
Hi Ramana,
- regarding your example: no, it is not the intended behavior. I'll
have a look asap.
- regarding the infinite loop: do you mean that it goes most
Solved. The new version is uploaded:
https://github.com/aravantv/HOL4-impconv
Thanks for the report! Was indeed a mistake in the translation from
HOL-Light/Ocaml to HOL4/SML...
V.
Le 10/02/2014 21:00, Vincent Aravantinos a écrit :
So indeed, the goal is solved immediatly in HOL Light
option.) See, for example, the commands in the Holmakefile in
src/0.
Michael
PS: if you’re not on Windows, don’t use Moscow ML.
On 30 Oct 2013, at 11:03 am, Vincent Aravantinos
vincent.aravanti...@fortiss.org wrote:
Hi list,
in HOL4, I am trying to compile some utility files (i.e
the problem seems to be that I am defining a structure inside my
utility files. Can Holmake deal with this?
For information, I use MoscowML 2.10.
Thanks!
V.
--
Dr Vincent Aravantinos
Analysis and Design of Dependable Systems
fortiss GmbH www.fortiss.org/en
Guerickestrasse 25 | 80805 Munich
://pubads.g.doubleclick.net/gampad/clk?id=60135031iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
--
Vincent Aravantinos, PhD
Analysis and Design of Dependable Systems
?
On Thu, Jul 11, 2013 at 11:08 AM, Vincent Aravantinos
vincent.aravanti...@gmail.com wrote:
Hi list,
I developed a new tactic that takes a theorem of the form P == l = r and
replaces l by r in a goal adding whatever it needs to make it work properly
(typically conjunction with P; but can
/Teaching_files/zol.pdf
Ocaml source: http://users.encs.concordia.ca/~vincent/Teaching_files/zol.ml
SML source: http://users.encs.concordia.ca/~vincent/Teaching_files/zol.sml
Main page: http://users.encs.concordia.ca/~vincent/Teaching.html
Regards,
V.
--
Vincent ARAVANTINOS - PostDoctoral Fellow
is currently under review.
Regards,
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
--
See everything from the browser to the database
rewriting package has been part of HOL for many years.
Perhaps if you desire some additional functionality, it could be folded
into this package?
Cheers,
Peter
On Thu, Jul 11, 2013 at 6:08 AM, Vincent Aravantinos
vincent.aravanti...@gmail.com wrote:
Hi list,
I developed a new tactic
Forgot: in the examples below, both tactics are used with the theorem |-
!x. x 0 == x / x = 1
2013/7/11 Vincent Aravantinos vincent.aravanti...@gmail.com
Hi Peter,
here is the difference:
(* The new hypotheses are added as conjuncts rather than as a *)
(* separate subgoal
Hi Bill,
Le 2013-07-02 à 00:00, Bill Richter rich...@math.northwestern.edu a écrit :
I hope folks can help me improve my code readable.ml, which in the new
subversion 166 is in
hol_light/RichterHilbertAxiomGeometry/
1) Can you pretty-print error messages in HOL Light? E.g. here:
Am 2013-05-05 um 03:31 schrieb Ramana Kumar ramana.ku...@cl.cam.ac.uk:
On Sun, May 5, 2013 at 5:45 AM, Vincent Aravantinos
vincent.aravanti...@gmail.com wrote:
Hi Bill
2013/5/4 Bill Richter rich...@math.northwestern.edu
Question: given the string of a theorem IN_ELIM_THM, how can I
as many other tactics).
V.
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
--
Introducing AppDynamics Lite, a free troubleshooting tool
to understand what they did,
especially if we use strings, as I posted here recently, instead of
preterms.
I still don't understand why you want to avoid preterms.
--
Best,
Bill
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http
the environment?
HOL Light does a lot less than you think: it just sees a variable with
name v and type real^2, now if it sees elsewhere a variables with
the same name and same type then they are equal. As simple as that.
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware
On 04/26/2013 11:58 AM, Ramana Kumar wrote:
On Fri, Apr 26, 2013 at 4:50 PM, Vincent Aravantinos
vincent.aravanti...@gmail.com mailto:vincent.aravanti...@gmail.com
wrote:
Sure. I don't know what was the original reason for allowing two
variables of different types to have the same
have the same name but different types,
then they are different; this is really counter intuitive)
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
be doubled. If the
preterm parser was present by default in HOL Light, I could update my Pa
module to take preterms instead of strings as input, and these problems
would be solved.
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http
that ourselves?
I don't get what you mean, here...
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
--
Precog is a next-generation
the approach you suggest with option types is used?
(Preferably some elementary theory where I won't get too lost as a
non-mathematician.) This is unfamiliar to me except of course in the
programming language.
Regards,
Cris
On Thu, Apr 4, 2013 at 4:28 PM, Vincent Aravantinos
vincent.aravanti
this the right way...
--
Vincent Aravantinos
PostDoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
Am 2013-04-04 um 18:11 schrieb Cris Perdue c...@perdues.com:
Dear HOL experts,
I am hoping for wisdom and recommendations from you all related
Bill Richter rich...@math.northwestern.edu:
Vincent, you gave me a nice exercise which I'll try to work, but it dawned on
me that we can't use that unless we permanently change the parser. E.g.
every time I use miz3, I have to change the parser for that entire HOL Light
session. The
Oh, so that answers my PS, haha: that's where I saw this symbol! Sorry, I just
caught the conversation when it started to deal with types and I am not fully
aware of miz3. Then, Bill, just change the corresponding character to whatever
you want. A dot for instance.
--
Vincent Aravantinos
.
That's why in my last email, the hack I suggested was to do the work
only until this phase.
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent
`1 +
1` from being evaluated, and that was wrong. I learned about parse_term from
Freek, as a way to emulate backquotes into miz3, which doesn't allow them.
But outside of miz3, doesn't parse_term mean the same as backquotes?
Yes.
(note: I know almost nothing about miz3)
--
Vincent
exotic way if you like
(e.g., a '$' sign in the 4th position, or a # sign at every prime number
position, well whatever you like...).
Cheers,
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent
a paper on this and explain my views and the
underlying reasons in more details.
Cheers,
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent
the parser
works, but if you did, it should be straightforward.
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
--
Own the Future
require understanding how
the parser works, but if you did, it should be straightforward.
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent
\/ t2`. That's not going to be possible if HOL Light does type
inference on `t1` and `t2 before disj_term goes to work. And I'm sure from
Freek's miz3 that HOL Light does not perform such type inference.
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Great, I'll have a look, thank you all!
--
Vincent Aravantinos
PostDoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
Le 2013-03-16 à 23:16, Konrad Slind konrad.sl...@gmail.com a écrit :
Hi Vincent:
Michael has done a thorough job
Hi Ramana, sure, I'll do it asap.
Le 11/02/2013 10:15, Ramana Kumar a écrit :
Any chance you'll check this in to the HOL4 repository, Vincent?
On Sat, Dec 29, 2012 at 12:35 AM, Vincent Aravantinos
vincent.aravanti...@gmail.com mailto:vincent.aravanti...@gmail.com
wrote:
Le 28/12/12 08
, if I need it, to just translate my current HINT_EXISTS_TAC to
HOL4 (roughly nothing more than Ocaml-SML). I'll have a look at
quantHeuristicsLib when I get the time though, because maybe the
my problem will actually happen to be useless in the end.
Thanks,
V.
--
Vincent ARAVANTINOS
GEN_HINT_EXISTS_TAC not
applicable
|_ = failwith GEN_HINT_EXISTS_TAC not applicable
in
(EXISTS_TAC witness THEN ASM_REWRITE_TAC[]) g
end;
Cheers,
V.
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http
, using my phone.
On Dec 26, 2012 10:57 PM, Vincent Aravantinos
vincent.aravanti...@gmail.com
mailto:vincent.aravanti...@gmail.com wrote:
Hi list,
here is another situation which I don't like and often meet (both in
HOL-Light and HOL4), and a potential solution.
Please tell me
the goal,
it can also be used just to make progress in the proof without necessary
concluding.
*)
A HOL-Light implementation for HINT_EXISTS_TAC is provided below the
signature.
One for HOL4 can easily be implemented if anyone expresses some interest
for it.
Cheers,
V.
--
Vincent
unabbreviated after.
HINT_EXISTS_TAC might still be an improvement.
Sorry for no proper backquotes, using my phone.
On Dec 26, 2012 10:57 PM, Vincent Aravantinos
vincent.aravanti...@gmail.com mailto:vincent.aravanti...@gmail.com
wrote:
Hi list,
here is another situation which I don't
. It seems you
have
to load it before opening it. There is documentation in
src/1/dep_rewrite.sml
in the distribution.
Cheers,
Konrad.
On Thu, Nov 22, 2012 at 2:31 PM, Vincent Aravantinos
vincent.aravanti...@gmail.com mailto:vincent.aravanti...@gmail.com
wrote:
Hi list,
I often face
://code.google.com/p/flyspeck/downloads/list
If you are interested, read the description of the rewrite tactic in
the SSReflect/HOL Light manual.
Best,
Alexey
On 11/22/2012 3:31 PM, Vincent Aravantinos wrote:
Hi list,
I often face the following small but annoying problem:
* Situation:
- I
, Vincent Aravantinos wrote:
Hi list,
I often face the following small but annoying problem:
* Situation:
- I have a theorem (say, Th) of the form P == t = u
ex: REAL_DIV_REFL
(|- !x. ~(x =0) == x / x =1 in HOL-Light, |- !x. x 0 == (x
/ x = 1) in HOL4)
- the conclusion of my
`
(in this case, the application of the tactic will diverge).
Le 26/11/2012 19:30, Vincent Aravantinos a écrit :
Hi Michael,
Another possibility to solve this problem is to add the required
assumption as a conjunction with the atomic proposition in which the
rewrite occurs.
For instance `!x. x 0
x =
REWRITE_TAC[MP (!th) x] THEN STRIP_ASSUME_TAC x)) g
end;
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
--
Monitor your
for 25 servers or applications!
http://p.sf.net/sfu/zoho_dev2dev_nov
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware
CARD_CLAUSES)) FINITE_EMPTY;
CARD_CLAUSES;NOT_IN_EMPTY]);;
At least for me it has been standard practice to build my own little
libraries of lemmas to make reasoning about a particular theory easier
and more tailored to my needs.
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University
+ 1`;;
Exception: Failure typechecking error (overload resolution).
Best regards,
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
be enough to just provide x and HOL
Light would find out the type of x from the context.
Thanks,
V.
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent
Le 24/10/12 14:58, Vincent Aravantinos a écrit :
does anybody know of something providing in HOL-Light the same
functionality as the Q module in HOL4?
It was actually easy to define mine, see
http://users.encs.concordia.ca/~vincent/Software_files/q.ml if interested.
Summary:
The module
#toc77) or
aliasing
(http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc74) of
modules. But both seem incompatible with the current camlp5 extension
used by HOL Light.
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware Verification Group
http
) or
aliasing
(http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc74) of
modules. But both seem incompatible with the current camlp5 extension
used by HOL Light.
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca
from Thierry Coquand's name?
Coq is both a reference to the Calculus of Constructions (CoC)
which is the type system underlying Coq, and a kind of tribute to
Thierry Coquand who introduced this type system.
--
Vincent Aravantinos
PostDoctoral fellow, Concordia University, Hardware
overload it: *)
# overload_interface(inv,`inv:real-real`);;
val it : unit = ()
--
Vincent Aravantinos
PostDoctoral fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
Le 14 mai 12 à 22:53, Bill Richter a écrit :
Trying to improve my group theory code, I
OLIBDIR=C:\cygwin\opt\lib\ocaml
BINDIR=/usr/bin
LIBDIR=C:\cygwin\opt\lib\ocaml
MANDIR=/usr/man
=== strict mode ===
1. add C:\cygwin\lib\ocaml to path
then I get the same error again..
On 15 March 2012 03:51, Vincent Aravantinos
vincent.aravanti...@gmail.comwrote:
Adding
60 matches
Mail list logo
