Document Zbl 1535.68448

<!doctype html> <html lang="en"> <head> <meta charset="utf-8"> <title>Document Zbl 1535.68448 - 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%3Aan.jie+cc%3A03"> <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:an.jie cc:03" 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/chen.mingshuai" title="Author Profile">Chen, Mingshuai</a>; <a href="/authors/wang.jian.95" title="Author Profile">Wang, Jian</a>; <a href="/authors/an.jie" title="Author Profile">An, Jie</a>; <a href="/authors/zhan.bohua" title="Author Profile">Zhan, Bohua</a>; <a href="/authors/kapur.deepak" title="Author Profile">Kapur, Deepak</a>; <a href="/authors/zhan.naijun" title="Author Profile">Zhan, Naijun</a></div> <h2 class="title"> <strong>NIL: learning nonlinear interpolants.</strong> <i>(English)</i> <a class="label nowrap" href="/1535.68448">Zbl 1535.68448</a> </h2> <div class="source"> Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 178-196 (2019). </div> <div class="abstract">Summary: Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model checking, abstract interpretation, etc. The underlying synthesis problem, however, is challenging and existing methods have limitations on the form of formulae to be interpolated. We leverage classification techniques with space transformations and kernel tricks as established in the realm of machine learning, and present a counterexample-guided method named NIL for synthesizing polynomial interpolants, thereby yielding a unified framework tackling the interpolation problem for the general quantifier-free theory of nonlinear arithmetic, possibly involving transcendental functions. We prove the soundness of NIL and propose sufficient conditions under which NIL is guaranteed to converge, i.e., the derived sequence of candidate interpolants converges to an actual interpolant, and is complete, namely the algorithm terminates by producing an interpolant if there exists one. The applicability and effectiveness of our technique are demonstrated experimentally on a collection of representative benchmarks from the literature, where in particular, our method suffices to address more interpolation tasks, including those with perturbations in parameters, and in many cases synthesizes simpler interpolants compared with existing approaches.<br class="zbmathjax-paragraph">For the entire collection see [<a href="/1428.68018">Zbl 1428.68018</a>].</div> <div class="clear"></div> <br> <div class="citations"><div class="clear"><a href="/?q=rf%3A7178976">Cited in <strong>2</strong> Documents</a></div></div> <div class="classification"> <h3>MSC:</h3> <table><tr> <td> <a class="mono" href="/classification/?q=cc%3A68V15" title="MSC2020">68V15</a> </td> <td class="space"> Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) </td> </tr><tr> <td> <a class="mono" href="/classification/?q=cc%3A03C40" title="MSC2020">03C40</a> </td> <td class="space"> Interpolation, preservation, definability </td> </tr><tr> <td> <a class="mono" href="/classification/?q=cc%3A68Q60" title="MSC2020">68Q60</a> </td> <td class="space"> Specification and verification (program logics, model checking, etc.) </td> </tr><tr> <td> <a class="mono" href="/classification/?q=cc%3A68T05" title="MSC2020">68T05</a> </td> <td class="space"> Learning and adaptive systems in artificial intelligence </td> </tr></table> </div><div class="keywords"> <h3>Keywords:</h3><a href="/?q=ut%3Anonlinear+Craig+interpolant">nonlinear Craig interpolant</a>; <a href="/?q=ut%3Acounterexample-guided+learning">counterexample-guided learning</a>; <a href="/?q=ut%3Aprogram+verification">program verification</a>; <a href="/?q=ut%3Asupport+vector+machines">support vector machines</a></div> <div class="software"> <h3>Software:</h3><a href="/software/3484">PVS</a>; <a href="/software/4879">LIBSVM</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 1535.68448" data-ciurl="/ci/07178976" data-biburl="/bibtex/07178976.bib" data-amsurl="/amsrefs/07178976.bib" data-xmlurl="/xml/07178976.xml" > Cite </a> <a class="btn btn-default btn-xs pdf" data-container="body" type="button" href="/pdf/07178976.pdf" title="Zbl 1535.68448 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/978-3-030-29436-6_11" aria-label="DOI for “NIL: learning nonlinear interpolants”" title="10.1007/978-3-030-29436-6_11">DOI</a> <a class="btn btn-default btn-xs" type="button" href="https://arxiv.org/abs/1905.11625"title="Note: arXiv document may differ from published version">arXiv</a> </div> <div class="sfx" style="float: right;"> </div> </div> <div class="references"> <h3>References:</h3> <table><tr> <td>[1]</td> <td class="space">Bennett, K.P., Bredensteiner, E.J.: Duality and geometry in SVM classifiers. In: ICML 2000, pp. 57-64 (2000)</td> </tr><tr> <td>[2]</td> <td class="space">Bishop, CM, Pattern Recognition and Machine Learning, 326-328 (2006), New York: Springer, New York · <a href="/1107.68072" class="nowrap">Zbl 1107.68072</a></td> </tr><tr> <td>[3]</td> <td class="space">Boser, B.E., Guyon, I., Vapnik, V.: A training algorithm for optimal margin classifiers. In: COLT 1992, pp. 144-152 (1992)</td> </tr><tr> <td>[4]</td> <td class="space">Bourbaki, N., Topological Vector Spaces (1987), Heidelberg: Springer, Heidelberg · <a href="/0622.46001" class="nowrap">Zbl 0622.46001</a> · <a href="https://doi.org/10.1007/978-3-642-61715-7" class="nowrap">doi:10.1007/978-3-642-61715-7</a></td> </tr><tr> <td>[5]</td> <td class="space">Chang, C.; Lin, C., LIBSVM: a library for support vector machines, ACM TIST, 2, 3, 27:1-27:27 (2011)</td> </tr><tr> <td>[6]</td> <td class="space">Chen, M., Wang, J., An, J., Zhan, B., Kapur, D., Zhan, N.: NIL: learning nonlinear interpolants (full version). http://lcs.ios.ac.cn/ chenms/papers/CADE-27_FULL.pdf · <a href="/1535.68448" class="nowrap">Zbl 1535.68448</a></td> </tr><tr> <td>[7]</td> <td class="space">Cimatti, A.; Griggio, A.; Sebastiani, R.; Ramakrishnan, CR; Rehof, J., Efficient interpolant generation in satisfiability modulo theories, Tools and Algorithms for the Construction and Analysis of Systems, 397-412 (2008), Heidelberg: Springer, Heidelberg · <a href="/1134.68402" class="nowrap">Zbl 1134.68402</a> · <a href="https://doi.org/10.1007/978-3-540-78800-3_30" class="nowrap">doi:10.1007/978-3-540-78800-3_30</a></td> </tr><tr> <td>[8]</td> <td class="space">Clarke, E.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H.; Emerson, EA; Sistla, AP, Counterexample-guided abstraction refinement, Computer Aided Verification, 154-169 (2000), Heidelberg: Springer, Heidelberg · <a href="/0974.68517" class="nowrap">Zbl 0974.68517</a> · <a href="https://doi.org/10.1007/10722167_15" class="nowrap">doi:10.1007/10722167_15</a></td> </tr><tr> <td>[9]</td> <td class="space">Collins, GE; Brakhage, H., Quantifier elimination for real closed fields by cylindrical algebraic decompostion, Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, May 20-23, 1975, 134-183 (1975), Heidelberg: Springer, Heidelberg · <a href="https://doi.org/10.1007/3-540-07407-4_17" class="nowrap">doi:10.1007/3-540-07407-4_17</a></td> </tr><tr> <td>[10]</td> <td class="space">Craig, W., Linear reasoning. A new form of the Herbrand-Gentzen theorem, J. Symb. Log., 22, 3, 250-268 (1957) · <a href="/0081.24402" class="nowrap">Zbl 0081.24402</a> · <a href="https://doi.org/10.2307/2963593" class="nowrap">doi:10.2307/2963593</a></td> </tr><tr> <td>[11]</td> <td class="space">Dai, L.; Xia, B.; Zhan, N.; Sharygina, N.; Veith, H., Generating non-linear interpolants by semidefinite programming, Computer Aided Verification, 364-380 (2013), Heidelberg: Springer, Heidelberg · <a href="/1503.68181" class="nowrap">Zbl 1503.68181</a> · <a href="https://doi.org/10.1007/978-3-642-39799-8_25" class="nowrap">doi:10.1007/978-3-642-39799-8_25</a></td> </tr><tr> <td>[12]</td> <td class="space">Dathathri, S., Arechiga, N., Gao, S., Murray, R.M.: Learning-based abstractions for nonlinear constraint solving. In: IJCAI 2017, pp. 592-599 (2017)</td> </tr><tr> <td>[13]</td> <td class="space">D’Silva, V.; Kroening, D.; Purandare, M.; Weissenbacher, G.; Barthe, G.; Hermenegildo, M., Interpolant strength, Verification, Model Checking, and Abstract Interpretation, 129-145 (2010), Heidelberg: Springer, Heidelberg · <a href="/1273.68225" class="nowrap">Zbl 1273.68225</a> · <a href="https://doi.org/10.1007/978-3-642-11319-2_12" class="nowrap">doi:10.1007/978-3-642-11319-2_12</a></td> </tr><tr> <td>[14]</td> <td class="space">Gan, T.; Dai, L.; Xia, B.; Zhan, N.; Kapur, D.; Chen, M.; Olivetti, N.; Tiwari, A., Interpolant synthesis for quadratic polynomial inequalities and combination with EUF, Automated Reasoning, 195-212 (2016), Cham: Springer, Cham · <a href="/1475.03072" class="nowrap">Zbl 1475.03072</a> · <a href="https://doi.org/10.1007/978-3-319-40229-1_14" class="nowrap">doi:10.1007/978-3-319-40229-1_14</a></td> </tr><tr> <td>[15]</td> <td class="space">Gao, S.; Zufferey, D.; Chechik, M.; Raskin, J-F, Interpolants in nonlinear theories over the reals, Tools and Algorithms for the Construction and Analysis of Systems, 625-641 (2016), Heidelberg: Springer, Heidelberg · <a href="/1420.68187" class="nowrap">Zbl 1420.68187</a> · <a href="https://doi.org/10.1007/978-3-662-49674-9_41" class="nowrap">doi:10.1007/978-3-662-49674-9_41</a></td> </tr><tr> <td>[16]</td> <td class="space">Gilbert, S., A nullstellensatz and a positivstellensatz in semialgebraic geometry, Math. Ann., 207, 2, 87-97 (1974) · <a href="/0253.14001" class="nowrap">Zbl 0253.14001</a> · <a href="https://doi.org/10.1007/BF01362149" class="nowrap">doi:10.1007/BF01362149</a></td> </tr><tr> <td>[17]</td> <td class="space">Graf, S.; Saidi, H.; Grumberg, O., Construction of abstract state graphs with PVS, Computer Aided Verification, 72-83 (1997), Heidelberg: Springer, Heidelberg · <a href="https://doi.org/10.1007/3-540-63166-6_10" class="nowrap">doi:10.1007/3-540-63166-6_10</a></td> </tr><tr> <td>[18]</td> <td class="space">Gulavani, BS; Chakraborty, S.; Nori, AV; Rajamani, SK; Ramakrishnan, CR; Rehof, J., Automatically refining abstract interpretations, Tools and Algorithms for the Construction and Analysis of Systems, 443-458 (2008), Heidelberg: Springer, Heidelberg · <a href="/1134.68356" class="nowrap">Zbl 1134.68356</a> · <a href="https://doi.org/10.1007/978-3-540-78800-3_33" class="nowrap">doi:10.1007/978-3-540-78800-3_33</a></td> </tr><tr> <td>[19]</td> <td class="space">Hastie, T.; Tibshirani, R.; Friedman, J., The Elements of Statistical Learning: Data Mining, Inference, and Prediction (2009), New York: Springer, New York · <a href="/1273.62005" class="nowrap">Zbl 1273.62005</a> · <a href="https://doi.org/10.1007/978-0-387-84858-7" class="nowrap">doi:10.1007/978-0-387-84858-7</a></td> </tr><tr> <td>[20]</td> <td class="space">Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL 2004, pp. 232-244 (2004) · <a href="/1325.68147" class="nowrap">Zbl 1325.68147</a></td> </tr><tr> <td>[21]</td> <td class="space">Hong, H.; Din, MSE, Variant quantifier elimination, J. Symb. Comput., 47, 7, 883-901 (2012) · <a href="/1238.14001" class="nowrap">Zbl 1238.14001</a> · <a href="https://doi.org/10.1016/j.jsc.2011.05.014" class="nowrap">doi:10.1016/j.jsc.2011.05.014</a></td> </tr><tr> <td>[22]</td> <td class="space">Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE 2010, pp. 215-224 (2010)</td> </tr><tr> <td>[23]</td> <td class="space">Jhala, R.; Podelski, A.; Rybalchenko, A.; Clarke, E.; Henzinger, T.; Veith, H.; Bloem, R., Predicate abstraction for program verification, Handbook of Model Checking, 447-491 (2018), Cham: Springer, Cham · <a href="/1392.68253" class="nowrap">Zbl 1392.68253</a> · <a href="https://doi.org/10.1007/978-3-319-10575-8_15" class="nowrap">doi:10.1007/978-3-319-10575-8_15</a></td> </tr><tr> <td>[24]</td> <td class="space">Jung, Y.; Lee, W.; Wang, B-Y; Yi, K.; Abdulla, PA; Leino, KRM, Predicate generation for learning-based quantifier-free loop invariant inference, Tools and Algorithms for the Construction and Analysis of Systems, 205-219 (2011), Heidelberg: Springer, Heidelberg · <a href="/1315.68097" class="nowrap">Zbl 1315.68097</a> · <a href="https://doi.org/10.1007/978-3-642-19835-9_17" class="nowrap">doi:10.1007/978-3-642-19835-9_17</a></td> </tr><tr> <td>[25]</td> <td class="space">Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: FSE 2006, pp. 105-116 (2006)</td> </tr><tr> <td>[26]</td> <td class="space">Kovács, L.; Voronkov, A.; Schmidt, RA, Interpolation and symbol elimination, Automated Deduction - CADE-22, 199-213 (2009), Heidelberg: Springer, Heidelberg · <a href="/1250.68193" class="nowrap">Zbl 1250.68193</a> · <a href="https://doi.org/10.1007/978-3-642-02959-2_17" class="nowrap">doi:10.1007/978-3-642-02959-2_17</a></td> </tr><tr> <td>[27]</td> <td class="space">Krajíček, J., Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. Symb. Log., 62, 2, 457-486 (1997) · <a href="/0891.03029" class="nowrap">Zbl 0891.03029</a> · <a href="https://doi.org/10.2307/2275541" class="nowrap">doi:10.2307/2275541</a></td> </tr><tr> <td>[28]</td> <td class="space">Kupferschmid, S.; Becker, B.; Fahrenberg, U.; Tripakis, S., Craig interpolation in the presence of non-linear constraints, Formal Modeling and Analysis of Timed Systems, 240-255 (2011), Heidelberg: Springer, Heidelberg · <a href="/1348.68141" class="nowrap">Zbl 1348.68141</a> · <a href="https://doi.org/10.1007/978-3-642-24310-3_17" class="nowrap">doi:10.1007/978-3-642-24310-3_17</a></td> </tr><tr> <td>[29]</td> <td class="space">Lang, S., Introduction to Diophantine Approximations: New Expanded Edition (2012), New York: Springer, New York</td> </tr><tr> <td>[30]</td> <td class="space">McMillan, KL; Hunt, WA; Somenzi, F., Interpolation and SAT-based model checking, Computer Aided Verification, 1-13 (2003), Heidelberg: Springer, Heidelberg · <a href="/1278.68184" class="nowrap">Zbl 1278.68184</a> · <a href="https://doi.org/10.1007/978-3-540-45069-6_1" class="nowrap">doi:10.1007/978-3-540-45069-6_1</a></td> </tr><tr> <td>[31]</td> <td class="space">McMillan, KL; Jensen, K.; Podelski, A., An interpolating theorem prover, Tools and Algorithms for the Construction and Analysis of Systems, 16-30 (2004), Heidelberg: Springer, Heidelberg · <a href="/1126.68573" class="nowrap">Zbl 1126.68573</a> · <a href="https://doi.org/10.1007/978-3-540-24730-2_2" class="nowrap">doi:10.1007/978-3-540-24730-2_2</a></td> </tr><tr> <td>[32]</td> <td class="space">McMillan, KL; Ramakrishnan, CR; Rehof, J., Quantified invariant generation using an interpolating saturation prover, Tools and Algorithms for the Construction and Analysis of Systems, 413-427 (2008), Heidelberg: Springer, Heidelberg · <a href="/1134.68416" class="nowrap">Zbl 1134.68416</a> · <a href="https://doi.org/10.1007/978-3-540-78800-3_31" class="nowrap">doi:10.1007/978-3-540-78800-3_31</a></td> </tr><tr> <td>[33]</td> <td class="space">Okudono, T.; Nishida, Y.; Kojima, K.; Suenaga, K.; Kido, K.; Hasuo, I.; Chang, B-YE, Sharper and simpler nonlinear interpolants for program verification, Programming Languages and Systems, 491-513 (2017), Cham: Springer, Cham · <a href="/1503.68184" class="nowrap">Zbl 1503.68184</a> · <a href="https://doi.org/10.1007/978-3-319-71237-6_24" class="nowrap">doi:10.1007/978-3-319-71237-6_24</a></td> </tr><tr> <td>[34]</td> <td class="space">Parrilo, PA, Semidefinite programming relaxations for semialgebraic problems, Math. Program., 96, 2, 293-320 (2003) · <a href="/1043.14018" class="nowrap">Zbl 1043.14018</a> · <a href="https://doi.org/10.1007/s10107-003-0387-5" class="nowrap">doi:10.1007/s10107-003-0387-5</a></td> </tr><tr> <td>[35]</td> <td class="space">Pudlák, P., Lower bounds for resolution and cutting plane proofs and monotone computations, J. Symb. Log., 62, 3, 981-998 (1997) · <a href="/0945.03086" class="nowrap">Zbl 0945.03086</a> · <a href="https://doi.org/10.2307/2275583" class="nowrap">doi:10.2307/2275583</a></td> </tr><tr> <td>[36]</td> <td class="space">Rybalchenko, A.; Sofronie-Stokkermans, V.; Cook, B.; Podelski, A., Constraint solving for interpolation, Verification, Model Checking, and Abstract Interpretation, 346-362 (2007), Heidelberg: Springer, Heidelberg · <a href="/1132.68480" class="nowrap">Zbl 1132.68480</a> · <a href="https://doi.org/10.1007/978-3-540-69738-1_25" class="nowrap">doi:10.1007/978-3-540-69738-1_25</a></td> </tr><tr> <td>[37]</td> <td class="space">Sharma, R.; Nori, AV; Aiken, A.; Madhusudan, P.; Seshia, SA, Interpolants as classifiers, Computer Aided Verification, 71-87 (2012), Heidelberg: Springer, Heidelberg · <a href="https://doi.org/10.1007/978-3-642-31424-7_11" class="nowrap">doi:10.1007/978-3-642-31424-7_11</a></td> </tr><tr> <td>[38]</td> <td class="space">Sofronie-Stokkermans, V.; Furbach, U.; Shankar, N., Interpolation in local theory extensions, Automated Reasoning, 235-250 (2006), Heidelberg: Springer, Heidelberg · <a href="/1222.03018" class="nowrap">Zbl 1222.03018</a> · <a href="https://doi.org/10.1007/11814771_21" class="nowrap">doi:10.1007/11814771_21</a></td> </tr><tr> <td>[39]</td> <td class="space">Sofronie-Stokkermans, V.; Olivetti, N.; Tiwari, A., On interpolation and symbol elimination in theory extensions, Automated Reasoning, 273-289 (2016), Cham: Springer, Cham · <a href="/1476.03042" class="nowrap">Zbl 1476.03042</a> · <a href="https://doi.org/10.1007/978-3-319-40229-1_19" class="nowrap">doi:10.1007/978-3-319-40229-1_19</a></td> </tr><tr> <td>[40]</td> <td class="space">Solar-Lezama, A., Rabbah, R.M., Bodík, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI 2005, pp. 281-294 (2005)</td> </tr><tr> <td>[41]</td> <td class="space">Strzeboński, A.W.: Real root isolation for exp-log functions. In: ISSAC 2008, pp. 303-314 (2008) · <a href="/1236.65057" class="nowrap">Zbl 1236.65057</a></td> </tr><tr> <td>[42]</td> <td class="space">Strzeboński, A.W.: Real root isolation for tame elementary functions. In: ISSAC 2009, pp. 341-350 (2009) · <a href="/1237.33015" class="nowrap">Zbl 1237.33015</a></td> </tr><tr> <td>[43]</td> <td class="space">Strzeboński, AW, Cylindrical decomposition for systems transcendental in the first variable, J. Symb. Comput., 46, 11, 1284-1290 (2011) · <a href="/1243.03015" class="nowrap">Zbl 1243.03015</a> · <a href="https://doi.org/10.1016/j.jsc.2011.08.009" class="nowrap">doi:10.1016/j.jsc.2011.08.009</a></td> </tr><tr> <td>[44]</td> <td class="space">Tarski, A., A Decision Method for Elementary Algebra and Geometry (1951), Berkeley: University of California Press, Berkeley · <a href="/0044.25102" class="nowrap">Zbl 0044.25102</a> · <a href="https://doi.org/10.1525/9780520348097" class="nowrap">doi:10.1525/9780520348097</a></td> </tr><tr> <td>[45]</td> <td class="space">Vladimir, V., Pattern recognition using generalized portrait method, Autom. Remote Control, 24, 774-780 (1963)</td> </tr><tr> <td>[46]</td> <td class="space">Yorsh, G.; Musuvathi, M.; Nieuwenhuis, R., A combination method for generating interpolants, Automated Deduction - CADE-20, 353-368 (2005), Heidelberg: Springer, Heidelberg · <a href="/1135.03331" class="nowrap">Zbl 1135.03331</a> · <a href="https://doi.org/10.1007/11532231_26" class="nowrap">doi:10.1007/11532231_26</a></td> </tr><tr> <td>[47]</td> <td class="space">Zhang, J.; Feng, Y., Obtaining exact value by approximate computations, Sci. China Ser. A Math., 50, 9, 1361 (2007) · <a href="/1202.68494" class="nowrap">Zbl 1202.68494</a> · <a href="https://doi.org/10.1007/s11425-007-0092-6" class="nowrap">doi:10.1007/s11425-007-0092-6</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"> © 2025 <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 1535.68448 - zbMATH Open