The line you saw is just internal logging of the Metis search for a proof. It
can be nice to see that it is still doing something by watching that output.
(Normally, you should just give up if there is too much logging and the goal is
not proved very quickly.)
Michael
On 12 Apr 2015, at 10:39, Ada <[email protected]<mailto:[email protected]>> wrote:
Hey guys,
I am learning to use HOL. When I use METIS_TAC, I don't know the system's
response.
For example:
what I input are:
-open arithmeticTheory;
-val divides_def = Define `divides a b = ?x. b = a * x`;
-set_fixity "divides" (Infix(NONASSOC,450));
-g`!x.x divides 0`;
-e(METIS_TAC [divides_def,MULT_CLAUSES]);
Finally,what system response is:
OK..
metis: r[+0+10]+0+0+0+1+2#
> val it =
Initial goal proved.
|- !x. x divides 0 : proof
* Does anyone know what is the meaning of metis: r[+0+10]+0+0+0+1+2# ?
Thanks! --Wish.
------------------------------------------------------------------------------
BPM Camp - Free Virtual Workshop May 6th at 10am PDT/1PM EDT
Develop your own process in accordance with the BPMN 2 standard
Learn Process modeling best practices with Bonita BPM through live exercises
http://www.bonitasoft.com/be-part-of-it/events/bpm-camp-virtual- event?utm_
source=Sourceforge_BPM_Camp_5_6_15&utm_medium=email&utm_campaign=VA_SF
_______________________________________________
hol-info mailing list
[email protected]<mailto:[email protected]>
https://lists.sourceforge.net/lists/listinfo/hol-info
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
BPM Camp - Free Virtual Workshop May 6th at 10am PDT/1PM EDT
Develop your own process in accordance with the BPMN 2 standard
Learn Process modeling best practices with Bonita BPM through live exercises
http://www.bonitasoft.com/be-part-of-it/events/bpm-camp-virtual- event?utm_
source=Sourceforge_BPM_Camp_5_6_15&utm_medium=email&utm_campaign=VA_SF
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
