Document Zbl 07757157

<!doctype html> <html lang="en"> <head> <meta charset="utf-8"> <title>Document Zbl 07757157 - zbMATH Open</title> <meta name="viewport" content="width=device-width, minimum-scale=0.1, maximum-scale=5.0"> <meta name="robots" content="noarchive, noindex"> <meta name="referrer" content="origin-when-cross-origin"> <link href="https://static.zbmath.org/contrib/bootstrap/v3.3.7/css/bootstrap.min.css" rel="stylesheet" media="screen,print"> <link href="https://static.zbmath.org/contrib/bootstrap/v3.3.7/css/bootstrap-theme.min.css" rel="stylesheet" media="screen,print"> <link href="https://static.zbmath.org/contrib/bootstrap-lightbox/v0.7.0/bootstrap-lightbox.min.css" rel="stylesheet" media="screen,print"> <link rel="stylesheet" href="https://static.zbmath.org/contrib/bootstrap-select/v1.13.14/css/bootstrap-select.min.css"> <link href="/static/css/smoothness/jquery-ui-1.10.1.custom.min.css" rel="stylesheet" media="screen"> <link href="/static/styles.css?v=20241024" rel="stylesheet" media="screen,print"> <link href="https://static.zbmath.org/zbMathJax/v0.1.38/zbmathjax.css" rel="stylesheet" media="screen,print"> <link rel="shortcut icon" href="/static/zbmath.ico"> <script type="application/ld+json"> { "@context": "http://schema.org", "@type": "Organization", "url": "https://zbmath.org/", "logo": "https://zbmath.org/static/zbMATH.png" } </script> </head> <body> <div id="line"></div> <span id="clear" style="cursor: pointer;">×</span> <div id="page"> <div id="head"> <nav id="menu" class="navbar navbar-default"> <div class="container-fluid"> <div class="navbar-header"> <button type="button" class="navbar-toggle collapsed" data-toggle="collapse" data-target="#zbnav" aria-expanded="false"> <span class="sr-only">Toggle navigation</span> <span class="icon-bar"></span> <span class="icon-bar"></span> <span class="icon-bar"></span> </button> <a class="navbar-brand" href="#"> <img class="logo" src="/static/zbmath.gif" alt="zbMATH Open logo"> </a> </div> <div id="zbnav" class="collapse navbar-collapse"> <ul class="nav navbar-nav pages"> <li class="about"> <a href="/about/">About</a> </li> <li class="frequently-asked-questions"> <a href="/frequently-asked-questions/">FAQ</a> </li> <li class="general-help"> <a href="/general-help/">General Help</a> </li> <li class="reviewer-service"> <a href="https://zbmath.org/reviewer-service/" target="_self" >Reviewer Service</a> </li> <li> <a href="/tools-and-resources/">Tools & Resources</a> </li> <li class="contact"> <a href="/contact/">Contact</a> </li> </ul> <ul class="nav navbar-nav navbar-right prefs"> <li class="preferences dropdown"> <a data-toggle="dropdown" href="#">Preferences <i class="caret"></i></a> <ul class="dropdown-menu preferences"> <li> <form id="preferences" class="navbar-form" method="post" action="/preferences/" onsubmit="return confirm('This website uses cookies for the purposes of storing preference information on your device. Do you agree to this?\n\nPlease refer to our Privacy Policy to learn more about our use of cookies.')" > <input type="hidden" name="path" value="/?q=ra%3Azhou.lu+se%3A1839"> <span class=""> <label class="title">Search Form</label> <div class="form-group"> <input id="search-multi-line" type="radio" name="search" value="multi-line" checked> <label for="search-multi-line" class="radio">Multi-Line Search (default)</label> </div> <div class="form-group"> <input id="search-one-line" type="radio" name="search" value="one-line"> <label for="search-one-line" class="radio">One-Line Search</label> </div> </span> <span class="count"> <label class="title">Hits per Page</label> <div class="form-group"> <input id="count-10" type="radio" name="count" value="10"> <label for="count-10" class="radio">10</label> </div> <div class="form-group"> <input id="count-20" type="radio" name="count" value="20"> <label for="count-20" class="radio">20</label> </div> <div class="form-group"> <input id="count-50" type="radio" name="count" value="50"> <label for="count-50" class="radio">50</label> </div> <div class="form-group"> <input id="count-100" type="radio" name="count" value="100" checked> <label for="count-100" class="radio">100 (default)</label> </div> <div class="form-group"> <input id="count-200" type="radio" name="count" value="200"> <label for="count-200" class="radio">200</label> </div> </span> <span class="format"> <label class="title">Display Format</label> <div class="form-group"> <input id="format-mathjax" type="radio" name="format" value="mathjax" checked> <label for="format-mathjax" class="radio">MathJax (default)</label> </div> <div class="form-group"> <input id="format-amstex" type="radio" name="format" value="latex"> <label for="format-amstex" class="radio">LaTeX</label> </div> </span> <span class="ranking"> <label class="title">Documents Sorting</label> <div class="form-group"> <input id="documents-ranking-default" type="radio" name="documents_ranking" value="date" checked> <label for="documents-ranking-default" class="radio">Newest first (default)</label> </div> <div class="form-group"> <input id="documents-ranking-references" type="radio" name="documents_ranking" value="references"> <label for="documents-ranking-references" class="radio">Citations</label> </div> <div class="form-group"> <input id="documents-ranking-relevance" type="radio" name="documents_ranking" value="relevance"> <label for="documents-ranking-relevance" class="radio">Relevance</label> </div> </span> <span class="ranking"> <label class="title">Authors Sorting</label> <div class="form-group"> <input id="authors-ranking-default" type="radio" name="authors_ranking" value="alpha" checked> <label for="authors-ranking-default" class="radio">Alphabetically (default)</label> </div> <div class="form-group"> <input id="authors-ranking-references" type="radio" name="authors_ranking" value="references"> <label for="authors-ranking-references" class="radio">Citations</label> </div> </span> <span class="ranking"> <label class="title">Serials Sorting</label> <div class="form-group"> <input id="serials-ranking-default" type="radio" name="serials_ranking" value="alpha" checked> <label for="serials-ranking-default" class="radio">Alphabetically (default)</label> </div> <div class="form-group"> <input id="serials-ranking-references" type="radio" name="serials_ranking" value="references"> <label for="serials-ranking-references" class="radio">Citations</label> </div> </span> <span class="ranking"> <label class="title">Software Sorting</label> <div class="form-group"> <input id="software-ranking-default" type="radio" name="software_ranking" value="references" checked> <label for="software-ranking-default" class="radio">Citations (default)</label> </div> <div class="form-group"> <input id="software-ranking-alpha" type="radio" name="software_ranking" value="alpha"> <label for="software-ranking-alpha" class="radio">Alphabetically</label> </div> </span> <button type="submit" class="btn btn-default">OK</button> <div class="clearfix"> </form> </li> </ul> </li> </ul> </div> </div> </nav> <div id="tabs"> <h1 class="logo"> <a class="logo" href="/"> <img class="logo" src="/static/zbmath.gif" alt="zbMATH Open — the first resource for mathematics" > </a> </h1> <nav> <ul class="nav nav-tabs"> <li class="tab-documents active"> <a href="/">Documents</a> </li> <li class="tab-authors"> <a href="/authors/">Authors</a> </li> <li class="tab-serials"> <a href="/serials/">Serials</a> </li> <li class="tab-software"> <a href="/software/">Software</a> </li> <li class="tab-classification"> <a href="/classification/">Classification</a> </li> <li class="tab-formulae"> <a href="/formulae/">Formulæ</a> </li> </ul> </nav> <div class="clearfix"></div> </div> <div class="content-fixed"> <div class="content-formular"> <div style="display: none;"> <div class="row ml-0"id="multi-line-new-line" style="display: none;"> <div class="col-xs-12 form-inline multi-line"> <select class="form-control multi-line-field multi-line-selectpicker" name="ml-0-f" aria-label="field"> <option data-type="input" value="any" selected>Anywhere</option> <option data-type="input" value="au">Authors</option> <option data-type="input" value="ti">Title</option> <option data-type="input" value="py">Year</option> <option data-type="range" value="pyr">Year Range</option> <option data-type="input" value="cc">MSC</option> <option data-type="input" value="cc1">MSC Primary</option> <option data-type="input" value="so">Source / Journal</option> <option data-type="input" value="pu">Publisher</option> <option data-type="input" value="la">Language</option> <option data-type="input" value="ab">Summary / Review</option> <option data-type="input" value="rv">Reviewer</option> <option data-type="input" value="an">zbMATH ID</option> <option data-type="input" value="en">External ID</option> <option data-type="input" value="ut">Keywords</option> <option data-type="input" value="sw">Software</option> <option data-type="input" value="br">Biographic Ref</option> <option data-type="input" value="rft">Reference Text</option> <option data-type="multiselect-db" value="db">Database</option> <option data-divider="true"></option> <option data-function="remove-line" data-content='<span class="glyphicon glyphicon-minus" aria-hidden="true"></span> remove line' value="any">remove line</option> </select><input name="ml-0-v" class="form-control multi-line-value multi-line-input" type="text" value="" aria-label="value"><select class="form-control multi-line-operators multi-line-selectpicker" name="ml-0-op" aria-label="operator"> <option value="and" selected>AND</option> <option value="andnot">AND NOT</option> <option value="or">OR</option> </select></div> </div> <input name="ml-0-v" class="form-control multi-line-value multi-line-input" type="text" value="" aria-label="value" id="multi-line-type-input"> <span class="multi-line-value" id="multi-line-type-range"><span style="padding-left: 5px;">from</span> <input name="ml-0-v1" class="form-control multi-line-input" type="text" value="" aria-label="value"> until <input name="ml-0-v2" class="form-control multi-line-input" type="text" value="" aria-label="value"></span> <input name="ml-0-v" class="form-control multi-line-value multi-line-input" type="text" value="" aria-label="value" id="multi-line-type-input-la" placeholder="use name or ISO code"> <input name="ml-0-v" class="form-control multi-line-value multi-line-input" type="text" value="" aria-label="value" id="multi-line-type-input-rv" placeholder="enter name or zbMATH reviewer number"> <input name="ml-0-v" class="form-control multi-line-value multi-line-input" type="text" value="" aria-label="value" id="multi-line-type-input-an" placeholder="Zbl, JFM or ERAM number"> <input name="ml-0-v" class="form-control multi-line-value multi-line-input" type="text" value="" aria-label="value" id="multi-line-type-input-en" placeholder="e.g. DOI, ISBN, arXiv ID"> <input name="ml-0-v" class="form-control multi-line-value multi-line-input" type="text" value="" aria-label="value" id="multi-line-type-input-sw" placeholder="use * to find all documents using software"> <input name="ml-0-v" class="form-control multi-line-value multi-line-input" type="text" value="" aria-label="value" id="multi-line-type-input-br" placeholder="find documents about the life or work of a person"> <span class="multi-line-value" id="multi-line-type-multiselect-db"> <select class="multi-line-selectpicker" data-width="100%" multiple> <option value="zbl">Zbl</option> <option value="arxiv">arXiv</option> <option value="jfm">JFM</option> <option value="eram">ERAM</option> </select> <input type="hidden" class="multi-line-input" name="ml-0-v" value=""> </span> </div> <form name="documents" method="GET" action="/" autocomplete="off"> <div class="documents multi-line" style="display: none;"> <div class="forms"> <ul class="nav forms"> <li class="one-line"> <span tabindex="0" class="glyphicon glyphicon-question-sign" title="One-Line Search allows for free logical combinations of search fields" aria-label="One-Line Search allows for free logical combinations of search fields" data-placement="bottom"></span> <a style="display: inline-block;" href="#">One-Line Search <span class="glyphicon glyphicon-search"></span></a> </li> </ul> </div> <div class="clearfix"></div> <div class="container-fluid"> <input type="hidden" id="multi-line-ml" name="ml" value="3"> <div id="multi-line-row-wrapper"> <div class="row ml-1"> <div class="col-xs-12 form-inline multi-line"> <select class="form-control multi-line-field multi-line-selectpicker" name="ml-1-f" aria-label="field"> <option data-type="input" value="any" selected>Anywhere</option> <option data-type="input" value="au">Authors</option> <option data-type="input" value="ti">Title</option> <option data-type="input" value="py">Year</option> <option data-type="range" value="pyr">Year Range</option> <option data-type="input" value="cc">MSC</option> <option data-type="input" value="cc1">MSC Primary</option> <option data-type="input" value="so">Source / Journal</option> <option data-type="input" value="pu">Publisher</option> <option data-type="input" value="la">Language</option> <option data-type="input" value="ab">Summary / Review</option> <option data-type="input" value="rv">Reviewer</option> <option data-type="input" value="an">zbMATH ID</option> <option data-type="input" value="en">External ID</option> <option data-type="input" value="ut">Keywords</option> <option data-type="input" value="sw">Software</option> <option data-type="input" value="br">Biographic Ref</option> <option data-type="input" value="rft">Reference Text</option> <option data-type="multiselect-db" value="db">Database</option> <option data-divider="true"></option> <option data-function="remove-line" data-content='<span class="glyphicon glyphicon-minus" aria-hidden="true"></span> remove line' value="any">remove line</option> </select><input name="ml-1-v" class="form-control multi-line-value multi-line-input" type="text" value="" aria-label="value"><select class="form-control multi-line-operators multi-line-selectpicker" name="ml-1-op" aria-label="operator"> <option value="and" selected>AND</option> <option value="andnot">AND NOT</option> <option value="or">OR</option> </select></div> </div> <div class="row ml-2"> <div class="col-xs-12 form-inline multi-line"> <select class="form-control multi-line-field multi-line-selectpicker" name="ml-2-f" aria-label="field"> <option data-type="input" value="any">Anywhere</option> <option data-type="input" value="au" selected>Authors</option> <option data-type="input" value="ti">Title</option> <option data-type="input" value="py">Year</option> <option data-type="range" value="pyr">Year Range</option> <option data-type="input" value="cc">MSC</option> <option data-type="input" value="cc1">MSC Primary</option> <option data-type="input" value="so">Source / Journal</option> <option data-type="input" value="pu">Publisher</option> <option data-type="input" value="la">Language</option> <option data-type="input" value="ab">Summary / Review</option> <option data-type="input" value="rv">Reviewer</option> <option data-type="input" value="an">zbMATH ID</option> <option data-type="input" value="en">External ID</option> <option data-type="input" value="ut">Keywords</option> <option data-type="input" value="sw">Software</option> <option data-type="input" value="br">Biographic Ref</option> <option data-type="input" value="rft">Reference Text</option> <option data-type="multiselect-db" value="db">Database</option> <option data-divider="true"></option> <option data-function="remove-line" data-content='<span class="glyphicon glyphicon-minus" aria-hidden="true"></span> remove line' value="any">remove line</option> </select><input name="ml-2-v" class="form-control multi-line-value multi-line-input" type="text" value="" aria-label="value"><select class="form-control multi-line-operators multi-line-selectpicker" name="ml-2-op" aria-label="operator"> <option value="and" selected>AND</option> <option value="andnot">AND NOT</option> <option value="or">OR</option> </select></div> </div> <div class="row ml-3"> <div class="col-xs-12 form-inline multi-line"> <select class="form-control multi-line-field multi-line-selectpicker" name="ml-3-f" aria-label="field"> <option data-type="input" value="any">Anywhere</option> <option data-type="input" value="au">Authors</option> <option data-type="input" value="ti" selected>Title</option> <option data-type="input" value="py">Year</option> <option data-type="range" value="pyr">Year Range</option> <option data-type="input" value="cc">MSC</option> <option data-type="input" value="cc1">MSC Primary</option> <option data-type="input" value="so">Source / Journal</option> <option data-type="input" value="pu">Publisher</option> <option data-type="input" value="la">Language</option> <option data-type="input" value="ab">Summary / Review</option> <option data-type="input" value="rv">Reviewer</option> <option data-type="input" value="an">zbMATH ID</option> <option data-type="input" value="en">External ID</option> <option data-type="input" value="ut">Keywords</option> <option data-type="input" value="sw">Software</option> <option data-type="input" value="br">Biographic Ref</option> <option data-type="input" value="rft">Reference Text</option> <option data-type="multiselect-db" value="db">Database</option> <option data-divider="true"></option> <option data-function="remove-line" data-content='<span class="glyphicon glyphicon-minus" aria-hidden="true"></span> remove line' value="any">remove line</option> </select><input name="ml-3-v" class="form-control multi-line-value multi-line-input" type="text" value="" aria-label="value"><div id="multi-line-plus"> <a href="#"><span class="glyphicon glyphicon-plus" aria-hidden="true"></span> add line</a> </div></div> </div> </div> <div class="row"> <div class="col-xs-12 form-inline"> <div class="form-group field checkboxes-wrapper" id="checkboxes-wrapper-test" style="visibility: hidden; position: fixed;"> <label>Document Type:</label> <div class="checkboxes"> <div class="slider"> <label title="search for Articles in Journals"> <input type="checkbox" class="form-control" value="j" checked> <span tabindex="0"><small></small></span> Journal Articles </label> </div> <div class="slider"> <label title="search for Articles in Conference Proceedings and Collected Volumes"> <input type="checkbox" class="form-control" value="a" checked> <span tabindex="0"><small></small></span> Collection Articles </label> </div> <div class="slider"> <label title="search for Monographs, Proceedings, Dissertations etc."> <input type="checkbox" class="form-control" value="b" checked> <span tabindex="0"><small></small></span> Books </label> </div> <div class="slider"> <label title="search for arXiv Preprints"> <input type="checkbox" class="form-control" value="p" checked> <span tabindex="0"><small></small></span> arXiv Preprints </label> </div> </div> </div> <div class="form-group field checkboxes-wrapper" id="checkboxes-wrapper-real"> <label>Document Type:</label> <div class="checkboxes"> <div class="slider"> <label for="dt-j" title="search for Articles in Journals"> <input type="checkbox" id="dt-j" name="dt" class="form-control" value="j" checked> <span tabindex="0"><small></small></span> Journal Articles </label> </div> <div class="slider"> <label for="dt-a" title="search for Articles in Conference Proceedings and Collected Volumes"> <input type="checkbox" id="dt-a" name="dt" class="form-control" value="a" checked> <span tabindex="0"><small></small></span> Collection Articles </label> </div> <div class="slider"> <label for="dt-b" title="search for Monographs, Proceedings, Dissertations etc."> <input type="checkbox" id="dt-b" name="dt" class="form-control" value="b" checked> <span tabindex="0"><small></small></span> Books </label> </div> <div class="slider"> <label for="dt-p" title="search for arXiv Preprints"> <input type="checkbox" id="dt-p" name="dt" class="form-control" value="p" checked> <span tabindex="0"><small></small></span> arXiv Preprints </label> </div> </div> </div> </div> </div> <div class="row"> <div class="col-xs-12 buttons"> <a tabindex="0" class="btn btn-default clear-all">Reset all <span class="glyphicon glyphicon-remove"></span></a> <div class="submit"> <button class="btn btn-default search" type="submit">Search <span class="glyphicon glyphicon-search"></span></button> </div> </div> </div> </div> </div> </form> <form class="form-inline" name="documents" method="GET" action="/"> <div class="documents one-line" style="display: block;"> <div class="forms"> <ul class="nav forms"> <li class="multi-line"><a href="#">New Multi-Line Search <span class="glyphicon glyphicon-list"></span></a></li> </ul> </div> <div id="search-row" class="input-group box"> <span> <div id="search-field"> <input class="query form-control" type="text" name="q" value="ra:zhou.lu se:1839" aria-label="Search for documents" placeholder="Search for documents" autocomplete="off"> </div> <div class="search-buttons input-group-btn"> <div class="btn-group"> <button class="btn btn-default search" type="submit"><span class="virtual">Search</span> <span class="glyphicon glyphicon-search" style="top: 2px;"></span></button> </div> </div> </span> <span> <div class="search-buttons input-group-btn"> <div class="btn-group"> <div class="btn-group fields"> <button class="btn btn-default dropdown-toggle" data-toggle="dropdown">Fields <i class="caret"></i></button> <ul id="fields" class="dropdown-menu pull-right"> <li><a href="#"><span class="token item">any:</span><span> </span>anywhere (default)</a></li> <li><a href="#"><span class="token item">ab:</span><span>  </span>review text</a></li> <li><a href="#"><span class="token item">an:</span><span>  </span>zbmath id</a></li> <li><a href="#"><span class="token item">any:</span><span>  </span>anywhere</a></li> <li><a href="#"><span class="token item">au:</span><span>  </span>contributor name</a></li> <li><a href="#"><span class="token item">br:</span><span>  </span>biographic reference name</a></li> <li><a href="#"><span class="token item">cc:</span><span>  </span>msc title</a></li> <li><a href="#"><span class="token item">dt:</span><span>  </span>document type</a></li> <li><a href="#"><span class="token item">doi:</span><span>  </span>doi</a></li> <li><a href="#"><span class="token item">en:</span><span>  </span>external id</a></li> <li><a href="#"><span class="token item">la:</span><span>  </span>language</a></li> <li><a href="#"><span class="token item">pu:</span><span>  </span>publisher</a></li> <li><a href="#"><span class="token item">py:</span><span>  </span>year</a></li> <li><a href="#"><span class="token item">rv:</span><span>  </span>reviewer name</a></li> <li><a href="#"><span class="token item">so:</span><span>  </span>source</a></li> <li><a href="#"><span class="token item">sw:</span><span>  </span>software name</a></li> <li><a href="#"><span class="token item">ti:</span><span>  </span>title</a></li> <li><a href="#"><span class="token item">ut:</span><span>  </span>keyword</a></li> </ul> </div> <div class="btn-group operators"> <button class="btn btn-default dropdown-toggle" data-toggle="dropdown">Operators <i class="caret"></i></button> <ul id="operators" class="dropdown-menu pull-right"> <li><a href="#"><span class="token">a <span class="item">&</span> b </span><span> </span>logical and (default)</a></li> <li><a href="#"><span class="token">a <span class="item">|</span> b </span><span> </span>logical or</a></li> <li><a href="#"><span class="token"><span class="item">!</span>ab   </span><span> </span>logical not</a></li> <li><a href="#"><span class="token">abc<span class="item">*</span>  </span><span> </span>right wildcard</a></li> <li><a href="#"><span class="token"><span class="item">"</span>ab c<span class="item">"</span></span><span> </span>phrase</a></li> <li><a href="#"><span class="token"><span class="item">(</span>ab c<span class="item">)</span></span><span> </span>parentheses</a></li> </ul> </div> </div> </div> <div class="special"> <ul class="nav help-button"> <li class="dropdown pull-right"> <a href="#">Help <i class="caret"></i></a> </li> </ul> </div> </span> </div> <div class="help"><h2>Examples</h2> <div id="help-terms" role="table"> <div class="help-item" role="row"> <span class="search-example" role="rowheader"><a href="/?q=Geometry">Geometry</a></span> <span class="search-explanation" role="cell" role="cell">Search for the term <em>Geometry</em> in <strong>any</strong> field. Queries are <strong>case-independent</strong>.</span> </div> <div class="help-item" role="row"> <span class="search-example" role="rowheader"><a href="/?q=Funct%2A">Funct*</a></span> <span class="search-explanation" role="cell"><strong>Wildcard</strong> queries are specified by <strong><u>*</u></strong> (e.g. <em>functions</em>, <em>functorial</em>, etc.). Otherwise the search is <strong>exact</strong>.</span> </div> <div class="help-item" role="row"> <span class="search-example" role="rowheader"><a href="/?q=%22Topological+group%22">"Topological group"</a></span> <span class="search-explanation" role="cell"><strong>Phrases</strong> (multi-words) should be set in <u>"</u>straight quotation marks<u>"</u>.</span> </div> <div class="help-item" role="row"> <span class="search-example" role="rowheader"><a href="/?q=au%3A+Bourbaki+%26+ti%3A+Algebra">au: Bourbaki & ti: Algebra</a></span> <span class="search-explanation" role="cell">Search for <strong><u>au</u>thor</strong> and <strong><u>ti</u>tle</strong>. The <strong>and-operator &</strong> is default and can be omitted.</span> </div> <div class="help-item" role="row"> <span class="search-example" role="rowheader"><a href="/?q=Chebyshev+%7C+Tschebyscheff">Chebyshev | Tschebyscheff</a></span> <span class="search-explanation" role="cell">The <strong>or-operator |</strong> allows to search for <em>Chebyshev</em> or <em>Tschebyscheff</em>.</span> </div> <div class="help-item" role="row"> <span class="search-example" role="rowheader"><a href="/?q=Quasi%2A+map%2A+py%3A+1989">Quasi* map* py: 1989</a></span> <span class="search-explanation" role="cell">The resulting documents have <strong><u>p</u>ublication <u>y</u>ear</strong> <em>1989</em>.</span> </div> <div class="help-item" role="row"> <span class="search-example" role="rowheader"><a href="/?q=so%3A+Eur%2A+J%2A+Mat%2A+Soc%2A+cc%3A+14">so: Eur* J* Mat* Soc* cc: 14</a></span> <span class="search-explanation" role="cell">Search for publications in a particular <strong><u>so</u>urce</strong> with a <strong>Mathematics Subject <u>C</u>lassification <u>c</u>ode (<u>cc</u>)</strong> in <em>14</em>.</span> </div> <div class="help-item" role="row"> <span class="search-example" role="rowheader"><a href="/?q=%22Partial+diff%2A+eq%2A%22+%21+elliptic">"Partial diff* eq*" ! elliptic</a></span> <span class="search-explanation" role="cell">The <strong>not</strong>-operator <strong>!</strong> eliminates all results containing the word <em>elliptic</em>.</span> </div> <div class="help-item" role="row"> <span class="search-example" role="rowheader"><a href="/?q=dt%3A+b+%26+au%3A+Hilbert">dt: b & au: Hilbert</a></span> <span class="search-explanation" role="cell">The <strong><u>d</u>ocument <u>t</u>ype</strong> is set to books; alternatively: <u>j</u> for <strong>journal articles</strong>, <u>a</u> for <strong>book articles</strong>.</span> </div> <div class="help-item" role="row"> <span class="search-example" role="rowheader"><a href="/?q=py%3A+2000-2015+cc%3A+%2894A+%7C+11T%29">py: 2000-2015 cc: (94A | 11T)</a></span> <span class="search-explanation" role="cell">Number <strong>ranges</strong> are accepted. Terms can be grouped within <strong><u>(</u>parentheses<u>)</u></strong>.</span> </div> <div class="help-item" role="row"> <span class="search-example" role="rowheader"><a href="/?q=la%3A+chinese">la: chinese</a></span> <span class="search-explanation" role="cell">Find documents in a given <strong><u>la</u>nguage</strong>. <a href="http://en.wikipedia.org/wiki/ISO_639-1">ISO 639-1</a> language codes can also be used.</span> </div> </div> <div id="help-fields"> <h2>Fields</h2> <table> <tr> <td class="nowrap padding" role="rowheader"><strong>any</strong></td> <td class="padding">anywhere</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>an</strong></td> <td class="padding">internal document identifier</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>au</strong></td> <td class="padding">author, editor</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>ai</strong></td> <td class="padding">internal author identifier</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>ti</strong></td> <td class="padding">title</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>la</strong></td> <td class="padding">language</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>so</strong></td> <td class="padding">source</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>ab</strong></td> <td class="padding">review, abstract</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>py</strong></td> <td class="padding">publication year</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>rv</strong></td> <td class="padding">reviewer</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>cc</strong></td> <td class="padding">MSC code</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>ut</strong></td> <td class="padding">uncontrolled term</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>dt</strong></td> <td class="padding" colspan="4">document type (<strong>j</strong>: journal article; <strong>b</strong>: book; <strong>a</strong>: book article)</td> </tr> </table> </div> <div id="help-operators"> <h2>Operators</h2> <table> <tr> <td class="nowrap padding" role="rowheader">a <strong>&</strong> b</td> <td class="padding">logic and</td> </tr> <tr> <td class="nowrap padding" role="rowheader">a <strong>|</strong> b</td> <td class="padding">logic or</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>!</strong>ab</td> <td class="padding">logic not</td> </tr> <tr> <td class="nowrap padding" role="rowheader">abc<strong>*</strong></td> <td class="padding">right wildcard</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>"</strong>ab c<strong>"</strong></td> <td class="padding">phrase</td> </tr> <tr> <td class="nowrap padding" role="rowheader"><strong>(</strong>ab c<strong>)</strong></td> <td class="padding">parentheses</td> </tr> </table> </div> <p> See also our <a href="/general-help/">General Help</a>. </p></div> </div> </form> <div class="clearfix"></div> </div> <div class="content-shadow"></div> </div> </div> <div id="body"> <div id="main"> <div class="messages"> </div> <div id="documents"> <div class="content-main"> <div class="content-item"><div class="item"> <article> <div class="author"><a href="/authors/ganesh.vijay" title="Author Profile">Ganesh, Vijay</a>; <a href="/authors/seshia.sanjit-arunkumar" title="Author Profile">Seshia, Sanjit A.</a>; <a href="/authors/jha.somesh" title="Author Profile">Jha, Somesh</a></div> <h2 class="title"> <strong>Machine learning and logic: a new frontier in artificial intelligence.</strong> <i>(English)</i> <a class="label nowrap" href="/7757157">Zbl 07757157</a> </h2> <div class="source"> <a href="/serials/1839" title="Journal Profile">Form. Methods Syst. Des.</a> <a href="/?q=in%3A503753" title="Articles in this Issue">60, No. 3, 426-451 (2022)</a>. </div> <div class="abstract">Summary: Machine learning and logical reasoning have been the two foundational pillars of Artificial Intelligence (AI) since its inception, and yet, until recently the interactions between these two fields have been relatively limited. Despite their individual success and largely independent development, there are new problems on the horizon that seem solvable only via a combination of ideas from these two fields of AI. These problems can be broadly characterized as follows: how can learning be used to make logical reasoning and synthesis/verification engines more efficient and powerful, and in the reverse direction, how can we use reasoning to improve the accuracy, generalizability, and trustworthiness of learning. In this perspective paper, we address the above-mentioned questions with an emphasis on certain paradigmatic trends at the intersection of learning and reasoning. Our intent here is not to be a comprehensive survey of all the ways in which learning and reasoning have been combined in the past. Rather we focus on certain recent paradigms where <span class="zbmathjax-textit">corrective feedback loops</span> between learning and reasoning seem to play a particularly important role. Specifically, we observe the following three trends: first, the use of learning techniques (especially, reinforcement learning) in sequencing, selecting, and initializing proof rules in solvers/provers; second, combinations of inductive learning and deductive reasoning in the context of program synthesis and verification; and third, the use of solver layers in providing corrective feedback to machine learning models in order to help improve their accuracy, generalizability, and robustness with respect to partial specifications or domain knowledge. We believe that these paradigms are likely to have significant and dramatic impact on AI and its applications for a long time to come.</div> <div class="clear"></div> <div class="classification"> <h3>MSC:</h3> <table><tr> <td> <a class="mono" href="/classification/?q=cc%3A68-XX" title="MSC2020">68-XX</a> </td> <td class="space"> Computer science </td> </tr></table> </div><div class="keywords"> <h3>Keywords:</h3><a href="/?q=ut%3Acombinations+of+learning+and+reasoning">combinations of learning and reasoning</a>; <a href="/?q=ut%3Alearning+for+solvers">learning for solvers</a>; <a href="/?q=ut%3Alearning+for+verification+and+synthesis">learning for verification and synthesis</a>; <a href="/?q=ut%3Asolver+layers+in+deep+neural+networks">solver layers in deep neural networks</a></div> <div class="software"> <h3>Software:</h3><a href="/software/3136">SLAM</a>; <a href="/software/7833">Glucose</a>; <a href="/software/6281">SATzilla</a>; <a href="/software/43881">HOList</a>; <a href="/software/34795">STP</a>; <a href="/software/41593">MedleySolver</a>; <a href="/software/46009">NeuroSAT</a>; <a href="/software/40572">MachSMT</a>; <a href="/software/46232">GPT-4</a>; <a href="/software/4887">z3</a>; <a href="/software/577">MiniSat</a></div>  <div class="modal fade" id="metadataModal" tabindex="-1" role="dialog" aria-labelledby="myModalLabel"> <div class="modal-dialog" role="document"> <div class="modal-content"> <div class="modal-header"> <button type="button" class="close" data-dismiss="modal" aria-label="Close"><span aria-hidden="true">×</span></button> <h4 class="modal-title" id="myModalLabel">Cite</h4> </div> <div class="modal-body"> <div class="form-group"> <label for="select-output" class="control-label">Format</label> <select id="select-output" class="form-control" aria-label="Select Metadata format"></select> </div> <div class="form-group"> <label for="metadataText" class="control-label">Result</label> <textarea class="form-control" id="metadataText" rows="10" style="min-width: 100%;max-width: 100%"></textarea> </div> <div id="metadata-alert" class="alert alert-danger" role="alert" style="display: none;">  </div> </div> <div class="modal-footer"> <button type="button" class="btn btn-primary" onclick="copyMetadata()">Copy to clipboard</button> <button type="button" class="btn btn-default" data-dismiss="modal">Close</button> </div> </div> </div> </div> <div class="functions clearfix"> <div class="function">  <a type="button" class="btn btn-default btn-xs pdf" data-toggle="modal" data-target="#metadataModal" data-itemtype="Zbl" data-itemname="Zbl 07757157" data-ciurl="/ci/07757157" data-biburl="/bibtex/07757157.bib" data-amsurl="/amsrefs/07757157.bib" data-xmlurl="/xml/07757157.xml" > Cite </a> <a class="btn btn-default btn-xs pdf" data-container="body" type="button" href="/pdf/07757157.pdf" title="Zbl 07757157 as PDF">Review PDF</a> </div> <div class="fulltexts"> <span class="fulltext">Full Text:</span> <a class="btn btn-default btn-xs" type="button" href="https://doi.org/10.1007/s10703-023-00430-1" aria-label="DOI for “Machine learning and logic: a new frontier in artificial intelligence”" title="10.1007/s10703-023-00430-1">DOI</a> </div> <div class="sfx" style="float: right;"> </div> </div> <div class="references"> <h3>References:</h3> <table><tr> <td>[1]</td> <td class="space">Alur R, Bodik R, Juniwal G, Martin Milo MK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: Proceedings of the IEEE international conference on formal methods in computer-aided design (FMCAD), pp 1-17</td> </tr><tr> <td>[2]</td> <td class="space">Abate A, David C, Kesseli P, Kroening D, Polgreen E (2018) Counterexample guided inductive synthesis modulo theories. In: Computer aided verification-30th international conference (CAV), volume 10981 of Lecture Notes in Computer Science, pp 270-288. Springer · <a href="/1511.68064" class="nowrap">Zbl 1511.68064</a></td> </tr><tr> <td>[3]</td> <td class="space">Atserias, A.; Fichte, JK; Thurley, M.; Kullmann, O., Clause-learning algorithms with many restarts and bounded-width resolution, Theory and Applications of Satisfiability Testing - SAT, 114-127 (2009), Berlin, Heidelberg: Springer, Berlin Heidelberg, Berlin, Heidelberg · <a href="/1247.68245" class="nowrap">Zbl 1247.68245</a></td> </tr><tr> <td>[4]</td> <td class="space">Angluin, D., Queries and concept learning, Mach Learn, 2, 4, 319-342 (1988) · <a href="/1470.68050" class="nowrap">Zbl 1470.68050</a> · <a href="https://doi.org/10.1007/BF00116828" class="nowrap">doi:10.1007/BF00116828</a></td> </tr><tr> <td>[5]</td> <td class="space">Audemard Gilles, Simon Laurent (2013) Glucose 2.3 in the SAT 2013 Competition. In: Proceedings of SAT competition 2013, pp 42-43</td> </tr><tr> <td>[6]</td> <td class="space">Alur, R.; Singh, R.; Fisman, D.; Solar-Lezama, A., Search-based program synthesis, Commun ACM, 61, 12, 84-93 (2018) · <a href="https://doi.org/10.1145/3208071" class="nowrap">doi:10.1145/3208071</a></td> </tr><tr> <td>[7]</td> <td class="space">Ashok D, Scott J, Wetzel SJ, Panju M, Ganesh V (2021) Logic guided genetic algorithms. In: 35th AAAI conference on artificial intelligence, AAAI 2021, 33rd Conference on innovative applications of artificial intelligence, IAAI 2021, The 11th symposium on educational advances in artificial intelligence, EAAI 2021, virtual event, Feb 2-9, 2021, pp 15753-15754. AAAI Press</td> </tr><tr> <td>[8]</td> <td class="space">Alaa AM, Schaar M van der (2019) Demystifying black-box models with symbolic metamodels. Adv Neural Inf Process Syst 32</td> </tr><tr> <td>[9]</td> <td class="space">Bouraoui Z, Cornuéjols A, Denoeux T, Destercke S, Dubois D, Guillaume R, Marques-Silva J, Mengin J, Prade H, Schockaert S, Serrurier M, Vrain C (2019) From shallow to deep interactions between knowledge representation, reasoning and machine learning (kay r. amel group). CoRR, abs/1912.06612</td> </tr><tr> <td>[10]</td> <td class="space">Biere A, Heule M, van Maaren H, Walsh T (2009) (eds) Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications. IOS Press · <a href="/1183.68568" class="nowrap">Zbl 1183.68568</a></td> </tr><tr> <td>[11]</td> <td class="space">Bünz B, Lamm M (2017) Graph neural networks and boolean satisfiability. CoRR, abs/1702.03592</td> </tr><tr> <td>[12]</td> <td class="space">Bengio, Y.; LeCun, Y.; Hinton, GE, Deep learning for AI, Commun ACM, 64, 7, 58-65 (2021) · <a href="https://doi.org/10.1145/3448250" class="nowrap">doi:10.1145/3448250</a></td> </tr><tr> <td>[13]</td> <td class="space">Bak S, Liu C, Johnson TT (2021) The second international verification of neural networks competition (VNN-COMP 2021): Summary and results. CoRR, abs/2109.00498</td> </tr><tr> <td>[14]</td> <td class="space">Ball, T.; Levin, V.; Rajamani, SK, A decade of software model checking with SLAM, Commun ACM, 54, 7, 68-76 (2011) · <a href="https://doi.org/10.1145/1965724.1965743" class="nowrap">doi:10.1145/1965724.1965743</a></td> </tr><tr> <td>[15]</td> <td class="space">Bansal K, Loos SM, Rabe MN, Szegedy C, Wilcox S (2019) Holist: an environment for machine learning of higher order logic theorem proving. In: Kamalika C and Ruslan S, (eds.) Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pp 454-463. PMLR</td> </tr><tr> <td>[16]</td> <td class="space">Bader-El-Den MB, Poli R (2007) Generating SAT local-search heuristics using a GP hyper-heuristic framework. In: Nicolas M, El-Ghazali T, Pierre C, Marc S, Evelyne L, (eds), Artificial Evolution, 8th International Conference, Evolution Artificielle, EA 2007, Tours, France, October 29-31, 2007, revised selected papers, volume 4926 of Lecture Notes in Computer Science, Springer, pp 37-49</td> </tr><tr> <td>[17]</td> <td class="space">Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y., Bounded model checking using satisfiability solving, Formal Methods Syst Des, 19, 1, 7-34 (2001) · <a href="/0985.68038" class="nowrap">Zbl 0985.68038</a> · <a href="https://doi.org/10.1023/A:1011276507260" class="nowrap">doi:10.1023/A:1011276507260</a></td> </tr><tr> <td>[18]</td> <td class="space">Cropper, A.; Dumancic, S.; Evans, R.; Muggleton, SH, Inductive logic programming at 30, Mach Learn, 111, 1, 147-172 (2022) · <a href="/07510309" class="nowrap">Zbl 07510309</a> · <a href="https://doi.org/10.1007/s10994-021-06089-1" class="nowrap">doi:10.1007/s10994-021-06089-1</a></td> </tr><tr> <td>[19]</td> <td class="space">Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of programs, pp 52-71 · <a href="/0546.68014" class="nowrap">Zbl 0546.68014</a></td> </tr><tr> <td>[20]</td> <td class="space">Clarke EM, Fehnker A, Han Z, Krogh BH, Stursberg O, Theobald M (2003) Verification of hybrid systems based on counterexample-guided abstraction refinement. In: TACAS, pp 192-207 · <a href="/1031.68078" class="nowrap">Zbl 1031.68078</a></td> </tr><tr> <td>[21]</td> <td class="space">Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: 12th international conference on computer aided verification (CAV), vol. 1855 of Lecture Notes in Computer Science, Springer, pp 154-169 · <a href="/0974.68517" class="nowrap">Zbl 0974.68517</a></td> </tr><tr> <td>[22]</td> <td class="space">Clarke, EM; Grumberg, O.; Jha, S.; Yuan, L.; Veith, H., Counterexample-guided abstraction refinement for symbolic model checking, J ACM, 50, 5, 752-794 (2003) · <a href="/1325.68145" class="nowrap">Zbl 1325.68145</a> · <a href="https://doi.org/10.1145/876638.876643" class="nowrap">doi:10.1145/876638.876643</a></td> </tr><tr> <td>[23]</td> <td class="space">Clarke EM, Gupta A, Kukula JH, Strichman O (2002) SAT based abstraction-refinement using ILP and machine learning techniques. In: computer aided verification, 14th international conference (CAV), vol. 2404 of Lecture Notes in Computer Science, Springer, pp 265-279 · <a href="/1010.68515" class="nowrap">Zbl 1010.68515</a></td> </tr><tr> <td>[24]</td> <td class="space">Cadar C, Ganesh V, Pawlowski PM, Dill DL, Engler DR (2006) EXE: automatically generating inputs of death. In: Proceedings of the 13th ACM conference on computer and communications security, CCS ’06, New York, NY, USA. ACM, pp 322-335</td> </tr><tr> <td>[25]</td> <td class="space">Cook S (1971) The complexity of theorem-proving procedures. In: proceedings of the third annual ACM symposium on theory of computing (STOC), ACM, pp 151-158 · <a href="/0253.68020" class="nowrap">Zbl 0253.68020</a></td> </tr><tr> <td>[26]</td> <td class="space">Dash T, Chitlangia S, Ahuja A, Srinivasan A (2021) How to tell deep neural networks what we know. CoRR, abs/2107.10295</td> </tr><tr> <td>[27]</td> <td class="space">Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem-proving, Commun ACM, 5, 7, 394-397 (1962) · <a href="/0217.54002" class="nowrap">Zbl 0217.54002</a> · <a href="https://doi.org/10.1145/368273.368557" class="nowrap">doi:10.1145/368273.368557</a></td> </tr><tr> <td>[28]</td> <td class="space">De Moura L, Bjørner N (2008) Z3: An efficient smt solver. In: international conference on tools and algorithms for the construction and analysis of systems, Springer, pp 337-340</td> </tr><tr> <td>[29]</td> <td class="space">Duan H, Nejati S, Trimponias G, Poupart P, Ganesh V (2020) Online bayesian moment matching based SAT solver heuristics. In: Proceedings of the 37th international conference on machine learning, ICML 2020, 13-18 July 2020, Virtual Event, vol. 119 of proceedings of machine learning research, PMLR, pp 2710-2719</td> </tr><tr> <td>[30]</td> <td class="space">Devlin D, O’Sullivan B (2008) Satisfiability as a classification problem. In: Proceedings of the 19th Irish Conference on artificial intelligence and cognitive science</td> </tr><tr> <td>[31]</td> <td class="space">Dubois D, Prade H (2019) Towards a reconciliation between reasoning and learning-a position paper. In: Nahla Ben A, Benjamin Q, Martin T, (eds) scalable uncertainty management-13th international conference, SUM 2019, Compiègne, France, Dec 16-18, 2019, Proceedings, vol. 11940 of lecture notes in computer science, Springer, pp 153-168</td> </tr><tr> <td>[32]</td> <td class="space">Eén N, Sörensson N (2004) Theory and applications of satisfiability testing: 6th international conference, SAT 2003, santa margherita ligure, Italy, May 5-8, 2003, selected revised papers, chapter an extensible SAT-solver, Springer Berlin Heidelberg, Berlin, Heidelberg, pp 502-518 · <a href="/1204.68191" class="nowrap">Zbl 1204.68191</a></td> </tr><tr> <td>[33]</td> <td class="space">Ertel W, Schumann J, Suttner CB (1989) Learning heuristics for a theorem prover using back propagation. In: Johannes R, Karl L, (eds) 5. Österreichische Artificial Intelligence-Tagung, Igls, Tirol, 28. bis 30. Sept 1989, Proceedings, vol. 208 of Informatik-Fachberichte, Springer, pp 87-95</td> </tr><tr> <td>[34]</td> <td class="space">Flint A, Blaschko MB (2012) Perceptron learning of SAT. In: Bartlett PL, Pereira FNC, Burges CJC, Léon B, Weinberger KQ, (eds) Advances in neural information processing systems 25: 26th annual conference on neural information processing systems 2012. Proceedings of a meeting held Dec 3-6, 2012, Lake Tahoe, Nevada, United States, pp 2780-2788</td> </tr><tr> <td>[35]</td> <td class="space">Froleyks, N.; Heule, M.; Iser, M.; Järvisalo, M.; Suda, M., SAT competition 2020, Artif Intell, 301, 103572 (2021) · <a href="/1478.68320" class="nowrap">Zbl 1478.68320</a> · <a href="https://doi.org/10.1016/j.artint.2021.103572" class="nowrap">doi:10.1016/j.artint.2021.103572</a></td> </tr><tr> <td>[36]</td> <td class="space">Feldman, YMY; Immerman, N.; Sagiv, M.; Shoham, S., Complexity and information in invariant inference, Proc ACM Program Lang, 4, POPL, 5:1-5:29 (2020) · <a href="https://doi.org/10.1145/3371073" class="nowrap">doi:10.1145/3371073</a></td> </tr><tr> <td>[37]</td> <td class="space">First E, Rabe MN, Ringer T, Brun Y (2023) Baldur: whole-proof generation and repair with large language models. CoRR, abs/2303.04910</td> </tr><tr> <td>[38]</td> <td class="space">Fukunaga AS (2002) Automated discovery of composite SAT variable-selection heuristics. In: Dechter R, Kearns MJ, Sutton RS, (eds) proceedings of the eighteenth national conference on artificial intelligence and fourteenth conference on innovative applications of artificial intelligence, July 28 - August 1, 2002, Edmonton, Alberta, Canada, AAAI Press / The MIT Press, pp 641-648</td> </tr><tr> <td>[39]</td> <td class="space">Fukunaga AS (2004) Evolving local search heuristics for SAT using genetic programming. In: Kalyanmoy D, Riccardo P, Wolfgang B, Hans-Georg B, Burke EK, Darwen PJ, Dasgupta D, Floreano D, Foster JA, Mark H, Owen H, Pier Luca L, Lee S, Andrea T, Dirk T, Tyrrell AM, (eds) Genetic and evolutionary computation-GECCO 2004, genetic and evolutionary computation conference, Seattle, WA, USA, June 26-30, 2004, Proceedings, Part II, volume 3103 of Lecture Notes in Computer Science, Springer, pp 483-494</td> </tr><tr> <td>[40]</td> <td class="space">Fukunaga, AS, Automated discovery of local search heuristics for satisfiability testing, Evol Comput, 16, 1, 31-61 (2008) · <a href="https://doi.org/10.1162/evco.2008.16.1.31" class="nowrap">doi:10.1162/evco.2008.16.1.31</a></td> </tr><tr> <td>[41]</td> <td class="space">Ian, JG; Yoshua, B.; Courville, AC, Deep Learning, Adaptive computation and machine learning (2016), Cambridge: MIT Press, Cambridge · <a href="/1373.68009" class="nowrap">Zbl 1373.68009</a></td> </tr><tr> <td>[42]</td> <td class="space">Goldman, SA; Kearns, MJ, On the complexity of teaching, J Comput Syst Sci, 50, 303-314 (1992)</td> </tr><tr> <td>[43]</td> <td class="space">Gupta A (2006) Learning Abstractions for Model Checking. PhD thesis, Carnegie Mellon University, June</td> </tr><tr> <td>[44]</td> <td class="space">Hutter F, Babic D, Hoos HH, Hu AJ (2007) Boosting verification by automatic tuning of decision procedures. In: 7th international conference on formal methods in computer-aided design (FMCAD), IEEE Computer Society, pp 27-34</td> </tr><tr> <td>[45]</td> <td class="space">Hart, PE; Nilsson, NJ; Raphael, B., A formal basis for the heuristic determination of minimum cost paths, IEEE Trans Syst Sci Cybern, 4, 2, 100-107 (1968) · <a href="https://doi.org/10.1109/TSSC.1968.300136" class="nowrap">doi:10.1109/TSSC.1968.300136</a></td> </tr><tr> <td>[46]</td> <td class="space">Holden, SB, Machine learning for automated theorem proving: learning to solve SAT and QSAT, Found Trends Mach Learn, 14, 6, 807-989 (2021) · <a href="/1524.68280" class="nowrap">Zbl 1524.68280</a> · <a href="https://doi.org/10.1561/2200000081" class="nowrap">doi:10.1561/2200000081</a></td> </tr><tr> <td>[47]</td> <td class="space">Hopfield, JJ; Tank, DW, Neural computation of decisions in optimization problems, Biol Cybern, 52, 141-152 (1985) · <a href="/0572.68041" class="nowrap">Zbl 0572.68041</a> · <a href="https://doi.org/10.1007/BF00339943" class="nowrap">doi:10.1007/BF00339943</a></td> </tr><tr> <td>[48]</td> <td class="space">Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Proceedings of the 32nd international conference on software engineering (ICSE), pp 215-224</td> </tr><tr> <td>[49]</td> <td class="space">Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Synthesizing switching logic for safety and dwell-time requirements. In: proceedings of the international conference on cyber-physical systems (ICCPS), pp 22-31</td> </tr><tr> <td>[50]</td> <td class="space">Johnson, JL, A neural network approach to the 3-satisfiability problem, J Parallel Distributed Comput, 6, 435-449 (1989) · <a href="https://doi.org/10.1016/0743-7315(89)90068-3" class="nowrap">doi:10.1016/0743-7315(89)90068-3</a></td> </tr><tr> <td>[51]</td> <td class="space">Jha, S.; Seshia, SA, A theory of formal synthesis via inductive learning, Acta Inform, 54, 7, 693-726 (2017) · <a href="/1380.68124" class="nowrap">Zbl 1380.68124</a> · <a href="https://doi.org/10.1007/s00236-017-0294-5" class="nowrap">doi:10.1007/s00236-017-0294-5</a></td> </tr><tr> <td>[52]</td> <td class="space">Kim, S.; Lu, PY; Mukherjee, S.; Gilbert, M.; Jing, L.; Čeperić, V.; Soljačić, M., Integration of neural network-based symbolic regression in deep learning for scientific discovery, IEEE Trans Neural Netw Learn Syst, 32, 9, 4166-4177 (2021) · <a href="https://doi.org/10.1109/TNNLS.2020.3017010" class="nowrap">doi:10.1109/TNNLS.2020.3017010</a></td> </tr><tr> <td>[53]</td> <td class="space">Kautz HA, Selman B (1992) Planning as satisfiability. In: Bernd N, (ed) 10th European conference on artificial intelligence, ECAI 92, Vienna, Austria, August 3-7, 1992. Proceedings, John Wiley and Sons, pp 359-363</td> </tr><tr> <td>[54]</td> <td class="space">Kurshan R (1994) Automata-theoretic verification of coordinating processes. In: 11th international conference on analysis and optimization of systems-discrete event systems, vol. 199 of LNCS, Springer, pp 16-28</td> </tr><tr> <td>[55]</td> <td class="space">Lewkowycz A, Andreassen A, Dohan D, Dyer E, Michalewski H, Ramasesh VV, Slone A, Anil C, Schlag I, Gutman-Solo T, Wu Y, Neyshabur B, Gur-Ari G, Misra V (2022) Solving quantitative reasoning problems with language models. CoRR, abs/2206.14858</td> </tr><tr> <td>[56]</td> <td class="space">Liang JH, Ganesh V, Poupart P, Czarnecki K (2016) Learning rate based branching heuristic for SAT solvers. In: Nadia C, Daniel LB, (eds) Theory and applications of satisfiability testing-SAT 2016, Cham. Springer International Publishing, pp 123-140 · <a href="/1475.68348" class="nowrap">Zbl 1475.68348</a></td> </tr><tr> <td>[57]</td> <td class="space">Liang JH (2018) Machine learning for SAT solvers. PhD thesis, University of Waterloo, Canada · <a href="/1511.68253" class="nowrap">Zbl 1511.68253</a></td> </tr><tr> <td>[58]</td> <td class="space">Lagoudakis Michail, G.; Littman Michael, L., Learning to select branching rules in the DPLL procedure for satisfiability, Electron Notes Discrete Math, 9, 344-359 (2001) · <a href="/0990.90543" class="nowrap">Zbl 0990.90543</a> · <a href="https://doi.org/10.1016/S1571-0653(04)00332-4" class="nowrap">doi:10.1016/S1571-0653(04)00332-4</a></td> </tr><tr> <td>[59]</td> <td class="space">Liang JH, Oh C, Mathew M, Thomas C, Li C, Ganesh V (2018) Machine learning-based restart policy for CDCL SAT solvers. In: theory and applications of satisfiability testing-SAT 2018 - 21st international conference, SAT 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, pp 94-110 · <a href="/1511.68253" class="nowrap">Zbl 1511.68253</a></td> </tr><tr> <td>[60]</td> <td class="space">Lederman G, Rabe MN, Seshia S, Lee EA (2020) Learning heuristics for quantified boolean formulas through reinforcement learning. In: 8th international conference on learning representations (ICLR), April</td> </tr><tr> <td>[61]</td> <td class="space">Lorenz JH, Wörz F (2020) On the effect of learned clauses on stochastic local search. In: Luca P, Martina S, (eds) Theory and applications of satisfiability testing-SAT 2020-23rd international conference, Alghero, Italy, July 3-10, 2020, Proceedings, vol. 12178 of lecture notes in computer science, Springer, pp 89-106 · <a href="/07331014" class="nowrap">Zbl 07331014</a></td> </tr><tr> <td>[62]</td> <td class="space">Tom, M., Mitchell (1997), Machine Learning: McGraw-Hill, Machine Learning · <a href="/0913.68167" class="nowrap">Zbl 0913.68167</a></td> </tr><tr> <td>[63]</td> <td class="space">Marques-Silva JP, Sakallah KA (1996) GRASP-A new search algorithm for satisfiability. In: proceedings of the 1996 IEEE/ACM international conference on computer-aided design, ICCAD ’96, Washington, DC, USA. IEEE Computer Society, pp 220-227</td> </tr><tr> <td>[64]</td> <td class="space">Manna, Z.; Waldinger, R., A deductive approach to program synthesis, ACM Trans Program Lang Syst (TOPLAS), 2, 1, 90-121 (1980) · <a href="/0468.68009" class="nowrap">Zbl 0468.68009</a> · <a href="https://doi.org/10.1145/357084.357090" class="nowrap">doi:10.1145/357084.357090</a></td> </tr><tr> <td>[65]</td> <td class="space">Nejati S, Frioux LL, Ganesh V (2020) A machine learning based splitting heuristic for divide-and-conquer solvers. In: Helmut S, (ed) Principles and practice of constraint programming-26th international conference, CP 2020, Louvain-la-Neuve, Belgium, Sept 7-11, 2020, Proceedings, vol. 12333 of lecture notes in computer science, Springer, pp 899-916</td> </tr><tr> <td>[66]</td> <td class="space">OpenAI. GPT-4 technical report. CoRR, abs/2303.08774, 2023</td> </tr><tr> <td>[67]</td> <td class="space">Panju M (2021) Automated Knowledge Discovery using Neural Networks. PhD thesis, University of Waterloo, Ontario, Canada</td> </tr><tr> <td>[68]</td> <td class="space">Polgreen E, Cheang K, Gaddamadugu P, Godbole A, Laeufer K, Lin S, Manerkar YA, Mora F, Seshia SA (2022) UCLID5: multi-modal formal modeling, verification, and synthesis. In: computer aided verification-34th international conference (CAV), vol. 13371 of lecture notes in computer science, Springer, pp 538-551</td> </tr><tr> <td>[69]</td> <td class="space">Pipatsrisawat, K.; Darwiche, A., On the power of clause-learning SAT solvers as resolution engines, Artif Intell, 175, 2, 512-525 (2011) · <a href="/1216.68235" class="nowrap">Zbl 1216.68235</a> · <a href="https://doi.org/10.1016/j.artint.2010.10.002" class="nowrap">doi:10.1016/j.artint.2010.10.002</a></td> </tr><tr> <td>[70]</td> <td class="space">Andrei, P.; Polat, ES; Alexander, F.; Mathias, U.; Müslüm, A.; Viet-Man, L.; Klaus, P.; Martin, E.; Trang, TTN, An overview of machine learning techniques in constraint solving, J Intell Inf Syst, 58, 1, 91-118 (2022) · <a href="https://doi.org/10.1007/s10844-021-00666-5" class="nowrap">doi:10.1007/s10844-021-00666-5</a></td> </tr><tr> <td>[71]</td> <td class="space">Pimpalkhare N, Mora F, Polgreen E, Seshia SA (2021) MedleySolver: online SMT algorithm selection. In: 24th international conference on theory and applications of satisfiability testing (SAT), vol. 12831 of lecture notes in computer science, Springer, pp 453-470 · <a href="/07495591" class="nowrap">Zbl 07495591</a></td> </tr><tr> <td>[72]</td> <td class="space">Pogancic MV, Paulus A, Musil V, Martius G, Rolínek M (2020) Differentiation of blackbox combinatorial solvers. In: 8th international conference on learning representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net</td> </tr><tr> <td>[73]</td> <td class="space">Polgreen E, Reynolds A, Seshia SA (2022) Satisfiability and synthesis modulo oracles. In: Proceedings of the 23rd international conference on verification, model checking, and abstract interpretation (VMCAI) · <a href="/1498.68082" class="nowrap">Zbl 1498.68082</a></td> </tr><tr> <td>[74]</td> <td class="space">De Raedt, L., Logical and relational learning, Cognitive technologies (2008), Berlin: Springer, Berlin · <a href="/1203.68145" class="nowrap">Zbl 1203.68145</a></td> </tr><tr> <td>[75]</td> <td class="space">Russell, S.; Norvig, P., Artificial intelligence: a modern approach (2020), London: Pearson, London · <a href="/0835.68093" class="nowrap">Zbl 0835.68093</a></td> </tr><tr> <td>[76]</td> <td class="space">Rossi F, van Beek P, Walsh T (2006) editors. Handbook of Constraint Programming, vol. 2 of Foundations of Artificial Intelligence. Elsevier · <a href="/1175.90011" class="nowrap">Zbl 1175.90011</a></td> </tr><tr> <td>[77]</td> <td class="space">Richard, SS; Andrew, GB, Reinforcement learning-an introduction, Adaptive computation and machine learning (1998), Cambridge: MIT Press, Cambridge</td> </tr><tr> <td>[78]</td> <td class="space">Seshia SA (2005) Adaptive eager boolean encoding for arithmetic reasoning in verification. PhD thesis, Carnegie Mellon University</td> </tr><tr> <td>[79]</td> <td class="space">Seshia SA (2012) Sciduction: combining induction, deduction, and structure for verification and synthesis. In: proceedings of the design automation conference (DAC), pp 356-365</td> </tr><tr> <td>[80]</td> <td class="space">Seshia, SA, Combining induction, deduction, and structure for verification and synthesis, Proc IEEE, 103, 11, 2036-2051 (2015) · <a href="https://doi.org/10.1109/JPROC.2015.2471838" class="nowrap">doi:10.1109/JPROC.2015.2471838</a></td> </tr><tr> <td>[81]</td> <td class="space">Selsam D, Lamm M, Bünz B, Liang P, de Moura L, Dill DL (2019) Learning a SAT solver from single-bit supervision. In: 7th international conference on learning representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net</td> </tr><tr> <td>[82]</td> <td class="space">Solar-Lezama A, Tancau L, Bodík R, Seshia SA, Saraswat VA (2006) Combinatorial sketching for finite programs. In: proceedings of the 12th international conference on architectural support for programming languages and operating systems (ASPLOS), ACM Press, pp 404-415</td> </tr><tr> <td>[83]</td> <td class="space">Scott J, Niemetz A, Preiner M, Nejati S, Ganesh V (2021) Machsmt: a machine learning-based algorithm selector for SMT solvers. In: Jan Friso G, Kim Guldstrand L, (eds) Tools and algorithms for the construction and analysis of systems-27th international conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27-April 1, 2021, Proceedings, Part II, vol. 12652 of Lecture Notes in Computer Science, Springer, pp 303-325 · <a href="/1471.68016" class="nowrap">Zbl 1471.68016</a></td> </tr><tr> <td>[84]</td> <td class="space">Scott J, Panju M, Ganesh V (2020) LGML: logic guided machine learning. In: the thirty-fourth AAAI conference on artificial intelligence, AAAI 2020, the thirty-second innovative applications of artificial intelligence conference, IAAI 2020, the tenth AAAI symposium on educational advances in artificial intelligence, EAAI 2020, New York, NY, USA, Feb 7-12, 2020, AAAI Press, pp 13909-13910</td> </tr><tr> <td>[85]</td> <td class="space">Marques SJP, Sakallah KA (1996) GRASP-a new search algorithm for satisfiability. In: Rutenbar RA, Otten RHJM, (eds) proceedings of the 1996 IEEE/ACM international conference on computer-aided design, ICCAD 1996, San Jose, CA, USA, Nov 10-14, 1996, IEEE Computer Society / ACM, pp 220-227</td> </tr><tr> <td>[86]</td> <td class="space">Seshia SA, Subramanyan P (2018) UCLID5: integrating modeling, verification, synthesis, and learning. In: proceedings of the 15th ACM/IEEE international conference on formal methods and models for codesign (MEMOCODE)</td> </tr><tr> <td>[87]</td> <td class="space">Seshia, SA; Sadigh, D.; Sastry, SS, Toward verified artificial intelligence, Commun ACM, 65, 7, 46-55 (2022) · <a href="https://doi.org/10.1145/3503914" class="nowrap">doi:10.1145/3503914</a></td> </tr><tr> <td>[88]</td> <td class="space">Seshia SA, Sharygina N, Tripakis S (2018) Modeling for verification. In: Clarke EM, Thomas H, Helmut V, (eds) Handbook of Model Checking, chapter 3. Springer · <a href="/1392.68264" class="nowrap">Zbl 1392.68264</a></td> </tr><tr> <td>[89]</td> <td class="space">Sarker, Md; Kamruzzaman, ZL; Aaron, E.; Pascal, H., Neuro-symbolic artificial intelligence, AI Commun, 34, 3, 197-209 (2021) · <a href="/1487.68188" class="nowrap">Zbl 1487.68188</a> · <a href="https://doi.org/10.3233/AIC-210084" class="nowrap">doi:10.3233/AIC-210084</a></td> </tr><tr> <td>[90]</td> <td class="space">van Harmelen F, Lifschitz V, Porter BW (2008) (eds) Handbook of Knowledge Representation, vol. 3 of Foundations of Artificial Intelligence. Elsevier · <a href="/1183.68611" class="nowrap">Zbl 1183.68611</a></td> </tr><tr> <td>[91]</td> <td class="space">The Verification of Neural Networks Library (VNN-LIB). www.vnnlib.org, 2019</td> </tr><tr> <td>[92]</td> <td class="space">Wang PW, Donti PL, Wilder B, Zico KJ (2019) Satnet: bridging deep learning and logical reasoning using a differentiable satisfiability solver. In: Kamalika C, Ruslan S, (eds) proceedings of the 36th international conference on machine learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, vol. 97 of Proceedings of Machine Learning Research, PMLR, pp 6545-6554</td> </tr><tr> <td>[93]</td> <td class="space">Jeannette, MW, Trustworthy AI, Commun ACM, 64, 10, 64-71 (2021) · <a href="https://doi.org/10.1145/3448248" class="nowrap">doi:10.1145/3448248</a></td> </tr><tr> <td>[94]</td> <td class="space">Lin, X.; Hutter, F.; Hoos, HH; Leyton-Brown, K., SATzilla: portfolio-based algorithm selection for SAT, J Artif Intell Res, 32, 1, 565-606 (2008) · <a href="/1182.68272" class="nowrap">Zbl 1182.68272</a></td> </tr></table> <div class="reference_disclaimer"> This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching. </div> </div></article> </div></div> </div> </div> <div class="clearfix"></div> </div> </div> <div id="foot"><div class="copyright"> © 2024 <a target="fiz" href="https://www.fiz-karlsruhe.de/en">FIZ Karlsruhe GmbH</a> <a href="/privacy-policy/">Privacy Policy</a> <a href="/legal-notices/">Legal Notices</a> <a href="/terms-conditions/">Terms & Conditions</a> <div class="info"> <ul class="nav"> <li class="mastodon"> <a href="https://mathstodon.xyz/@zbMATH" target="_blank" class="no-new-tab-icon"> <img src="/static/mastodon.png" title="zbMATH at Mathstodon (opens in new tab)" alt="Mastodon logo"> </a> </li> </ul> </div> </div> <div class="clearfix" style="height: 0px;"></div> </div> </div> <script src="https://static.zbmath.org/contrib/jquery/1.9.1/jquery.min.js"></script> <script src="https://static.zbmath.org/contrib/jquery-caret/1.5.2/jquery.caret.min.js"></script> <script src="/static/js/jquery-ui-1.10.1.custom.min.js"></script> <script src="https://static.zbmath.org/contrib/bootstrap/v3.3.7zb1/js/bootstrap.min.js"></script> <script src="https://static.zbmath.org/contrib/bootstrap-lightbox/v0.7.0/bootstrap-lightbox.min.js"></script> <script src="https://static.zbmath.org/contrib/retina/unknown/retina.js"></script> <script src="https://static.zbmath.org/contrib/bootstrap-select/v1.13.14/js/bootstrap-select.min.js"></script> <script> var SCRIPT_ROOT = ""; </script> <script src="/static/scripts.js?v=20240926"> </script> <script src="https://static.zbmath.org/contrib/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> <script type="text/x-mathjax-config"> MathJax.Hub.Config({ "HTML-CSS": { preferredFont: "TeX", availableFonts: [ "STIX", "TeX" ], linebreaks: { automatic: true }, EqnChunk: (MathJax.Hub.Browser.isMobile ? 10 : 50) }, tex2jax: { processEscapes: true, ignoreClass: "tex2jax_ignore|dno" }, TeX: { Macros: { Aut: "\\operatorname{Aut}", Hom: "\\operatorname{Hom}" }, noUndefined: { attributes: { mathcolor: "#039", //"red", mathbackground: "white", //"#FFEEEE", mathsize: "90%" } } }, messageStyle: "none" }); </script> <script type="text/javascript"> $(document).ready(function() { $("#MathInput").stop(true, true).keyup(function() { $.ajax({ url: "/mwsq/", type: "POST", data: { query : $("#MathInput").val() }, dataType: "text" }) .done(function(xml) { $("#MathPreview").html(xml); $(window).resize(); }); }); var press = jQuery.Event("keyup"); press.ctrlKey = false; press.which = 40; $("#MathInput").trigger(press); }); </script> <div id="new_tab_icon" style="display: none"> <span class="glyphicon glyphicon-new-window" aria-hidden="true"></span><span class="sr-only">(opens in new tab)</span></div> </body> </html>

CINXE.COM

Document Zbl 07757157 - zbMATH Open