<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"><head><meta http-equiv=Content-Type content="text/html; charset=utf-8"><meta name=Generator content="Microsoft Word 15 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
        {font-family:"Cambria Math";
        panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
        {font-family:Calibri;
        panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0cm;
        margin-bottom:.0001pt;
        font-size:11.0pt;
        font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
        {mso-style-priority:99;
        color:blue;
        text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
        {mso-style-priority:99;
        color:#954F72;
        text-decoration:underline;}
.MsoChpDefault
        {mso-style-type:export-only;}
@page WordSection1
        {size:612.0pt 792.0pt;
        margin:70.85pt 70.85pt 2.0cm 70.85pt;}
div.WordSection1
        {page:WordSection1;}
--></style></head><body lang=DE link=blue vlink="#954F72"><div class=WordSection1><p class=MsoNormal>Hi Makarius,</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Compared to „argo“ the „smt“ method is more powerful since it supports quantifiers as well as linear natural and integer arithmetic. For the moment, argo is not capable of proving problems that require both equality reasoning and linear real arithmetic. This combination of theories is no problem for „smt“.</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>I would mark „old-smt“ as legacy for the coming release and remove it right after the release fork. Please also consider Jasmin’s opinion on this case.</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Indeed, the names sound similar, but this is a coincidence as there is no relation to „alt-ergo“.</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Cheers,</p><p class=MsoNormal>Sascha</p><p class=MsoNormal><span style='font-size:12.0pt;font-family:"Times New Roman",serif'><o:p> </o:p></span></p><div style='mso-element:para-border-div;border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm'><p class=MsoNormal style='border:none;padding:0cm'><b>Von: </b><a href="mailto:makarius@sketis.net">Makarius</a><br><b>Gesendet: </b>Samstag, 1. Oktober 2016 14:07<br><b>An: </b><a href="mailto:boehmes@in.tum.de">Sascha Boehme</a>; <a href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a><br><b>Betreff: </b>Re: [isabelle-dev] NEWS: new proof method "argo"</p></div><p class=MsoNormal><span style='font-size:12.0pt;font-family:"Times New Roman",serif'><o:p> </o:p></span></p><p class=MsoNormal>On 29/09/16 21:44, Sascha Boehme wrote:</p><p class=MsoNormal>> *** HOL ***</p><p class=MsoNormal>> </p><p class=MsoNormal>> * New proof method "argo" using the built-in Argo solver based on SMT technology.</p><p class=MsoNormal>> The method can be used to prove goals of quantifier-free propositional logic,</p><p class=MsoNormal>> goals based on a combination of quantifier-free propositional logic with equality,</p><p class=MsoNormal>> and goals based on a combination of quantifier-free propositional logic with</p><p class=MsoNormal>> linear real arithmetic including min/max/abs. See HOL/ex/Argo_Examples.thy for</p><p class=MsoNormal>> examples.</p><p class=MsoNormal>> </p><p class=MsoNormal>> This refers e.g. to Isabelle/ed98a055b9a5.</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>This looks very interesting.</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>How does it relate to "smt" (with Z3 in the back), concerning</p><p class=MsoNormal>performance and problem classes that can be solved?</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Concerning the name "argo", is the a relation to "alt-ergo"?</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>For the coming release, there is still the question what to do with</p><p class=MsoNormal>"old_smt". Shall we remove it now? Or declare it more explicitly as</p><p class=MsoNormal>legacy and remove it later?</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>           Makarius</p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><o:p> </o:p></p></div></body></html>