CINXE.COM

<!DOCTYPE html> <html class="client-nojs vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-sticky-header-enabled vector-toc-available" lang="en" dir="ltr"> <head> <meta charset="UTF-8"> <title>Program synthesis - Wikipedia</title> <script>(function(){var className="client-js vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-sticky-header-enabled vector-toc-available";var cookie=document.cookie.match(/(?:^|; )enwikimwclientpreferences=([^;]+)/);if(cookie){cookie[1].split('%2C').forEach(function(pref){className=className.replace(new RegExp('(^| )'+pref.replace(/-clientpref-\w+$|[^\w-]+/g,'')+'-clientpref-\\w+( |$)'),'$1'+pref+'$2');});}document.documentElement.className=className;}());RLCONF={"wgBreakFrames":false,"wgSeparatorTransformTable":["",""],"wgDigitTransformTable":["",""],"wgDefaultDateFormat":"dmy", "wgMonthNames":["","January","February","March","April","May","June","July","August","September","October","November","December"],"wgRequestId":"78771905-6448-42f5-ae39-591f8b4637dc","wgCanonicalNamespace":"","wgCanonicalSpecialPageName":false,"wgNamespaceNumber":0,"wgPageName":"Program_synthesis","wgTitle":"Program synthesis","wgCurRevisionId":1241784157,"wgRevisionId":1241784157,"wgArticleId":498152,"wgIsArticle":true,"wgIsRedirect":false,"wgAction":"view","wgUserName":null,"wgUserGroups":["*"],"wgCategories":["Harv and Sfn no-target errors","Articles with short description","Short description is different from Wikidata","All articles with unsourced statements","Articles with unsourced statements from June 2010","Articles to be expanded from December 2022","All articles to be expanded","Articles with unsourced statements from May 2016","Programming paradigms"],"wgPageViewLanguage":"en","wgPageContentLanguage":"en","wgPageContentModel":"wikitext","wgRelevantPageName": "Program_synthesis","wgRelevantArticleId":498152,"wgIsProbablyEditable":true,"wgRelevantPageIsProbablyEditable":true,"wgRestrictionEdit":[],"wgRestrictionMove":[],"wgNoticeProject":"wikipedia","wgCiteReferencePreviewsActive":false,"wgFlaggedRevsParams":{"tags":{"status":{"levels":1}}},"wgMediaViewerOnClick":true,"wgMediaViewerEnabledByDefault":true,"wgPopupsFlags":0,"wgVisualEditor":{"pageLanguageCode":"en","pageLanguageDir":"ltr","pageVariantFallbacks":"en"},"wgMFDisplayWikibaseDescriptions":{"search":true,"watchlist":true,"tagline":false,"nearby":true},"wgWMESchemaEditAttemptStepOversample":false,"wgWMEPageLength":20000,"wgEditSubmitButtonLabelPublish":true,"wgULSPosition":"interlanguage","wgULSisCompactLinksEnabled":false,"wgVector2022LanguageInHeader":true,"wgULSisLanguageSelectorEmpty":false,"wgWikibaseItemId":"Q4117718","wgCheckUserClientHintsHeadersJsApi":["brands","architecture","bitness","fullVersionList","mobile","model","platform","platformVersion"], "GEHomepageSuggestedEditsEnableTopics":true,"wgGETopicsMatchModeEnabled":false,"wgGEStructuredTaskRejectionReasonTextInputEnabled":false,"wgGELevelingUpEnabledForUser":false};RLSTATE={"ext.globalCssJs.user.styles":"ready","site.styles":"ready","user.styles":"ready","ext.globalCssJs.user":"ready","user":"ready","user.options":"loading","ext.cite.styles":"ready","ext.pygments":"ready","ext.math.styles":"ready","skins.vector.search.codex.styles":"ready","skins.vector.styles":"ready","skins.vector.icons":"ready","ext.wikimediamessages.styles":"ready","ext.visualEditor.desktopArticleTarget.noscript":"ready","ext.uls.interlanguage":"ready","wikibase.client.init":"ready","ext.wikimediaBadges":"ready"};RLPAGEMODULES=["ext.cite.ux-enhancements","ext.pygments.view","ext.scribunto.logs","site","mediawiki.page.ready","mediawiki.toc","skins.vector.js","ext.centralNotice.geoIP","ext.centralNotice.startUp","ext.gadget.ReferenceTooltips","ext.gadget.switcher","ext.urlShortener.toolbar", "ext.centralauth.centralautologin","mmv.bootstrap","ext.popups","ext.visualEditor.desktopArticleTarget.init","ext.visualEditor.targetLoader","ext.echo.centralauth","ext.eventLogging","ext.wikimediaEvents","ext.navigationTiming","ext.uls.interface","ext.cx.eventlogging.campaigns","ext.cx.uls.quick.actions","wikibase.client.vector-2022","ext.checkUser.clientHints","ext.growthExperiments.SuggestedEditSession"];</script> <script>(RLQ=window.RLQ||[]).push(function(){mw.loader.impl(function(){return["user.options@12s5i",function($,jQuery,require,module){mw.user.tokens.set({"patrolToken":"+\\","watchToken":"+\\","csrfToken":"+\\"}); }];});});</script> <link rel="stylesheet" href="/w/load.php?lang=en&modules=ext.cite.styles%7Cext.math.styles%7Cext.pygments%2CwikimediaBadges%7Cext.uls.interlanguage%7Cext.visualEditor.desktopArticleTarget.noscript%7Cext.wikimediamessages.styles%7Cskins.vector.icons%2Cstyles%7Cskins.vector.search.codex.styles%7Cwikibase.client.init&only=styles&skin=vector-2022"> <script async="" src="/w/load.php?lang=en&modules=startup&only=scripts&raw=1&skin=vector-2022"></script> <meta name="ResourceLoaderDynamicStyles" content=""> <link rel="stylesheet" href="/w/load.php?lang=en&modules=site.styles&only=styles&skin=vector-2022"> <meta name="generator" content="MediaWiki 1.44.0-wmf.16"> <meta name="referrer" content="origin"> <meta name="referrer" content="origin-when-cross-origin"> <meta name="robots" content="max-image-preview:standard"> <meta name="format-detection" content="telephone=no"> <meta name="viewport" content="width=1120"> <meta property="og:title" content="Program synthesis - Wikipedia"> <meta property="og:type" content="website"> <link rel="preconnect" href="//upload.wikimedia.org"> <link rel="alternate" media="only screen and (max-width: 640px)" href="//en.m.wikipedia.org/wiki/Program_synthesis"> <link rel="alternate" type="application/x-wiki" title="Edit this page" href="/w/index.php?title=Program_synthesis&action=edit"> <link rel="apple-touch-icon" href="/static/apple-touch/wikipedia.png"> <link rel="icon" href="/static/favicon/wikipedia.ico"> <link rel="search" type="application/opensearchdescription+xml" href="/w/rest.php/v1/search" title="Wikipedia (en)"> <link rel="EditURI" type="application/rsd+xml" href="//en.wikipedia.org/w/api.php?action=rsd"> <link rel="canonical" href="https://en.wikipedia.org/wiki/Program_synthesis"> <link rel="license" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en"> <link rel="alternate" type="application/atom+xml" title="Wikipedia Atom feed" href="/w/index.php?title=Special:RecentChanges&feed=atom"> <link rel="dns-prefetch" href="//meta.wikimedia.org" /> <link rel="dns-prefetch" href="login.wikimedia.org"> </head> <body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject mw-editable page-Program_synthesis rootpage-Program_synthesis skin-vector-2022 action-view"><a class="mw-jump-link" href="#bodyContent">Jump to content</a> <div class="vector-header-container"> <header class="vector-header mw-header"> <div class="vector-header-start"> <nav class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-dropdown" class="vector-dropdown vector-main-menu-dropdown vector-button-flush-left vector-button-flush-right" title="Main menu" > <input type="checkbox" id="vector-main-menu-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-main-menu-dropdown" class="vector-dropdown-checkbox " aria-label="Main menu" > <label id="vector-main-menu-dropdown-label" for="vector-main-menu-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-menu mw-ui-icon-wikimedia-menu"></span> <span class="vector-dropdown-label-text">Main menu</span> </label> <div class="vector-dropdown-content"> <div id="vector-main-menu-unpinned-container" class="vector-unpinned-container"> <div id="vector-main-menu" class="vector-main-menu vector-pinnable-element"> <div class="vector-pinnable-header vector-main-menu-pinnable-header vector-pinnable-header-unpinned" data-feature-name="main-menu-pinned" data-pinnable-element-id="vector-main-menu" data-pinned-container-id="vector-main-menu-pinned-container" data-unpinned-container-id="vector-main-menu-unpinned-container" > <div class="vector-pinnable-header-label">Main menu</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-main-menu.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-main-menu.unpin">hide</button> </div> <div id="p-navigation" class="vector-menu mw-portlet mw-portlet-navigation" > <div class="vector-menu-heading"> Navigation </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-mainpage-description" class="mw-list-item"><a href="/wiki/Main_Page" title="Visit the main page [z]" accesskey="z"><span>Main page</span></a></li><li id="n-contents" class="mw-list-item"><a href="/wiki/Wikipedia:Contents" title="Guides to browsing Wikipedia"><span>Contents</span></a></li><li id="n-currentevents" class="mw-list-item"><a href="/wiki/Portal:Current_events" title="Articles related to current events"><span>Current events</span></a></li><li id="n-randompage" class="mw-list-item"><a href="/wiki/Special:Random" title="Visit a randomly selected article [x]" accesskey="x"><span>Random article</span></a></li><li id="n-aboutsite" class="mw-list-item"><a href="/wiki/Wikipedia:About" title="Learn about Wikipedia and how it works"><span>About Wikipedia</span></a></li><li id="n-contactpage" class="mw-list-item"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us" title="How to contact Wikipedia"><span>Contact us</span></a></li><li id="n-specialpages" class="mw-list-item"><a href="/wiki/Special:SpecialPages"><span>Special pages</span></a></li> </ul> </div> </div> <div id="p-interaction" class="vector-menu mw-portlet mw-portlet-interaction" > <div class="vector-menu-heading"> Contribute </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-help" class="mw-list-item"><a href="/wiki/Help:Contents" title="Guidance on how to use and edit Wikipedia"><span>Help</span></a></li><li id="n-introduction" class="mw-list-item"><a href="/wiki/Help:Introduction" title="Learn how to edit Wikipedia"><span>Learn to edit</span></a></li><li id="n-portal" class="mw-list-item"><a href="/wiki/Wikipedia:Community_portal" title="The hub for editors"><span>Community portal</span></a></li><li id="n-recentchanges" class="mw-list-item"><a href="/wiki/Special:RecentChanges" title="A list of recent changes to Wikipedia [r]" accesskey="r"><span>Recent changes</span></a></li><li id="n-upload" class="mw-list-item"><a href="/wiki/Wikipedia:File_upload_wizard" title="Add images or other media for use on Wikipedia"><span>Upload file</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> <a href="/wiki/Main_Page" class="mw-logo"> <img class="mw-logo-icon" src="/static/images/icons/wikipedia.png" alt="" aria-hidden="true" height="50" width="50"> <span class="mw-logo-container skin-invert"> <img class="mw-logo-wordmark" alt="Wikipedia" src="/static/images/mobile/copyright/wikipedia-wordmark-en.svg" style="width: 7.5em; height: 1.125em;"> <img class="mw-logo-tagline" alt="The Free Encyclopedia" src="/static/images/mobile/copyright/wikipedia-tagline-en.svg" width="117" height="13" style="width: 7.3125em; height: 0.8125em;"> </span> </a> </div> <div class="vector-header-end"> <div id="p-search" role="search" class="vector-search-box-vue vector-search-box-collapses vector-search-box-show-thumbnail vector-search-box-auto-expand-width vector-search-box"> <a href="/wiki/Special:Search" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only search-toggle" title="Search Wikipedia [f]" accesskey="f"><span class="vector-icon mw-ui-icon-search mw-ui-icon-wikimedia-search"></span> <span>Search</span> </a> <div class="vector-typeahead-search-container"> <div class="cdx-typeahead-search cdx-typeahead-search--show-thumbnail cdx-typeahead-search--auto-expand-width"> <form action="/w/index.php" id="searchform" class="cdx-search-input cdx-search-input--has-end-button"> <div id="simpleSearch" class="cdx-search-input__input-wrapper" data-search-loc="header-moved"> <div class="cdx-text-input cdx-text-input--has-start-icon"> <input class="cdx-text-input__input" type="search" name="search" placeholder="Search Wikipedia" aria-label="Search Wikipedia" autocapitalize="sentences" title="Search Wikipedia [f]" accesskey="f" id="searchInput" > <span class="cdx-text-input__icon cdx-text-input__start-icon"></span> </div> <input type="hidden" name="title" value="Special:Search"> </div> <button class="cdx-button cdx-search-input__end-button">Search</button> </form> </div> </div> </div> <nav class="vector-user-links vector-user-links-wide" aria-label="Personal tools"> <div class="vector-user-links-main"> <div id="p-vector-user-menu-preferences" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-userpage" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-dropdown" class="vector-dropdown " title="Change the appearance of the page's font size, width, and color" > <input type="checkbox" id="vector-appearance-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-appearance-dropdown" class="vector-dropdown-checkbox " aria-label="Appearance" > <label id="vector-appearance-dropdown-label" for="vector-appearance-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-appearance mw-ui-icon-wikimedia-appearance"></span> <span class="vector-dropdown-label-text">Appearance</span> </label> <div class="vector-dropdown-content"> <div id="vector-appearance-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <div id="p-vector-user-menu-notifications" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-overflow" class="vector-menu mw-portlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="https://donate.wikimedia.org/?wmf_source=donate&wmf_medium=sidebar&wmf_campaign=en.wikipedia.org&uselang=en" class=""><span>Donate</span></a> </li> <li id="pt-createaccount-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:CreateAccount&returnto=Program+synthesis" title="You are encouraged to create an account and log in; however, it is not mandatory" class=""><span>Create account</span></a> </li> <li id="pt-login-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:UserLogin&returnto=Program+synthesis" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o" class=""><span>Log in</span></a> </li> </ul> </div> </div> </div> <div id="vector-user-links-dropdown" class="vector-dropdown vector-user-menu vector-button-flush-right vector-user-menu-logged-out" title="Log in and more options" > <input type="checkbox" id="vector-user-links-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-user-links-dropdown" class="vector-dropdown-checkbox " aria-label="Personal tools" > <label id="vector-user-links-dropdown-label" for="vector-user-links-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-ellipsis mw-ui-icon-wikimedia-ellipsis"></span> <span class="vector-dropdown-label-text">Personal tools</span> </label> <div class="vector-dropdown-content"> <div id="p-personal" class="vector-menu mw-portlet mw-portlet-personal user-links-collapsible-item" title="User menu" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport" class="user-links-collapsible-item mw-list-item"><a href="https://donate.wikimedia.org/?wmf_source=donate&wmf_medium=sidebar&wmf_campaign=en.wikipedia.org&uselang=en"><span>Donate</span></a></li><li id="pt-createaccount" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:CreateAccount&returnto=Program+synthesis" title="You are encouraged to create an account and log in; however, it is not mandatory"><span class="vector-icon mw-ui-icon-userAdd mw-ui-icon-wikimedia-userAdd"></span> <span>Create account</span></a></li><li id="pt-login" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:UserLogin&returnto=Program+synthesis" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o"><span class="vector-icon mw-ui-icon-logIn mw-ui-icon-wikimedia-logIn"></span> <span>Log in</span></a></li> </ul> </div> </div> <div id="p-user-menu-anon-editor" class="vector-menu mw-portlet mw-portlet-user-menu-anon-editor" > <div class="vector-menu-heading"> Pages for logged out editors <a href="/wiki/Help:Introduction" aria-label="Learn more about editing"><span>learn more</span></a> </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-anoncontribs" class="mw-list-item"><a href="/wiki/Special:MyContributions" title="A list of edits made from this IP address [y]" accesskey="y"><span>Contributions</span></a></li><li id="pt-anontalk" class="mw-list-item"><a href="/wiki/Special:MyTalk" title="Discussion about edits from this IP address [n]" accesskey="n"><span>Talk</span></a></li> </ul> </div> </div> </div> </div> </nav> </div> </header> </div> <div class="mw-page-container"> <div class="mw-page-container-inner"> <div class="vector-sitenotice-container"> <div id="siteNotice"></div> </div> <div class="vector-column-start"> <div class="vector-main-menu-container"> <div id="mw-navigation"> <nav id="mw-panel" class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-pinned-container" class="vector-pinned-container"> </div> </nav> </div> </div> <div class="vector-sticky-pinned-container"> <nav id="mw-panel-toc" aria-label="Contents" data-event-name="ui.sidebar-toc" class="mw-table-of-contents-container vector-toc-landmark"> <div id="vector-toc-pinned-container" class="vector-pinned-container"> <div id="vector-toc" class="vector-toc vector-pinnable-element"> <div class="vector-pinnable-header vector-toc-pinnable-header vector-pinnable-header-pinned" data-feature-name="toc-pinned" data-pinnable-element-id="vector-toc" > <h2 class="vector-pinnable-header-label">Contents</h2> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-toc.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-toc.unpin">hide</button> </div> <ul class="vector-toc-contents" id="mw-panel-toc-list"> <li id="toc-mw-content-text" class="vector-toc-list-item vector-toc-level-1"> <a href="#" class="vector-toc-link"> <div class="vector-toc-text">(Top)</div> </a> </li> <li id="toc-Origin" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Origin"> <div class="vector-toc-text"> <span class="vector-toc-numb">1</span> <span>Origin</span> </div> </a> <ul id="toc-Origin-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-21st_century_developments" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#21st_century_developments"> <div class="vector-toc-text"> <span class="vector-toc-numb">2</span> <span>21st century developments</span> </div> </a> <button aria-controls="toc-21st_century_developments-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Toggle 21st century developments subsection</span> </button> <ul id="toc-21st_century_developments-sublist" class="vector-toc-list"> <li id="toc-Syntax-guided_synthesis" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Syntax-guided_synthesis"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.1</span> <span>Syntax-guided synthesis</span> </div> </a> <ul id="toc-Syntax-guided_synthesis-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Counter-example_guided_inductive_synthesis" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Counter-example_guided_inductive_synthesis"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.2</span> <span>Counter-example guided inductive synthesis</span> </div> </a> <ul id="toc-Counter-example_guided_inductive_synthesis-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-The_framework_of_Manna_and_Waldinger" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#The_framework_of_Manna_and_Waldinger"> <div class="vector-toc-text"> <span class="vector-toc-numb">3</span> <span>The framework of Manna and Waldinger</span> </div> </a> <button aria-controls="toc-The_framework_of_Manna_and_Waldinger-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Toggle The framework of Manna and Waldinger subsection</span> </button> <ul id="toc-The_framework_of_Manna_and_Waldinger-sublist" class="vector-toc-list"> <li id="toc-Proof_rules" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Proof_rules"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.1</span> <span>Proof rules</span> </div> </a> <ul id="toc-Proof_rules-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Example" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Example"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.2</span> <span>Example</span> </div> </a> <ul id="toc-Example-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-See_also" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#See_also"> <div class="vector-toc-text"> <span class="vector-toc-numb">4</span> <span>See also</span> </div> </a> <ul id="toc-See_also-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Notes" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Notes"> <div class="vector-toc-text"> <span class="vector-toc-numb">5</span> <span>Notes</span> </div> </a> <ul id="toc-Notes-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-References" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#References"> <div class="vector-toc-text"> <span class="vector-toc-numb">6</span> <span>References</span> </div> </a> <ul id="toc-References-sublist" class="vector-toc-list"> </ul> </li> </ul> </div> </div> </nav> </div> </div> <div class="mw-content-container"> <main id="content" class="mw-body"> <header class="mw-body-header vector-page-titlebar"> <nav aria-label="Contents" class="vector-toc-landmark"> <div id="vector-page-titlebar-toc" class="vector-dropdown vector-page-titlebar-toc vector-button-flush-left" title="Table of Contents" > <input type="checkbox" id="vector-page-titlebar-toc-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-titlebar-toc" class="vector-dropdown-checkbox " aria-label="Toggle the table of contents" > <label id="vector-page-titlebar-toc-label" for="vector-page-titlebar-toc-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-listBullet mw-ui-icon-wikimedia-listBullet"></span> <span class="vector-dropdown-label-text">Toggle the table of contents</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-titlebar-toc-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <h1 id="firstHeading" class="firstHeading mw-first-heading"><span class="mw-page-title-main">Program synthesis</span></h1> <div id="p-lang-btn" class="vector-dropdown mw-portlet mw-portlet-lang" > <input type="checkbox" id="p-lang-btn-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-p-lang-btn" class="vector-dropdown-checkbox mw-interlanguage-selector" aria-label="Go to an article in another language. Available in 4 languages" > <label id="p-lang-btn-label" for="p-lang-btn-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--action-progressive mw-portlet-lang-heading-4" aria-hidden="true" ><span class="vector-icon mw-ui-icon-language-progressive mw-ui-icon-wikimedia-language-progressive"></span> <span class="vector-dropdown-label-text">4 languages</span> </label> <div class="vector-dropdown-content"> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li class="interlanguage-link interwiki-ar mw-list-item"><a href="https://ar.wikipedia.org/wiki/%D8%AA%D9%83%D9%88%D9%8A%D9%86_%D8%A7%D9%84%D8%A8%D8%B1%D9%86%D8%A7%D9%85%D8%AC" title="تكوين البرنامج – Arabic" lang="ar" hreflang="ar" data-title="تكوين البرنامج" data-language-autonym="العربية" data-language-local-name="Arabic" class="interlanguage-link-target"><span>العربية</span></a></li><li class="interlanguage-link interwiki-fr mw-list-item"><a href="https://fr.wikipedia.org/wiki/Synth%C3%A8se_de_programmes" title="Synthèse de programmes – French" lang="fr" hreflang="fr" data-title="Synthèse de programmes" data-language-autonym="Français" data-language-local-name="French" class="interlanguage-link-target"><span>Français</span></a></li><li class="interlanguage-link interwiki-ko mw-list-item"><a href="https://ko.wikipedia.org/wiki/%ED%94%84%EB%A1%9C%EA%B7%B8%EB%9E%A8_%ED%95%A9%EC%84%B1" title="프로그램 합성 – Korean" lang="ko" hreflang="ko" data-title="프로그램 합성" data-language-autonym="한국어" data-language-local-name="Korean" class="interlanguage-link-target"><span>한국어</span></a></li><li class="interlanguage-link interwiki-ja mw-list-item"><a href="https://ja.wikipedia.org/wiki/%E3%83%97%E3%83%AD%E3%82%B0%E3%83%A9%E3%83%A0%E5%90%88%E6%88%90" title="プログラム合成 – Japanese" lang="ja" hreflang="ja" data-title="プログラム合成" data-language-autonym="日本語" data-language-local-name="Japanese" class="interlanguage-link-target"><span>日本語</span></a></li> </ul> <div class="after-portlet after-portlet-lang"><span class="wb-langlinks-edit wb-langlinks-link"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q4117718#sitelinks-wikipedia" title="Edit interlanguage links" class="wbc-editpage">Edit links</a></span></div> </div> </div> </div> </header> <div class="vector-page-toolbar"> <div class="vector-page-toolbar-container"> <div id="left-navigation"> <nav aria-label="Namespaces"> <div id="p-associated-pages" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-associated-pages" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-nstab-main" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/Program_synthesis" title="View the content page [c]" accesskey="c"><span>Article</span></a></li><li id="ca-talk" class="vector-tab-noicon mw-list-item"><a href="/wiki/Talk:Program_synthesis" rel="discussion" title="Discuss improvements to the content page [t]" accesskey="t"><span>Talk</span></a></li> </ul> </div> </div> <div id="vector-variants-dropdown" class="vector-dropdown emptyPortlet" > <input type="checkbox" id="vector-variants-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-variants-dropdown" class="vector-dropdown-checkbox " aria-label="Change language variant" > <label id="vector-variants-dropdown-label" for="vector-variants-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">English</span> </label> <div class="vector-dropdown-content"> <div id="p-variants" class="vector-menu mw-portlet mw-portlet-variants emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> </div> </div> </nav> </div> <div id="right-navigation" class="vector-collapsible"> <nav aria-label="Views"> <div id="p-views" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-views" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-view" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/Program_synthesis"><span>Read</span></a></li><li id="ca-edit" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Program_synthesis&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-history" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Program_synthesis&action=history" title="Past revisions of this page [h]" accesskey="h"><span>View history</span></a></li> </ul> </div> </div> </nav> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-dropdown" class="vector-dropdown vector-page-tools-dropdown" > <input type="checkbox" id="vector-page-tools-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-tools-dropdown" class="vector-dropdown-checkbox " aria-label="Tools" > <label id="vector-page-tools-dropdown-label" for="vector-page-tools-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">Tools</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-tools-unpinned-container" class="vector-unpinned-container"> <div id="vector-page-tools" class="vector-page-tools vector-pinnable-element"> <div class="vector-pinnable-header vector-page-tools-pinnable-header vector-pinnable-header-unpinned" data-feature-name="page-tools-pinned" data-pinnable-element-id="vector-page-tools" data-pinned-container-id="vector-page-tools-pinned-container" data-unpinned-container-id="vector-page-tools-unpinned-container" > <div class="vector-pinnable-header-label">Tools</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-page-tools.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-page-tools.unpin">hide</button> </div> <div id="p-cactions" class="vector-menu mw-portlet mw-portlet-cactions emptyPortlet vector-has-collapsible-items" title="More options" > <div class="vector-menu-heading"> Actions </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-more-view" class="selected vector-more-collapsible-item mw-list-item"><a href="/wiki/Program_synthesis"><span>Read</span></a></li><li id="ca-more-edit" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Program_synthesis&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-more-history" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Program_synthesis&action=history"><span>View history</span></a></li> </ul> </div> </div> <div id="p-tb" class="vector-menu mw-portlet mw-portlet-tb" > <div class="vector-menu-heading"> General </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-whatlinkshere" class="mw-list-item"><a href="/wiki/Special:WhatLinksHere/Program_synthesis" title="List of all English Wikipedia pages containing links to this page [j]" accesskey="j"><span>What links here</span></a></li><li id="t-recentchangeslinked" class="mw-list-item"><a href="/wiki/Special:RecentChangesLinked/Program_synthesis" rel="nofollow" title="Recent changes in pages linked from this page [k]" accesskey="k"><span>Related changes</span></a></li><li id="t-upload" class="mw-list-item"><a href="//en.wikipedia.org/wiki/Wikipedia:File_Upload_Wizard" title="Upload files [u]" accesskey="u"><span>Upload file</span></a></li><li id="t-permalink" class="mw-list-item"><a href="/w/index.php?title=Program_synthesis&oldid=1241784157" title="Permanent link to this revision of this page"><span>Permanent link</span></a></li><li id="t-info" class="mw-list-item"><a href="/w/index.php?title=Program_synthesis&action=info" title="More information about this page"><span>Page information</span></a></li><li id="t-cite" class="mw-list-item"><a href="/w/index.php?title=Special:CiteThisPage&page=Program_synthesis&id=1241784157&wpFormIdentifier=titleform" title="Information on how to cite this page"><span>Cite this page</span></a></li><li id="t-urlshortener" class="mw-list-item"><a href="/w/index.php?title=Special:UrlShortener&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FProgram_synthesis"><span>Get shortened URL</span></a></li><li id="t-urlshortener-qrcode" class="mw-list-item"><a href="/w/index.php?title=Special:QrCode&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FProgram_synthesis"><span>Download QR code</span></a></li> </ul> </div> </div> <div id="p-coll-print_export" class="vector-menu mw-portlet mw-portlet-coll-print_export" > <div class="vector-menu-heading"> Print/export </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="coll-download-as-rl" class="mw-list-item"><a href="/w/index.php?title=Special:DownloadAsPdf&page=Program_synthesis&action=show-download-screen" title="Download this page as a PDF file"><span>Download as PDF</span></a></li><li id="t-print" class="mw-list-item"><a href="/w/index.php?title=Program_synthesis&printable=yes" title="Printable version of this page [p]" accesskey="p"><span>Printable version</span></a></li> </ul> </div> </div> <div id="p-wikibase-otherprojects" class="vector-menu mw-portlet mw-portlet-wikibase-otherprojects" > <div class="vector-menu-heading"> In other projects </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-wikibase" class="wb-otherproject-link wb-otherproject-wikibase-dataitem mw-list-item"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q4117718" title="Structured data on this page hosted by Wikidata [g]" accesskey="g"><span>Wikidata item</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> </div> </div> </div> <div class="vector-column-end"> <div class="vector-sticky-pinned-container"> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-pinned-container" class="vector-pinned-container"> </div> </nav> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-pinned-container" class="vector-pinned-container"> <div id="vector-appearance" class="vector-appearance vector-pinnable-element"> <div class="vector-pinnable-header vector-appearance-pinnable-header vector-pinnable-header-pinned" data-feature-name="appearance-pinned" data-pinnable-element-id="vector-appearance" data-pinned-container-id="vector-appearance-pinned-container" data-unpinned-container-id="vector-appearance-unpinned-container" > <div class="vector-pinnable-header-label">Appearance</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-appearance.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-appearance.unpin">hide</button> </div> </div> </div> </nav> </div> </div> <div id="bodyContent" class="vector-body" aria-labelledby="firstHeading" data-mw-ve-target-container> <div class="vector-body-before-content"> <div class="mw-indicators"> </div> <div id="siteSub" class="noprint">From Wikipedia, the free encyclopedia</div> </div> <div id="contentSub"><div id="mw-content-subtitle"></div></div> <div id="mw-content-text" class="mw-body-content"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr"><div class="shortdescription nomobile noexcerpt noprint searchaux" style="display:none">Task to construct a program meeting a formal specification</div> <p>In <a href="/wiki/Computer_science" title="Computer science">computer science</a>, <b>program synthesis</b> is the task to construct a <a href="/wiki/Computer_program" title="Computer program">program</a> that <a href="/wiki/Provably_correct" class="mw-redirect" title="Provably correct">provably</a> satisfies a given high-level <a href="/wiki/Formal_specification" title="Formal specification">formal specification</a>. In contrast to <a href="/wiki/Program_verification" class="mw-redirect" title="Program verification">program verification</a>, the program is to be constructed rather than given; however, both fields make use of formal proof techniques, and both comprise approaches of different degrees of automation. In contrast to <a href="/wiki/Automatic_programming" title="Automatic programming">automatic programming</a> techniques, specifications in program synthesis are usually non-<a href="/wiki/Algorithm" title="Algorithm">algorithmic</a> statements in an appropriate <a href="/wiki/Formal_system" title="Formal system">logical calculus</a>.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> </p><p>The primary application of program synthesis is to relieve the programmer of the burden of writing correct, efficient code that satisfies a specification. However, program synthesis also has applications to <a href="/wiki/Superoptimization" title="Superoptimization">superoptimization</a> and inference of <a href="/wiki/Loop_invariant" title="Loop invariant">loop invariants</a>.<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> </p> <meta property="mw:PageProp/toc" /> <div class="mw-heading mw-heading2"><h2 id="Origin">Origin</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Program_synthesis&action=edit&section=1" title="Edit section: Origin"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>During the Summer Institute of Symbolic Logic at Cornell University in 1957, <a href="/wiki/Alonzo_Church" title="Alonzo Church">Alonzo Church</a> defined the problem to synthesize a circuit from mathematical requirements.<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> Even though the work only refers to circuits and not programs, the work is considered to be one of the earliest descriptions of program synthesis and some researchers refer to program synthesis as "Church's Problem". In the 1960s, a similar idea for an "automatic programmer" was explored by researchers in artificial intelligence.<sup class="noprint Inline-Template Template-Fact" style="white-space:nowrap;">[<i><a href="/wiki/Wikipedia:Citation_needed" title="Wikipedia:Citation needed"><span title="This claim needs references to reliable sources. (June 2010)">citation needed</span></a></i>]</sup> </p><p>Since then, various research communities considered the problem of program synthesis. Notable works include the 1969 automata-theoretic approach by <a href="/wiki/Julius_Richard_B%C3%BCchi" title="Julius Richard Büchi">Büchi</a> and <a href="/wiki/Lawrence_Landweber" title="Lawrence Landweber">Landweber</a>,<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup> and the works by <a href="/wiki/Zohar_Manna" title="Zohar Manna">Manna</a> and <a href="/wiki/Richard_Waldinger" title="Richard Waldinger">Waldinger</a> (c. 1980). The development of modern <a href="/wiki/High-level_programming_language" title="High-level programming language">high-level programming languages</a> can also be understood as a form of program synthesis. </p> <div class="mw-heading mw-heading2"><h2 id="21st_century_developments">21st century developments</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Program_synthesis&action=edit&section=2" title="Edit section: 21st century developments"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1251242444">.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}</style><table class="box-Expand_section plainlinks metadata ambox mbox-small-left ambox-content" role="presentation"><tbody><tr><td class="mbox-image"><span typeof="mw:File"><a href="/wiki/File:Wiki_letter_w_cropped.svg" class="mw-file-description"><img alt="[icon]" src="//upload.wikimedia.org/wikipedia/commons/thumb/1/1c/Wiki_letter_w_cropped.svg/20px-Wiki_letter_w_cropped.svg.png" decoding="async" width="20" height="14" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/1/1c/Wiki_letter_w_cropped.svg/30px-Wiki_letter_w_cropped.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/1/1c/Wiki_letter_w_cropped.svg/40px-Wiki_letter_w_cropped.svg.png 2x" data-file-width="44" data-file-height="31" /></a></span></td><td class="mbox-text"><div class="mbox-text-span">This section <b>needs expansion</b> with: a more detailed overview of contemporary approaches. You can help by <a class="external text" href="https://en.wikipedia.org/w/index.php?title=Program_synthesis&action=edit&section=">adding to it</a>. <span class="date-container"><i>(<span class="date">December 2022</span>)</i></span></div></td></tr></tbody></table> <p>The early 21st century has seen a surge of practical interest in the idea of program synthesis in the <a href="/wiki/Formal_verification" title="Formal verification">formal verification</a> community and related fields. Armando Solar-Lezama showed that it is possible to encode program synthesis problems in <a href="/wiki/Boolean_logic" class="mw-redirect" title="Boolean logic">Boolean logic</a> and use algorithms for the <a href="/wiki/Boolean_satisfiability_problem" title="Boolean satisfiability problem">Boolean satisfiability problem</a> to automatically find programs.<sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup> </p> <div class="mw-heading mw-heading3"><h3 id="Syntax-guided_synthesis">Syntax-guided synthesis</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Program_synthesis&action=edit&section=3" title="Edit section: Syntax-guided synthesis"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>In 2013, a unified framework for program synthesis problems called Syntax-guided Synthesis (stylized SyGuS) was proposed by researchers at <a href="/wiki/UPenn" class="mw-redirect" title="UPenn">UPenn</a>, <a href="/wiki/UC_Berkeley" class="mw-redirect" title="UC Berkeley">UC Berkeley</a>, and <a href="/wiki/MIT" class="mw-redirect" title="MIT">MIT</a>.<sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite-bracket">[</span>6<span class="cite-bracket">]</span></a></sup> The input to a SyGuS algorithm consists of a logical specification along with a <a href="/wiki/Context-free_grammar" title="Context-free grammar">context-free grammar</a> of expressions that constrains the syntax of valid solutions.<sup id="cite_ref-7" class="reference"><a href="#cite_note-7"><span class="cite-bracket">[</span>7<span class="cite-bracket">]</span></a></sup> For example, to synthesize a function <var style="padding-right: 1px;">f</var> that returns the maximum of two integers, the logical specification might look like this: </p><p><span class="texhtml">(<i>f</i>(<i>x</i>,<i>y</i>) = <i>x</i> ∨ <i>f</i>(<i>x</i>,<i>y</i>) = <i>y</i>) ∧ <i>f</i>(<i>x</i>,<i>y</i>) ≥ x ∧ <i>f</i>(<i>x</i>,<i>y</i>) ≥ y</span> </p><p>and the grammar might be: </p> <div class="mw-highlight mw-highlight-lang-bnf mw-content-ltr" dir="ltr"><pre><span></span><span class="p"><</span><span class="nc">Exp</span><span class="p">></span> <span class="o">::=</span> x | y | 0 | 1 | <span class="p"><</span><span class="nc">Exp</span><span class="p">></span> + <span class="p"><</span><span class="nc">Exp</span><span class="p">></span> | ite(<span class="p"><</span><span class="nc">Cond</span><span class="p">></span>, <span class="p"><</span><span class="nc">Exp</span><span class="p">></span>, <span class="p"><</span><span class="nc">Exp</span><span class="p">></span>) <span class="p"><</span><span class="nc">Cond</span><span class="p">></span> <span class="o">::=</span> <span class="p"><</span><span class="nc">Exp</span><span class="p">></span> <= <span class="p"><</span><span class="nc">Exp</span><span class="p">></span> </pre></div> <p>where "ite" stands for "if-then-else". The expression </p> <pre>ite(x <= y, y, x) </pre> <p>would be a valid solution, because it conforms to the grammar and the specification. </p><p>From 2014 through 2019, the yearly Syntax-Guided Synthesis Competition (or SyGuS-Comp) compared the different algorithms for program synthesis in a competitive event.<sup id="cite_ref-8" class="reference"><a href="#cite_note-8"><span class="cite-bracket">[</span>8<span class="cite-bracket">]</span></a></sup> The competition used a standardized input format, SyGuS-IF, based on <a href="/wiki/SMT-LIB" class="mw-redirect" title="SMT-LIB">SMT-Lib 2</a>. For example, the following SyGuS-IF encodes the problem of synthesizing the maximum of two integers (as presented above): </p> <pre>(set-logic LIA) (synth-fun f ((x Int) (y Int)) Int ((i Int) (c Int) (b Bool)) ((i Int (c x y (+ i i) (ite b i i))) (c Int (0 1)) (b Bool ((<= i i))))) (declare-var x Int) (declare-var y Int) (constraint (>= (f x y) x)) (constraint (>= (f x y) y)) (constraint (or (= (f x y) x) (= (f x y) y))) (check-synth) </pre> <p>A compliant solver might return the following output: </p> <pre>((define-fun f ((x Int) (y Int)) Int (ite (<= x y) y x))) </pre> <div class="mw-heading mw-heading3"><h3 id="Counter-example_guided_inductive_synthesis">Counter-example guided inductive synthesis</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Program_synthesis&action=edit&section=4" title="Edit section: Counter-example guided inductive synthesis"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Counter-example guided inductive synthesis (CEGIS) is an effective approach to building sound program synthesizers.<sup id="cite_ref-9" class="reference"><a href="#cite_note-9"><span class="cite-bracket">[</span>9<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-10" class="reference"><a href="#cite_note-10"><span class="cite-bracket">[</span>10<span class="cite-bracket">]</span></a></sup> CEGIS involves the interplay of two components: a <i>generator</i> which generates candidate programs, and a <i>verifier</i> which checks whether the candidates satisfy the specification. </p><p>Given a set of inputs <var style="padding-right: 1px;">I</var>, a set of possible programs <var style="padding-right: 1px;">P</var>, and a specification <var style="padding-right: 1px;">S</var>, the goal of program synthesis is to find a program <var style="padding-right: 1px;">p</var> in <var style="padding-right: 1px;">P</var> such that for all inputs <var style="padding-right: 1px;">i</var> in <var style="padding-right: 1px;">I</var>, <var style="padding-right: 1px;">S</var>(<var style="padding-right: 1px;">p</var>, <var style="padding-right: 1px;">i</var>) holds. CEGIS is parameterized over a generator and a verifier: </p> <ul><li>The <i>generator</i> takes a set of inputs <var style="padding-right: 1px;">T</var>, and outputs a candidate program <var style="padding-right: 1px;">c</var> that is correct on all the inputs in <var style="padding-right: 1px;">T</var>, that is, a candidate such that for all inputs <var style="padding-right: 1px;">t</var> in <var style="padding-right: 1px;">T</var>, <var style="padding-right: 1px;">S</var>(<var style="padding-right: 1px;">c</var>, <var style="padding-right: 1px;">t</var>) holds.</li> <li>The <i>verifier</i> takes a candidate program <var style="padding-right: 1px;">c</var> and returns <i>true</i> if the program satisfies <var style="padding-right: 1px;">S</var> on all inputs, and otherwise returns a <i>counterexample</i>, that is, an input <var style="padding-right: 1px;">e</var> in <var style="padding-right: 1px;">I</var> such that <var style="padding-right: 1px;">S</var>(<var style="padding-right: 1px;">c</var>, <var style="padding-right: 1px;">e</var>) fails.</li></ul> <p>CEGIS runs the generator and verifier run in a loop, accumulating counter-examples: </p> <pre><b>algorithm</b> cegis <b>is</b> <b>input</b>: Program generator <i>generate</i>, verifier <i>verify</i>, specification <i>spec</i>, <b>output</b>: Program that satisfies <i>spec</i>, or failure <i>inputs</i> := empty set <b>loop</b> <i>candidate</i> := <i>generate</i>(<i>spec</i>, <i>inputs</i>) <b>if</b> <i>verify</i>(<i>spec</i>, <i>candidate</i>) <b>then</b> <b>return</b> <i>candidate</i> <b>else</b> <i>verify</i> yields a counterexample <i>e</i> add <i>e</i> to <i>inputs</i> <b>end if</b> </pre> <p>Implementations of CEGIS typically use <a href="/wiki/SMT_solver" class="mw-redirect" title="SMT solver">SMT solvers</a> as verifiers. </p><p>CEGIS was inspired by <a href="/wiki/Counterexample-guided_abstraction_refinement" title="Counterexample-guided abstraction refinement">counterexample-guided abstraction refinement</a> (CEGAR).<sup id="cite_ref-11" class="reference"><a href="#cite_note-11"><span class="cite-bracket">[</span>11<span class="cite-bracket">]</span></a></sup> </p> <div class="mw-heading mw-heading2"><h2 id="The_framework_of_Manna_and_Waldinger">The framework of Manna and Waldinger</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Program_synthesis&action=edit&section=5" title="Edit section: The framework of Manna and Waldinger"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <table class="wikitable" style="float:right;"> <caption>Non-clausal resolution rules (unifying substitutions not shown) </caption> <tbody><tr> <th>Nr</th> <th>Assertions</th> <th>Goals</th> <th>Program</th> <th>Origin </th></tr> <tr> <td>51</td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle E[p]}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>E</mi> <mo stretchy="false">[</mo> <mi>p</mi> <mo stretchy="false">]</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle E[p]}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/183127911e396aa5bec41e2f3e4c71d1d3fc3b1f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.239ex; height:2.843ex;" alt="{\displaystyle E[p]}"></span></td> <td></td> <td></td> <td> </td></tr> <tr> <td>52</td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F[p]}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> <mo stretchy="false">[</mo> <mi>p</mi> <mo stretchy="false">]</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F[p]}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/38f8a6d48ca352c71da6f0955c23e9be49548f75" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.204ex; height:2.843ex;" alt="{\displaystyle F[p]}"></span></td> <td></td> <td></td> <td> </td></tr> <tr> <td>53</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle G[p]}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>G</mi> <mo stretchy="false">[</mo> <mi>p</mi> <mo stretchy="false">]</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle G[p]}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fad4bb12f47ce1590009cc40e7cb8798d4abd3b4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.29ex; height:2.843ex;" alt="{\displaystyle G[p]}"></span></td> <td>s</td> <td> </td></tr> <tr> <td>54</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle H[p]}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>H</mi> <mo stretchy="false">[</mo> <mi>p</mi> <mo stretchy="false">]</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle H[p]}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/cabc873d77cf7398850a079339ef68aec423d9a5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.527ex; height:2.843ex;" alt="{\displaystyle H[p]}"></span></td> <td>t</td> <td> </td></tr> <tr> <td>55</td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle E[{\text{true}}]\lor F[{\text{false}}]}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>E</mi> <mo stretchy="false">[</mo> <mrow class="MJX-TeXAtom-ORD"> <mtext>true</mtext> </mrow> <mo stretchy="false">]</mo> <mo>∨</mo> <mi>F</mi> <mo stretchy="false">[</mo> <mrow class="MJX-TeXAtom-ORD"> <mtext>false</mtext> </mrow> <mo stretchy="false">]</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle E[{\text{true}}]\lor F[{\text{false}}]}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4253600db2f4e67cc3fe3a5324b7f0e7f9c170b3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.297ex; height:2.843ex;" alt="{\displaystyle E[{\text{true}}]\lor F[{\text{false}}]}"></span></td> <td></td> <td></td> <td>Resolve(51,52) </td></tr> <tr> <td>56</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot F[{\text{true}}]\land G[{\text{false}}]}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi>F</mi> <mo stretchy="false">[</mo> <mrow class="MJX-TeXAtom-ORD"> <mtext>true</mtext> </mrow> <mo stretchy="false">]</mo> <mo>∧</mo> <mi>G</mi> <mo stretchy="false">[</mo> <mrow class="MJX-TeXAtom-ORD"> <mtext>false</mtext> </mrow> <mo stretchy="false">]</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot F[{\text{true}}]\land G[{\text{false}}]}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/12de02b2283224d41387db0d2e99c9961baa0c37" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.899ex; height:2.843ex;" alt="{\displaystyle \lnot F[{\text{true}}]\land G[{\text{false}}]}"></span></td> <td>s</td> <td>Resolve(52,53) </td></tr> <tr> <td>57</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot F[{\text{false}}]\land G[{\text{true}}]}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi>F</mi> <mo stretchy="false">[</mo> <mrow class="MJX-TeXAtom-ORD"> <mtext>false</mtext> </mrow> <mo stretchy="false">]</mo> <mo>∧</mo> <mi>G</mi> <mo stretchy="false">[</mo> <mrow class="MJX-TeXAtom-ORD"> <mtext>true</mtext> </mrow> <mo stretchy="false">]</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot F[{\text{false}}]\land G[{\text{true}}]}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f08706bfdedee51052e87a91b1bf2e626aca7802" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.899ex; height:2.843ex;" alt="{\displaystyle \lnot F[{\text{false}}]\land G[{\text{true}}]}"></span></td> <td>s</td> <td>Resolve(53,52) </td></tr> <tr> <td>58</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle G[{\text{true}}]\land H[{\text{false}}]}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>G</mi> <mo stretchy="false">[</mo> <mrow class="MJX-TeXAtom-ORD"> <mtext>true</mtext> </mrow> <mo stretchy="false">]</mo> <mo>∧</mo> <mi>H</mi> <mo stretchy="false">[</mo> <mrow class="MJX-TeXAtom-ORD"> <mtext>false</mtext> </mrow> <mo stretchy="false">]</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle G[{\text{true}}]\land H[{\text{false}}]}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/224d17282e11087b284236fa5a769306c0c23d30" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.671ex; height:2.843ex;" alt="{\displaystyle G[{\text{true}}]\land H[{\text{false}}]}"></span></td> <td>p <a href="/wiki/%3F:" class="mw-redirect" title="?:">?</a> s <a href="/wiki/%3F:" class="mw-redirect" title="?:">:</a> t</td> <td>Resolve(53,54) </td></tr></tbody></table> <p>The framework of <a href="/wiki/Zohar_Manna" title="Zohar Manna">Manna</a> and <a href="/wiki/Richard_Waldinger" title="Richard Waldinger">Waldinger</a>, published in 1980,<sup id="cite_ref-12" class="reference"><a href="#cite_note-12"><span class="cite-bracket">[</span>12<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-13" class="reference"><a href="#cite_note-13"><span class="cite-bracket">[</span>13<span class="cite-bracket">]</span></a></sup> starts from a user-given <a href="/wiki/First-order_logic" title="First-order logic">first-order specification formula</a>. For that formula, a proof is constructed, thereby also synthesizing a <a href="/wiki/Functional_program" class="mw-redirect" title="Functional program">functional program</a> from <a href="/wiki/Unification_(computer_science)#Syntactic_unification_of_first-order_terms" title="Unification (computer science)">unifying</a> substitutions. </p><p>The framework is presented in a table layout, the columns containing: </p> <ul><li>A line number ("Nr") for reference purposes</li> <li><a href="/wiki/Well-formed_formula#Predicate_logic" title="Well-formed formula">Formulas</a> that already have been established, including axioms and preconditions, ("Assertions")</li> <li>Formulas still to be proven, including postconditions, ("Goals"),<sup id="cite_ref-14" class="reference"><a href="#cite_note-14"><span class="cite-bracket">[</span>note 1<span class="cite-bracket">]</span></a></sup></li> <li><a href="/wiki/Term_(logic)" title="Term (logic)">Terms</a> denoting a valid output value ("Program")<sup id="cite_ref-15" class="reference"><a href="#cite_note-15"><span class="cite-bracket">[</span>note 2<span class="cite-bracket">]</span></a></sup></li> <li>A justification for the current line ("Origin")</li></ul> <p>Initially, background knowledge, pre-conditions, and post-conditions are entered into the table. After that, appropriate proof rules are applied manually. The framework has been designed to enhance human readability of intermediate formulas: contrary to <a href="/wiki/Resolution_(logic)" title="Resolution (logic)">classical resolution</a>, it does not require <a href="/wiki/Clausal_normal_form" class="mw-redirect" title="Clausal normal form">clausal normal form</a>, but allows one to reason with formulas of arbitrary structure and containing any junctors ("<a href="/wiki/Non-clausal_resolution" class="mw-redirect" title="Non-clausal resolution">non-clausal resolution</a>"). The proof is complete when <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\it {true}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi class="MJX-tex-mathit" mathvariant="italic">t</mi> <mi class="MJX-tex-mathit" mathvariant="italic">r</mi> <mi class="MJX-tex-mathit" mathvariant="italic">u</mi> <mi class="MJX-tex-mathit" mathvariant="italic">e</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\it {true}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/5d6eb92039506485a14d4985233b8ce4b47c3f77" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; margin-right: -0.023ex; width:4.095ex; height:2.009ex;" alt="{\displaystyle {\it {true}}}"></span> has been derived in the <i>Goals</i> column, or, equivalently, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\it {false}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi class="MJX-tex-mathit" mathvariant="italic">f</mi> <mi class="MJX-tex-mathit" mathvariant="italic">a</mi> <mi class="MJX-tex-mathit" mathvariant="italic">l</mi> <mi class="MJX-tex-mathit" mathvariant="italic">s</mi> <mi class="MJX-tex-mathit" mathvariant="italic">e</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\it {false}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6aa3fce1eefce9b45d486f6d045dbc82b7a29a0d" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.052ex; margin-right: -0.023ex; width:4.594ex; height:2.509ex;" alt="{\displaystyle {\it {false}}}"></span> in the <i>Assertions</i> column. Programs obtained by this approach are guaranteed to satisfy the specification formula started from; in this sense they are <i>correct by construction</i>.<sup id="cite_ref-16" class="reference"><a href="#cite_note-16"><span class="cite-bracket">[</span>14<span class="cite-bracket">]</span></a></sup> Only a minimalist, yet <a href="/wiki/Turing-complete" class="mw-redirect" title="Turing-complete">Turing-complete</a>,<sup id="cite_ref-17" class="reference"><a href="#cite_note-17"><span class="cite-bracket">[</span>15<span class="cite-bracket">]</span></a></sup> <a href="/wiki/Purely_functional_programming_language" class="mw-redirect" title="Purely functional programming language">purely functional programming language</a>, consisting of conditional, recursion, and arithmetic and other operators<sup id="cite_ref-18" class="reference"><a href="#cite_note-18"><span class="cite-bracket">[</span>note 3<span class="cite-bracket">]</span></a></sup> is supported. Case studies performed within this framework synthesized algorithms to compute e.g. <a href="/wiki/Division_algorithm" title="Division algorithm">division</a>, <a href="/wiki/Remainder" title="Remainder">remainder</a>,<sup id="cite_ref-19" class="reference"><a href="#cite_note-19"><span class="cite-bracket">[</span>16<span class="cite-bracket">]</span></a></sup> <a href="/wiki/Square_root" title="Square root">square root</a>,<sup id="cite_ref-20" class="reference"><a href="#cite_note-20"><span class="cite-bracket">[</span>17<span class="cite-bracket">]</span></a></sup> <a href="/wiki/Unification_(computer_science)" title="Unification (computer science)">term unification</a>,<sup id="cite_ref-21" class="reference"><a href="#cite_note-21"><span class="cite-bracket">[</span>18<span class="cite-bracket">]</span></a></sup> answers to <a href="/wiki/Relational_database" title="Relational database">relational database</a> queries<sup id="cite_ref-22" class="reference"><a href="#cite_note-22"><span class="cite-bracket">[</span>19<span class="cite-bracket">]</span></a></sup> and several <a href="/wiki/Sorting_algorithm" title="Sorting algorithm">sorting algorithms</a>.<sup id="cite_ref-23" class="reference"><a href="#cite_note-23"><span class="cite-bracket">[</span>20<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-24" class="reference"><a href="#cite_note-24"><span class="cite-bracket">[</span>21<span class="cite-bracket">]</span></a></sup> </p> <div class="mw-heading mw-heading3"><h3 id="Proof_rules">Proof rules</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Program_synthesis&action=edit&section=6" title="Edit section: Proof rules"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Proof rules include: </p> <ul><li>Non-clausal <a href="/wiki/Resolution_(logic)" title="Resolution (logic)">resolution</a> (see table).</li></ul> <dl><dd>For example, line 55 is obtained by resolving Assertion formulas <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle E}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>E</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle E}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4232c9de2ee3eec0a9c0a19b15ab92daa6223f9b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.776ex; height:2.176ex;" alt="{\displaystyle E}"></span> from 51 and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"></span> from 52 which both share some common subformula <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>p</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/81eac1e205430d1f40810df36a0edffdc367af36" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}"></span>. The resolvent is formed as the disjunction of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle E}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>E</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle E}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4232c9de2ee3eec0a9c0a19b15ab92daa6223f9b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.776ex; height:2.176ex;" alt="{\displaystyle E}"></span>, with <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>p</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/81eac1e205430d1f40810df36a0edffdc367af36" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}"></span> replaced by <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\it {true}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi class="MJX-tex-mathit" mathvariant="italic">t</mi> <mi class="MJX-tex-mathit" mathvariant="italic">r</mi> <mi class="MJX-tex-mathit" mathvariant="italic">u</mi> <mi class="MJX-tex-mathit" mathvariant="italic">e</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\it {true}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/5d6eb92039506485a14d4985233b8ce4b47c3f77" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; margin-right: -0.023ex; width:4.095ex; height:2.009ex;" alt="{\displaystyle {\it {true}}}"></span>, and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"></span>, with <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>p</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/81eac1e205430d1f40810df36a0edffdc367af36" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}"></span> replaced by <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\it {false}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mi class="MJX-tex-mathit" mathvariant="italic">f</mi> <mi class="MJX-tex-mathit" mathvariant="italic">a</mi> <mi class="MJX-tex-mathit" mathvariant="italic">l</mi> <mi class="MJX-tex-mathit" mathvariant="italic">s</mi> <mi class="MJX-tex-mathit" mathvariant="italic">e</mi> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\it {false}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6aa3fce1eefce9b45d486f6d045dbc82b7a29a0d" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.052ex; margin-right: -0.023ex; width:4.594ex; height:2.509ex;" alt="{\displaystyle {\it {false}}}"></span>. This resolvent logically follows from the conjunction of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle E}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>E</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle E}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4232c9de2ee3eec0a9c0a19b15ab92daa6223f9b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.776ex; height:2.176ex;" alt="{\displaystyle E}"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"></span>. More generally, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle E}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>E</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle E}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4232c9de2ee3eec0a9c0a19b15ab92daa6223f9b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.776ex; height:2.176ex;" alt="{\displaystyle E}"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"></span> need to have only two unifiable subformulas <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>p</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p_{1}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b9b58f22283ca46dd5da309cc34303b06a797783" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:2.313ex; height:2.009ex;" alt="{\displaystyle p_{1}}"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p_{2}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>p</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>2</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p_{2}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/43f1b08d7d69712872e051c2b33fdfa9f5d42319" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:2.313ex; height:2.009ex;" alt="{\displaystyle p_{2}}"></span>, respectively; their resolvent is then formed from <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle E\theta }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>E</mi> <mi>θ</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle E\theta }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f21ca40c3b67a4d4de34b1deb159a313dc3b9cba" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.866ex; height:2.176ex;" alt="{\displaystyle E\theta }"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F\theta }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> <mi>θ</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F\theta }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ee4acbe9e464271f4a9e98dec47e1e3598ac5568" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.831ex; height:2.176ex;" alt="{\displaystyle F\theta }"></span> as before, where <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \theta }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>θ</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \theta }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6e5ab2664b422d53eb0c7df3b87e1360d75ad9af" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.09ex; height:2.176ex;" alt="{\displaystyle \theta }"></span> is the <a href="/wiki/Most_general_unifier" class="mw-redirect" title="Most general unifier">most general unifier</a> of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>p</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p_{1}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b9b58f22283ca46dd5da309cc34303b06a797783" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:2.313ex; height:2.009ex;" alt="{\displaystyle p_{1}}"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p_{2}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>p</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>2</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p_{2}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/43f1b08d7d69712872e051c2b33fdfa9f5d42319" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:2.313ex; height:2.009ex;" alt="{\displaystyle p_{2}}"></span>. This rule generalizes <a href="/wiki/Resolution_(logic)#Resolution_in_first_order_logic" title="Resolution (logic)">resolution of clauses</a>.<sup id="cite_ref-25" class="reference"><a href="#cite_note-25"><span class="cite-bracket">[</span>22<span class="cite-bracket">]</span></a></sup></dd> <dd>Program terms of parent formulas are combined as shown in line 58 to form the output of the resolvent. In the general case, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \theta }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>θ</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \theta }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/6e5ab2664b422d53eb0c7df3b87e1360d75ad9af" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.09ex; height:2.176ex;" alt="{\displaystyle \theta }"></span> is applied to the latter also. Since the subformula <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>p</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle p}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/81eac1e205430d1f40810df36a0edffdc367af36" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}"></span> appears in the output, care must be taken to resolve only on subformulas corresponding to <a href="/wiki/Computable" class="mw-redirect" title="Computable">computable</a> properties.</dd></dl> <ul><li>Logical transformations.</li></ul> <dl><dd>For example, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle E\land (F\lor G)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>E</mi> <mo>∧</mo> <mo stretchy="false">(</mo> <mi>F</mi> <mo>∨</mo> <mi>G</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle E\land (F\lor G)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c04d0ead68dc5e6839c4835aef01b6a63de933ee" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.318ex; height:2.843ex;" alt="{\displaystyle E\land (F\lor G)}"></span> can be transformed to <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (E\land F)\lor (E\land G)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>E</mi> <mo>∧</mo> <mi>F</mi> <mo stretchy="false">)</mo> <mo>∨</mo> <mo stretchy="false">(</mo> <mi>E</mi> <mo>∧</mo> <mi>G</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (E\land F)\lor (E\land G)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ed2ecf7eafe35ca16b37fe198882a04bff383823" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.485ex; height:2.843ex;" alt="{\displaystyle (E\land F)\lor (E\land G)}"></span>) in Assertions as well as in Goals, since both are equivalent.</dd></dl> <ul><li>Splitting of conjunctive assertions and of disjunctive goals.</li></ul> <dl><dd>An example is shown in lines 11 to 13 of the toy example below.</dd></dl> <ul><li><a href="/wiki/Structural_induction" title="Structural induction">Structural induction</a>.</li></ul> <dl><dd>This rule allows for synthesis of <a href="/wiki/Recursive_function_(programming)" class="mw-redirect" title="Recursive function (programming)">recursive functions</a>. For a given pre- and postcondition "Given <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/87f9e315fd7e2ba406057a97300593c4802b53e4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}"></span> such that <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\textit {pre}}(x)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mtext class="MJX-tex-mathit" mathvariant="italic">pre</mtext> </mrow> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\textit {pre}}(x)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/806d09ad2f9ed55d588a930099c87b9920ab3761" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:6.378ex; height:2.843ex;" alt="{\displaystyle {\textit {pre}}(x)}"></span>, find <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f(x)=y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>f</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo stretchy="false">)</mo> <mo>=</mo> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle f(x)=y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/0a5080a8b0a963407ea74ffa50702563771518d1" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.672ex; height:2.843ex;" alt="{\displaystyle f(x)=y}"></span> such that <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\textit {post}}(x,y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mtext class="MJX-tex-mathit" mathvariant="italic">post</mtext> </mrow> </mrow> <mo stretchy="false">(</mo> <mi>x</mi> <mo>,</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\textit {post}}(x,y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/817f872e774180a257469a444733c76679db42b0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.428ex; height:2.843ex;" alt="{\displaystyle {\textit {post}}(x,y)}"></span>", and an appropriate user-given <a href="/wiki/Well-ordering" class="mw-redirect" title="Well-ordering">well-ordering</a> <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \prec }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>≺</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \prec }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/59707ac9078525b52a9e21a1baf9ab787af7a9aa" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.808ex; height:1.843ex;" alt="{\displaystyle \prec }"></span> of the domain of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/87f9e315fd7e2ba406057a97300593c4802b53e4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}"></span>, it is always sound to add an Assertion "<span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mi>x</mi> <mo>′</mo> </msup> <mo>≺</mo> <mi>x</mi> <mo>∧</mo> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mtext class="MJX-tex-mathit" mathvariant="italic">pre</mtext> </mrow> </mrow> <mo stretchy="false">(</mo> <msup> <mi>x</mi> <mo>′</mo> </msup> <mo stretchy="false">)</mo> <mspace width="thickmathspace" /> <mo stretchy="false">⟹</mo> <mspace width="thickmathspace" /> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mtext class="MJX-tex-mathit" mathvariant="italic">post</mtext> </mrow> </mrow> <mo stretchy="false">(</mo> <msup> <mi>x</mi> <mo>′</mo> </msup> <mo>,</mo> <mi>f</mi> <mo stretchy="false">(</mo> <msup> <mi>x</mi> <mo>′</mo> </msup> <mo stretchy="false">)</mo> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/550cd26217a750a4659b7f8750d69e391969cf1f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:36.533ex; height:3.009ex;" alt="{\displaystyle x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))}"></span>".<sup id="cite_ref-26" class="reference"><a href="#cite_note-26"><span class="cite-bracket">[</span>23<span class="cite-bracket">]</span></a></sup> Resolving with this assertion can introduce a recursive call to <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>f</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle f}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/132e57acb643253e7810ee9702d9581f159a1c61" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.279ex; height:2.509ex;" alt="{\displaystyle f}"></span> in the Program term.</dd> <dd>An example is given in Manna, Waldinger (1980), p.108-111, where an algorithm to compute quotient and remainder of two given integers is synthesized, using the well-order <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (n',d')\prec (n,d)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <msup> <mi>n</mi> <mo>′</mo> </msup> <mo>,</mo> <msup> <mi>d</mi> <mo>′</mo> </msup> <mo stretchy="false">)</mo> <mo>≺</mo> <mo stretchy="false">(</mo> <mi>n</mi> <mo>,</mo> <mi>d</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (n',d')\prec (n,d)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fb60eea902bc3bd4c25572503c1ce8c1be651e84" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:15.378ex; height:3.009ex;" alt="{\displaystyle (n',d')\prec (n,d)}"></span> defined by <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 0\leq n'<n}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mn>0</mn> <mo>≤</mo> <msup> <mi>n</mi> <mo>′</mo> </msup> <mo><</mo> <mi>n</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle 0\leq n'<n}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ffc928b10eb6766708dab1a5131635b20ab1445c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:10.834ex; height:2.676ex;" alt="{\displaystyle 0\leq n'<n}"></span> (p.110).</dd></dl> <p>Murray has shown these rules to be <a href="/wiki/Completeness_(logic)" title="Completeness (logic)">complete</a> for <a href="/wiki/First-order_logic" title="First-order logic">first-order logic</a>.<sup id="cite_ref-27" class="reference"><a href="#cite_note-27"><span class="cite-bracket">[</span>24<span class="cite-bracket">]</span></a></sup> In 1986, Manna and Waldinger added generalized E-resolution and <a href="/wiki/Paramodulation" class="mw-redirect" title="Paramodulation">paramodulation</a> rules to handle also equality;<sup id="cite_ref-28" class="reference"><a href="#cite_note-28"><span class="cite-bracket">[</span>25<span class="cite-bracket">]</span></a></sup> later, these rules turned out to be incomplete (but nevertheless <a href="/wiki/Soundness" title="Soundness">sound</a>).<sup id="cite_ref-29" class="reference"><a href="#cite_note-29"><span class="cite-bracket">[</span>26<span class="cite-bracket">]</span></a></sup> </p> <div style="clear:both;" class=""></div> <div class="mw-heading mw-heading3"><h3 id="Example">Example</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Program_synthesis&action=edit&section=7" title="Edit section: Example"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <table class="wikitable" style="float:right;"> <caption>Example synthesis of maximum function </caption> <tbody><tr> <th>Nr</th> <th>Assertions</th> <th>Goals</th> <th>Program</th> <th>Origin </th></tr> <tr> <td>1</td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A=A}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> <mo>=</mo> <mi>A</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A=A}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/87cdf81a86b888d20e63e9c6242283612cd1be8c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.585ex; height:2.176ex;" alt="{\displaystyle A=A}"></span></td> <td></td> <td></td> <td>Axiom </td></tr> <tr> <td>2</td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A\leq A}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> <mo>≤</mo> <mi>A</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A\leq A}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1d5b76467b8592350744c892f469d81dcf5b9c68" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:6.585ex; height:2.343ex;" alt="{\displaystyle A\leq A}"></span></td> <td></td> <td></td> <td>Axiom </td></tr> <tr> <td>3</td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle A\leq B\lor B\leq A}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>A</mi> <mo>≤</mo> <mi>B</mi> <mo>∨</mo> <mi>B</mi> <mo>≤</mo> <mi>A</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle A\leq B\lor B\leq A}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d5cd8d2c3ee629d6e4815b296ab461565989e9a0" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:15.794ex; height:2.343ex;" alt="{\displaystyle A\leq B\lor B\leq A}"></span></td> <td></td> <td></td> <td>Axiom </td></tr> <tr> <td>10</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\leq M\land y\leq M\land (x=M\lor y=M)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mi>y</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mo stretchy="false">(</mo> <mi>x</mi> <mo>=</mo> <mi>M</mi> <mo>∨</mo> <mi>y</mi> <mo>=</mo> <mi>M</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\leq M\land y\leq M\land (x=M\lor y=M)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/8a88fff88037cc08817b2174234e1af98117837c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:36.69ex; height:2.843ex;" alt="{\displaystyle x\leq M\land y\leq M\land (x=M\lor y=M)}"></span></td> <td>M</td> <td>Specification </td></tr> <tr> <td>11</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (x\leq M\land y\leq M\land x=M)\lor (x\leq M\land y\leq M\land y=M)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>x</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mi>y</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mi>x</mi> <mo>=</mo> <mi>M</mi> <mo stretchy="false">)</mo> <mo>∨</mo> <mo stretchy="false">(</mo> <mi>x</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mi>y</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mi>y</mi> <mo>=</mo> <mi>M</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (x\leq M\land y\leq M\land x=M)\lor (x\leq M\land y\leq M\land y=M)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/863f7dacdc3495c798921b978624ff5c621ea3e3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:57.231ex; height:2.843ex;" alt="{\displaystyle (x\leq M\land y\leq M\land x=M)\lor (x\leq M\land y\leq M\land y=M)}"></span></td> <td>M</td> <td>Distr(10) </td></tr> <tr> <td>12</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\leq M\land y\leq M\land x=M}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mi>y</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mi>x</mi> <mo>=</mo> <mi>M</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\leq M\land y\leq M\land x=M}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/071ecb90d45b577c50ac86525a9ec94a0b6a015f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:25.602ex; height:2.509ex;" alt="{\displaystyle x\leq M\land y\leq M\land x=M}"></span></td> <td>M</td> <td>Split(11) </td></tr> <tr> <td>13</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\leq M\land y\leq M\land y=M}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mi>y</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mi>y</mi> <mo>=</mo> <mi>M</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\leq M\land y\leq M\land y=M}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1396ea8e2e7187cf3d4b24449f2c904be6e66283" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:25.428ex; height:2.509ex;" alt="{\displaystyle x\leq M\land y\leq M\land y=M}"></span></td> <td>M</td> <td>Split(11) </td></tr> <tr> <td>14</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\leq x\land y\leq x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≤</mo> <mi>x</mi> <mo>∧</mo> <mi>y</mi> <mo>≤</mo> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\leq x\land y\leq x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/015d21c14b713c625911019c000cc3a8f139bc72" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:13.924ex; height:2.343ex;" alt="{\displaystyle x\leq x\land y\leq x}"></span></td> <td>x</td> <td>Resolve(12,1) </td></tr> <tr> <td>15</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y\leq x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>y</mi> <mo>≤</mo> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle y\leq x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7de6a6e4f44d9dfcbfaadbdcf388d4b8a6fed109" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.584ex; height:2.343ex;" alt="{\displaystyle y\leq x}"></span></td> <td>x</td> <td>Resolve(14,2) </td></tr> <tr> <td>16</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot (x\leq y)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> <mi>x</mi> <mo>≤</mo> <mi>y</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot (x\leq y)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/77c0a6d3d5ea8d3d675a4241dc521541e5b5ebb4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.943ex; height:2.843ex;" alt="{\displaystyle \lnot (x\leq y)}"></span></td> <td>x</td> <td>Resolve(15,3) </td></tr> <tr> <td>17</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\leq y\land y\leq y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≤</mo> <mi>y</mi> <mo>∧</mo> <mi>y</mi> <mo>≤</mo> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\leq y\land y\leq y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/faa0d5f8c05823b10265015377a53a409124a69c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:13.576ex; height:2.343ex;" alt="{\displaystyle x\leq y\land y\leq y}"></span></td> <td>y</td> <td>Resolve(13,1) </td></tr> <tr> <td>18</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\leq y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≤</mo> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\leq y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c07a0bc023490be1c08e6c33a9cdc93bec908224" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.584ex; height:2.343ex;" alt="{\displaystyle x\leq y}"></span></td> <td>y</td> <td>Resolve(17,2) </td></tr> <tr> <td>19</td> <td></td> <td><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\textit {true}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mtext class="MJX-tex-mathit" mathvariant="italic">true</mtext> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\textit {true}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/39477b5045e93ab825d9d763e7f97e541f12851b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; margin-right: -0.023ex; width:4.095ex; height:2.009ex;" alt="{\displaystyle {\textit {true}}}"></span></td> <td>x<y <a href="/wiki/%3F:" class="mw-redirect" title="?:">?</a> y <a href="/wiki/%3F:" class="mw-redirect" title="?:">:</a> x</td> <td>Resolve(18,16) </td></tr></tbody></table> <p>As a toy example, a functional program to compute the maximum <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>M</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle M}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f82cade9898ced02fdd08712e5f0c0151758a0dd" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}"></span> of two numbers <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/87f9e315fd7e2ba406057a97300593c4802b53e4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b8a6208ec717213d4317e666f1ae872e00620a0d" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}"></span> can be derived as follows.<sup class="noprint Inline-Template Template-Fact" style="white-space:nowrap;">[<i><a href="/wiki/Wikipedia:Citation_needed" title="Wikipedia:Citation needed"><span title="This claim needs references to reliable sources. (May 2016)">citation needed</span></a></i>]</sup> </p><p>Starting from the requirement description "<i>The maximum is larger than or equal to any given number, and is one of the given numbers</i>", the first-order formula <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \forall X\forall Y\exists M:X\leq M\land Y\leq M\land (X=M\lor Y=M)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">∀</mi> <mi>X</mi> <mi mathvariant="normal">∀</mi> <mi>Y</mi> <mi mathvariant="normal">∃</mi> <mi>M</mi> <mo>:</mo> <mi>X</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mi>Y</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mo stretchy="false">(</mo> <mi>X</mi> <mo>=</mo> <mi>M</mi> <mo>∨</mo> <mi>Y</mi> <mo>=</mo> <mi>M</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \forall X\forall Y\exists M:X\leq M\land Y\leq M\land (X=M\lor Y=M)}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4d737a296e53a8e65d46298c84d2c7fdba025af7" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:51.237ex; height:2.843ex;" alt="{\displaystyle \forall X\forall Y\exists M:X\leq M\land Y\leq M\land (X=M\lor Y=M)}"></span> is obtained as its formal translation. This formula is to be proved. By reverse <a href="/wiki/Skolemization" class="mw-redirect" title="Skolemization">Skolemization</a>,<sup id="cite_ref-30" class="reference"><a href="#cite_note-30"><span class="cite-bracket">[</span>note 4<span class="cite-bracket">]</span></a></sup> the specification in line 10 is obtained, an upper- and lower-case letter denoting a variable and a <a href="/wiki/Skolem_constant" class="mw-redirect" title="Skolem constant">Skolem constant</a>, respectively. </p><p>After applying a transformation rule for the <a href="/wiki/Distributive_law" class="mw-redirect" title="Distributive law">distributive law</a> in line 11, the proof goal is a disjunction, and hence can be split into two cases, viz. lines 12 and 13. </p><p>Turning to the first case, resolving line 12 with the axiom in line 1 leads to <a href="/wiki/Substitution_(logic)#First-order_logic" title="Substitution (logic)">instantiation</a> of the program variable <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>M</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle M}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f82cade9898ced02fdd08712e5f0c0151758a0dd" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}"></span> in line 14. Intuitively, the last conjunct of line 12 prescribes the value that <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle M}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>M</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle M}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f82cade9898ced02fdd08712e5f0c0151758a0dd" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.442ex; height:2.176ex;" alt="{\displaystyle M}"></span> must take in this case. Formally, the non-clausal resolution rule shown in line 57 above is applied to lines 12 and 1, with </p> <ul><li><style data-mw-deduplicate="TemplateStyles:r1239334494">@media screen{html.skin-theme-clientpref-night .mw-parser-output div:not(.notheme)>.tmp-color,html.skin-theme-clientpref-night .mw-parser-output p>.tmp-color,html.skin-theme-clientpref-night .mw-parser-output table:not(.notheme) .tmp-color{color:inherit!important}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output div:not(.notheme)>.tmp-color,html.skin-theme-clientpref-os .mw-parser-output p>.tmp-color,html.skin-theme-clientpref-os .mw-parser-output table:not(.notheme) .tmp-color{color:inherit!important}}</style><span class="tmp-color" style="color:#008000"><span class="texhtml">p</span></span> being the common instance <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#008000"><span class="texhtml">x=x</span></span> of <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#408000"><span class="texhtml">A=A</span></span> and <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#008040"><span class="texhtml">x=M</span></span>, obtained by syntactically <a href="/wiki/Unification_(computer_science)#Syntactic_unification_of_first-order_terms" title="Unification (computer science)">unifying</a> the latter formulas,</li> <li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#800000"><span class="texhtml">F[</span></span><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#008000"><span class="texhtml">p</span></span><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#800000"><span class="texhtml">]</span></span> being <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#800000"><span class="texhtml"><i>true</i> ∧ </span></span><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#008000"><span class="texhtml">x=x</span></span>, obtained from <a href="/wiki/Substitution_(logic)#First-order_logic" title="Substitution (logic)">instantiated</a> line 1 (appropriately padded to make the context <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#800000"><span class="texhtml">F[⋅]</span></span> around <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#008000"><span class="texhtml">p</span></span> visible), and</li> <li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#000080"><span class="texhtml">G[</span></span><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#008000"><span class="texhtml">p</span></span><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#000080"><span class="texhtml">]</span></span> being <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#000080"><span class="texhtml">x ≤ x ∧ y ≤ x ∧ </span></span><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#008000"><span class="texhtml">x = x</span></span>, obtained from instantiated line 12,</li></ul> <p>yielding <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot (}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mo stretchy="false">(</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot (}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2d287b6e913229b094a8481a8838c415d3f0990b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:2.455ex; height:2.843ex;" alt="{\displaystyle \lnot (}"></span><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#800000"><span class="texhtml"><i>true</i> ∧ </span></span><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#008000"><span class="texhtml"><i>false</i></span></span><span class="texhtml">) ∧ (</span><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#000080"><span class="texhtml">x ≤ x ∧ y ≤ x ∧ </span></span><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239334494"><span class="tmp-color" style="color:#008000"><span class="texhtml"><i>true</i></span></span><span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle )}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle )}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/775c8f99fbc2db4ef20dd618a468f110bae7bd76" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:0.905ex; height:2.843ex;" alt="{\displaystyle )}"></span>, which simplifies to <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\leq x\land y\leq x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≤</mo> <mi>x</mi> <mo>∧</mo> <mi>y</mi> <mo>≤</mo> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\leq x\land y\leq x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/015d21c14b713c625911019c000cc3a8f139bc72" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:13.924ex; height:2.343ex;" alt="{\displaystyle x\leq x\land y\leq x}"></span>. </p><p>In a similar way, line 14 yields line 15 and then line 16 by resolution. Also, the second case, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\leq M\land y\leq M\land y=M}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mi>y</mi> <mo>≤</mo> <mi>M</mi> <mo>∧</mo> <mi>y</mi> <mo>=</mo> <mi>M</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\leq M\land y\leq M\land y=M}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1396ea8e2e7187cf3d4b24449f2c904be6e66283" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:25.428ex; height:2.509ex;" alt="{\displaystyle x\leq M\land y\leq M\land y=M}"></span> in line 13, is handled similarly, yielding eventually line 18. </p><p>In a last step, both cases (i.e. lines 16 and 18) are joined, using the resolution rule from line 58; to make that rule applicable, the preparatory step 15→16 was needed. Intuitively, line 18 could be read as "in case <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x\leq y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>≤</mo> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x\leq y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c07a0bc023490be1c08e6c33a9cdc93bec908224" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.584ex; height:2.343ex;" alt="{\displaystyle x\leq y}"></span>, the output <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b8a6208ec717213d4317e666f1ae872e00620a0d" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.155ex; height:2.009ex;" alt="{\displaystyle y}"></span> is valid (with respect to the original specification), while line 15 says "in case <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle y\leq x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>y</mi> <mo>≤</mo> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle y\leq x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/7de6a6e4f44d9dfcbfaadbdcf388d4b8a6fed109" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.584ex; height:2.343ex;" alt="{\displaystyle y\leq x}"></span>, the output <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/87f9e315fd7e2ba406057a97300593c4802b53e4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}"></span> is valid; the step 15→16 established that both cases 16 and 18 are complementary.<sup id="cite_ref-31" class="reference"><a href="#cite_note-31"><span class="cite-bracket">[</span>note 5<span class="cite-bracket">]</span></a></sup> Since both line 16 and 18 comes with a program term, a <a href="/wiki/%3F:" class="mw-redirect" title="?:">conditional expression</a> results in the program column. Since the goal formula <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\textit {true}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mtext class="MJX-tex-mathit" mathvariant="italic">true</mtext> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\textit {true}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/39477b5045e93ab825d9d763e7f97e541f12851b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; margin-right: -0.023ex; width:4.095ex; height:2.009ex;" alt="{\displaystyle {\textit {true}}}"></span> has been derived, the proof is done, and the program column of the "<span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\textit {true}}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mrow class="MJX-TeXAtom-ORD"> <mrow class="MJX-TeXAtom-ORD"> <mtext class="MJX-tex-mathit" mathvariant="italic">true</mtext> </mrow> </mrow> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle {\textit {true}}}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/39477b5045e93ab825d9d763e7f97e541f12851b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; margin-right: -0.023ex; width:4.095ex; height:2.009ex;" alt="{\displaystyle {\textit {true}}}"></span>" line contains the program. </p> <div class="mw-heading mw-heading2"><h2 id="See_also">See also</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Program_synthesis&action=edit&section=8" title="Edit section: See also"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><a href="/wiki/Inductive_programming" title="Inductive programming">Inductive programming</a></li> <li><a href="/wiki/Metaprogramming" title="Metaprogramming">Metaprogramming</a></li> <li><a href="/wiki/Program_derivation" title="Program derivation">Program derivation</a></li> <li><a href="/wiki/Natural_language_programming" class="mw-redirect" title="Natural language programming">Natural language programming</a></li> <li><a href="/wiki/Reactive_synthesis" title="Reactive synthesis">Reactive synthesis</a></li></ul> <div class="mw-heading mw-heading2"><h2 id="Notes">Notes</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Program_synthesis&action=edit&section=9" title="Edit section: Notes"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1239543626">.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}</style><div class="reflist"> <div class="mw-references-wrap"><ol class="references"> <li id="cite_note-14"><span class="mw-cite-backlink"><b><a href="#cite_ref-14">^</a></b></span> <span class="reference-text">The distinction "Assertions" / "Goals" is for convenience only; following the paradigm of <a href="/wiki/Proof_by_contradiction" title="Proof by contradiction">proof by contradiction</a>, a Goal <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"></span> is equivalent to an assertion <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot F}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d1be87d4b5b721f671dcfaba45472bea40ccd6c9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.291ex; height:2.176ex;" alt="{\displaystyle \lnot F}"></span>.</span> </li> <li id="cite_note-15"><span class="mw-cite-backlink"><b><a href="#cite_ref-15">^</a></b></span> <span class="reference-text">When <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle s}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>s</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle s}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/01d131dfd7673938b947072a13a9744fe997e632" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.09ex; height:1.676ex;" alt="{\displaystyle s}"></span> is the Goal formula and the Program term in a line, respectively, then in all cases where <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"></span> holds, <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle s}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>s</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle s}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/01d131dfd7673938b947072a13a9744fe997e632" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.09ex; height:1.676ex;" alt="{\displaystyle s}"></span> is a valid output of the program to be synthesized. This <a href="/wiki/Invariant_(computer_science)" class="mw-redirect" title="Invariant (computer science)">invariant</a> is maintained by all proof rules. An Assertion formula usually is not associated with a Program term.</span> </li> <li id="cite_note-18"><span class="mw-cite-backlink"><b><a href="#cite_ref-18">^</a></b></span> <span class="reference-text">Only the conditional operator (<a href="/wiki/%3F:" class="mw-redirect" title="?:">?:</a>) is supported from the beginning. However, arbitrary new operators and relations can be added by providing their properties as axioms. In the toy example below, only the properties of <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle =}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>=</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle =}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/505a4ceef454c69dffd23792c84b90f488543743" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.307ex; margin-bottom: -0.478ex; width:1.808ex; height:1.343ex;" alt="{\displaystyle =}"></span> and <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \leq }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>≤</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \leq }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/440568a09c3bfdf0e1278bfa79eb137c04e94035" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \leq }"></span> that are actually needed in the proof have been axiomatized, in line 1 to 3.</span> </li> <li id="cite_note-30"><span class="mw-cite-backlink"><b><a href="#cite_ref-30">^</a></b></span> <span class="reference-text">While ordinary Skolemization preserves satisfiability, reverse Skolemization, i.e. replacing universally quantified variables by functions, preserves validity.</span> </li> <li id="cite_note-31"><span class="mw-cite-backlink"><b><a href="#cite_ref-31">^</a></b></span> <span class="reference-text">Axiom 3 was needed for that; in fact, if <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \leq }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo>≤</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \leq }</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/440568a09c3bfdf0e1278bfa79eb137c04e94035" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \leq }"></span> wasn't a <a href="/wiki/Total_order" title="Total order">total order</a>, no maximum could be computed for uncomparable inputs <span class="mwe-math-element"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x,y}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> <mo>,</mo> <mi>y</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x,y}</annotation> </semantics> </math></span><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/5ea0abffd33a692ded22accc104515a032851dff" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.519ex; height:2.009ex;" alt="{\displaystyle x,y}"></span>.</span> </li> </ol></div></div> <div class="mw-heading mw-heading2"><h2 id="References">References</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Program_synthesis&action=edit&section=10" title="Edit section: References"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239543626"><div class="reflist"> <div class="mw-references-wrap mw-references-columns"><ol class="references"> <li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text"><style data-mw-deduplicate="TemplateStyles:r1238218222">.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("//upload.wikimedia.org/wikipedia/commons/6/65/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("//upload.wikimedia.org/wikipedia/commons/d/d6/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("//upload.wikimedia.org/wikipedia/commons/a/aa/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("//upload.wikimedia.org/wikipedia/commons/4/4c/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}</style><cite id="CITEREFBasinDevilleFlenerHamfelt2004" class="citation book cs1">Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Fischer Nilsson, J. (2004). "Synthesis of programs in computational logic". In M. Bruynooghe and K.-K. Lau (ed.). <i>Program Development in Computational Logic</i>. LNCS. Vol. 3049. Springer. pp. <span class="nowrap">30–</span>65. <a href="/wiki/CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.4976">10.1.1.62.4976</a></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=bookitem&rft.atitle=Synthesis+of+programs+in+computational+logic&rft.btitle=Program+Development+in+Computational+Logic&rft.series=LNCS&rft.pages=%3Cspan+class%3D%22nowrap%22%3E30-%3C%2Fspan%3E65&rft.pub=Springer&rft.date=2004&rft_id=https%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fsummary%3Fdoi%3D10.1.1.62.4976%23id-name%3DCiteSeerX&rft.aulast=Basin&rft.aufirst=D.&rft.au=Deville%2C+Y.&rft.au=Flener%2C+P.&rft.au=Hamfelt%2C+A.&rft.au=Fischer+Nilsson%2C+J.&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text">(<a href="#CITEREFAlurSinghFisman">Alur, Singh & Fisman</a>)<span class="error harv-error" style="display: none; font-size:100%"> harv error: no target: CITEREFAlurSinghFisman (<a href="/wiki/Category:Harv_and_Sfn_template_errors" title="Category:Harv and Sfn template errors">help</a>)</span></span> </li> <li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFAlonzo_Church1957" class="citation journal cs1">Alonzo Church (1957). "Applications of recursive arithmetic to the problem of circuit synthesis". <i>Summaries of the Summer Institute of Symbolic Logic</i>. <b>1</b>: <span class="nowrap">3–</span>50.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Summaries+of+the+Summer+Institute+of+Symbolic+Logic&rft.atitle=Applications+of+recursive+arithmetic+to+the+problem+of+circuit+synthesis&rft.volume=1&rft.pages=%3Cspan+class%3D%22nowrap%22%3E3-%3C%2Fspan%3E50&rft.date=1957&rft.au=Alonzo+Church&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFRichard_Büchi,_Lawrence_Landweber1969" class="citation journal cs1">Richard Büchi, Lawrence Landweber (Apr 1969). <a rel="nofollow" class="external text" href="http://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=1087&context=cstech">"Solving Sequential Conditions by Finite-State Strategies"</a>. <i>Transactions of the American Mathematical Society</i>. <b>138</b>: <span class="nowrap">295–</span>311. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.2307%2F1994916">10.2307/1994916</a>. <a href="/wiki/JSTOR_(identifier)" class="mw-redirect" title="JSTOR (identifier)">JSTOR</a> <a rel="nofollow" class="external text" href="https://www.jstor.org/stable/1994916">1994916</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Transactions+of+the+American+Mathematical+Society&rft.atitle=Solving+Sequential+Conditions+by+Finite-State+Strategies&rft.volume=138&rft.pages=%3Cspan+class%3D%22nowrap%22%3E295-%3C%2Fspan%3E311&rft.date=1969-04&rft_id=info%3Adoi%2F10.2307%2F1994916&rft_id=https%3A%2F%2Fwww.jstor.org%2Fstable%2F1994916%23id-name%3DJSTOR&rft.au=Richard+B%C3%BCchi%2C+Lawrence+Landweber&rft_id=http%3A%2F%2Fdocs.lib.purdue.edu%2Fcgi%2Fviewcontent.cgi%3Farticle%3D1087%26context%3Dcstech&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-5">^</a></b></span> <span class="reference-text">(<a href="#CITEREFSolar-Lezama">Solar-Lezama</a>)<span class="error harv-error" style="display: none; font-size:100%"> harv error: no target: CITEREFSolar-Lezama (<a href="/wiki/Category:Harv_and_Sfn_template_errors" title="Category:Harv and Sfn template errors">help</a>)</span></span> </li> <li id="cite_note-6"><span class="mw-cite-backlink"><b><a href="#cite_ref-6">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFAlural.2013" class="citation conference cs1">Alur, Rajeev; al., et (2013). "Syntax-guided Synthesis". <i>Proceedings of Formal Methods in Computer-Aided Design</i>. IEEE. p. 8.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=conference&rft.atitle=Syntax-guided+Synthesis&rft.btitle=Proceedings+of+Formal+Methods+in+Computer-Aided+Design&rft.pages=8&rft.pub=IEEE&rft.date=2013&rft.aulast=Alur&rft.aufirst=Rajeev&rft.au=al.%2C+et&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-7"><span class="mw-cite-backlink"><b><a href="#cite_ref-7">^</a></b></span> <span class="reference-text">(<a href="#CITEREFDavidKroening">David & Kroening</a>)<span class="error harv-error" style="display: none; font-size:100%"> harv error: no target: CITEREFDavidKroening (<a href="/wiki/Category:Harv_and_Sfn_template_errors" title="Category:Harv and Sfn template errors">help</a>)</span></span> </li> <li id="cite_note-8"><span class="mw-cite-backlink"><b><a href="#cite_ref-8">^</a></b></span> <span class="reference-text"><a rel="nofollow" class="external text" href="https://sygus-org.github.io/comp/">SyGuS-Comp (Syntax-Guided Synthesis Competition)</a></span> </li> <li id="cite_note-9"><span class="mw-cite-backlink"><b><a href="#cite_ref-9">^</a></b></span> <span class="reference-text">(<a href="#CITEREFSolar-Lezama">Solar-Lezama</a>)<span class="error harv-error" style="display: none; font-size:100%"> harv error: no target: CITEREFSolar-Lezama (<a href="/wiki/Category:Harv_and_Sfn_template_errors" title="Category:Harv and Sfn template errors">help</a>)</span></span> </li> <li id="cite_note-10"><span class="mw-cite-backlink"><b><a href="#cite_ref-10">^</a></b></span> <span class="reference-text">(<a href="#CITEREFDavidKroening">David & Kroening</a>)<span class="error harv-error" style="display: none; font-size:100%"> harv error: no target: CITEREFDavidKroening (<a href="/wiki/Category:Harv_and_Sfn_template_errors" title="Category:Harv and Sfn template errors">help</a>)</span></span> </li> <li id="cite_note-11"><span class="mw-cite-backlink"><b><a href="#cite_ref-11">^</a></b></span> <span class="reference-text">(<a href="#CITEREFSolar-Lezama">Solar-Lezama</a>)<span class="error harv-error" style="display: none; font-size:100%"> harv error: no target: CITEREFSolar-Lezama (<a href="/wiki/Category:Harv_and_Sfn_template_errors" title="Category:Harv and Sfn template errors">help</a>)</span></span> </li> <li id="cite_note-12"><span class="mw-cite-backlink"><b><a href="#cite_ref-12">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFZohar_Manna,_Richard_Waldinger1980" class="citation journal cs1">Zohar Manna, Richard Waldinger (Jan 1980). "A Deductive Approach to Program Synthesis". <i>ACM Transactions on Programming Languages and Systems</i>. <b>2</b>: <span class="nowrap">90–</span>121. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F357084.357090">10.1145/357084.357090</a>. <a href="/wiki/S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:14770735">14770735</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=ACM+Transactions+on+Programming+Languages+and+Systems&rft.atitle=A+Deductive+Approach+to+Program+Synthesis&rft.volume=2&rft.pages=%3Cspan+class%3D%22nowrap%22%3E90-%3C%2Fspan%3E121&rft.date=1980-01&rft_id=info%3Adoi%2F10.1145%2F357084.357090&rft_id=https%3A%2F%2Fapi.semanticscholar.org%2FCorpusID%3A14770735%23id-name%3DS2CID&rft.au=Zohar+Manna%2C+Richard+Waldinger&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-13"><span class="mw-cite-backlink"><b><a href="#cite_ref-13">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFZohar_Manna_and_Richard_Waldinger1978" class="citation report cs1">Zohar Manna and Richard Waldinger (Dec 1978). <a rel="nofollow" class="external text" href="https://apps.dtic.mil/dtic/tr/fulltext/u2/a065558.pdf">A Deductive Approach to Program Synthesis</a> <span class="cs1-format">(PDF)</span> (Technical Note). SRI International. <a rel="nofollow" class="external text" href="https://web.archive.org/web/20210127052044/https://apps.dtic.mil/dtic/tr/fulltext/u2/a065558.pdf">Archived</a> <span class="cs1-format">(PDF)</span> from the original on January 27, 2021.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=report&rft.btitle=A+Deductive+Approach+to+Program+Synthesis&rft.pub=SRI+International&rft.date=1978-12&rft.au=Zohar+Manna+and+Richard+Waldinger&rft_id=https%3A%2F%2Fapps.dtic.mil%2Fdtic%2Ftr%2Ffulltext%2Fu2%2Fa065558.pdf&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-16"><span class="mw-cite-backlink"><b><a href="#cite_ref-16">^</a></b></span> <span class="reference-text">See Manna, Waldinger (1980), p.100 for correctness of the resolution rules.</span> </li> <li id="cite_note-17"><span class="mw-cite-backlink"><b><a href="#cite_ref-17">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFBoyerMoore1983" class="citation techreport cs1">Boyer, Robert S.; Moore, J. Strother (May 1983). <a rel="nofollow" class="external text" href="http://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp37.pdf"><i>A Mechanical Proof of the Turing Completeness of Pure Lisp</i></a> <span class="cs1-format">(PDF)</span> (Technical report). Institute for Computing Science, University of Texas at Austin. 37. <a rel="nofollow" class="external text" href="https://web.archive.org/web/20170922044624/http://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp37.pdf">Archived</a> <span class="cs1-format">(PDF)</span> from the original on 22 September 2017.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=report&rft.btitle=A+Mechanical+Proof+of+the+Turing+Completeness+of+Pure+Lisp&rft.pub=Institute+for+Computing+Science%2C+University+of+Texas+at+Austin&rft.date=1983-05&rft.aulast=Boyer&rft.aufirst=Robert+S.&rft.au=Moore%2C+J.+Strother&rft_id=http%3A%2F%2Fwww.cs.utexas.edu%2Fusers%2Fboyer%2Fftp%2Fics-reports%2Fcmp37.pdf&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-19"><span class="mw-cite-backlink"><b><a href="#cite_ref-19">^</a></b></span> <span class="reference-text">Manna, Waldinger (1980), p.108-111</span> </li> <li id="cite_note-20"><span class="mw-cite-backlink"><b><a href="#cite_ref-20">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFZohar_Manna_and_Richard_Waldinger1987" class="citation journal cs1">Zohar Manna and Richard Waldinger (Aug 1987). "The Origin of a Binary-Search Paradigm". <i>Science of Computer Programming</i>. <b>9</b> (1): <span class="nowrap">37–</span>83. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2F0167-6423%2887%2990025-6">10.1016/0167-6423(87)90025-6</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Science+of+Computer+Programming&rft.atitle=The+Origin+of+a+Binary-Search+Paradigm&rft.volume=9&rft.issue=1&rft.pages=%3Cspan+class%3D%22nowrap%22%3E37-%3C%2Fspan%3E83&rft.date=1987-08&rft_id=info%3Adoi%2F10.1016%2F0167-6423%2887%2990025-6&rft.au=Zohar+Manna+and+Richard+Waldinger&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-21"><span class="mw-cite-backlink"><b><a href="#cite_ref-21">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFDaniele_Nardi1989" class="citation journal cs1">Daniele Nardi (1989). "Formal Synthesis of a Unification Algorithm by the Deductive-Tableau Method". <i><a href="/wiki/Journal_of_Logic_Programming" class="mw-redirect" title="Journal of Logic Programming">Journal of Logic Programming</a></i>. <b>7</b>: <span class="nowrap">1–</span>43. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2F0743-1066%2889%2990008-3">10.1016/0743-1066(89)90008-3</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Journal+of+Logic+Programming&rft.atitle=Formal+Synthesis+of+a+Unification+Algorithm+by+the+Deductive-Tableau+Method&rft.volume=7&rft.pages=%3Cspan+class%3D%22nowrap%22%3E1-%3C%2Fspan%3E43&rft.date=1989&rft_id=info%3Adoi%2F10.1016%2F0743-1066%2889%2990008-3&rft.au=Daniele+Nardi&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-22"><span class="mw-cite-backlink"><b><a href="#cite_ref-22">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFDaniele_Nardi_and_Riccardo_Rosati1992" class="citation book cs1">Daniele Nardi and Riccardo Rosati (1992). "Deductive Synthesis of Programs for Query Answering". In Kung-Kiu Lau and Tim Clement (ed.). <i>International Workshop on Logic Program Synthesis and Transformation (LOPSTR)</i>. Workshops in Computing. Springer. pp. <span class="nowrap">15–</span>29. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-1-4471-3560-9_2">10.1007/978-1-4471-3560-9_2</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=bookitem&rft.atitle=Deductive+Synthesis+of+Programs+for+Query+Answering&rft.btitle=International+Workshop+on+Logic+Program+Synthesis+and+Transformation+%28LOPSTR%29&rft.series=Workshops+in+Computing&rft.pages=%3Cspan+class%3D%22nowrap%22%3E15-%3C%2Fspan%3E29&rft.pub=Springer&rft.date=1992&rft_id=info%3Adoi%2F10.1007%2F978-1-4471-3560-9_2&rft.au=Daniele+Nardi+and+Riccardo+Rosati&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-23"><span class="mw-cite-backlink"><b><a href="#cite_ref-23">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFJonathan_Traugott1986" class="citation book cs1">Jonathan Traugott (1986). "Deductive Synthesis of Sorting Programs". <i>Proceedings of the International Conference on Automated Deduction</i>. <a href="/wiki/LNCS" class="mw-redirect" title="LNCS">LNCS</a>. Vol. 230. Springer. pp. <span class="nowrap">641–</span>660.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=bookitem&rft.atitle=Deductive+Synthesis+of+Sorting+Programs&rft.btitle=Proceedings+of+the+International+Conference+on+Automated+Deduction&rft.series=LNCS&rft.pages=%3Cspan+class%3D%22nowrap%22%3E641-%3C%2Fspan%3E660&rft.pub=Springer&rft.date=1986&rft.au=Jonathan+Traugott&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-24"><span class="mw-cite-backlink"><b><a href="#cite_ref-24">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFJonathan_Traugott1989" class="citation journal cs1">Jonathan Traugott (Jun 1989). "Deductive Synthesis of Sorting Programs". <i><a href="/wiki/Journal_of_Symbolic_Computation" title="Journal of Symbolic Computation">Journal of Symbolic Computation</a></i>. <b>7</b> (6): <span class="nowrap">533–</span>572. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2FS0747-7171%2889%2980040-9">10.1016/S0747-7171(89)80040-9</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Journal+of+Symbolic+Computation&rft.atitle=Deductive+Synthesis+of+Sorting+Programs&rft.volume=7&rft.issue=6&rft.pages=%3Cspan+class%3D%22nowrap%22%3E533-%3C%2Fspan%3E572&rft.date=1989-06&rft_id=info%3Adoi%2F10.1016%2FS0747-7171%2889%2980040-9&rft.au=Jonathan+Traugott&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-25"><span class="mw-cite-backlink"><b><a href="#cite_ref-25">^</a></b></span> <span class="reference-text">Manna, Waldinger (1980), p.99</span> </li> <li id="cite_note-26"><span class="mw-cite-backlink"><b><a href="#cite_ref-26">^</a></b></span> <span class="reference-text">Manna, Waldinger (1980), p.104</span> </li> <li id="cite_note-27"><span class="mw-cite-backlink"><b><a href="#cite_ref-27">^</a></b></span> <span class="reference-text">Manna, Waldinger (1980), p.103, referring to: <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFNeil_V._Murray1979" class="citation techreport cs1">Neil V. Murray (Feb 1979). <a rel="nofollow" class="external text" href="http://surface.syr.edu/cgi/viewcontent.cgi?article=1005&context=eecs_techreports"><i>A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic</i></a> (Technical report). Syracuse Univ. 2-79.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=report&rft.btitle=A+Proof+Procedure+for+Quantifier-Free+Non-Clausal+First+Order+Logic&rft.pub=Syracuse+Univ.&rft.date=1979-02&rft.au=Neil+V.+Murray&rft_id=http%3A%2F%2Fsurface.syr.edu%2Fcgi%2Fviewcontent.cgi%3Farticle%3D1005%26context%3Deecs_techreports&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-28"><span class="mw-cite-backlink"><b><a href="#cite_ref-28">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFZohar_Manna,_Richard_Waldinger1986" class="citation journal cs1">Zohar Manna, Richard Waldinger (Jan 1986). <a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F4904.4905">"Special Relations in Automated Deduction"</a>. <i>Journal of the ACM</i>. <b>33</b>: <span class="nowrap">1–</span>59. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F4904.4905">10.1145/4904.4905</a></span>. <a href="/wiki/S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:15140138">15140138</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Journal+of+the+ACM&rft.atitle=Special+Relations+in+Automated+Deduction&rft.volume=33&rft.pages=%3Cspan+class%3D%22nowrap%22%3E1-%3C%2Fspan%3E59&rft.date=1986-01&rft_id=info%3Adoi%2F10.1145%2F4904.4905&rft_id=https%3A%2F%2Fapi.semanticscholar.org%2FCorpusID%3A15140138%23id-name%3DS2CID&rft.au=Zohar+Manna%2C+Richard+Waldinger&rft_id=https%3A%2F%2Fdoi.org%2F10.1145%252F4904.4905&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> <li id="cite_note-29"><span class="mw-cite-backlink"><b><a href="#cite_ref-29">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFZohar_Manna,_Richard_Waldinger1992" class="citation book cs1">Zohar Manna, Richard Waldinger (1992). "The Special-Relations Rules are Incomplete". <i>Proc. CADE 11</i>. LNCS. Vol. 607. Springer. pp. <span class="nowrap">492–</span>506.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=bookitem&rft.atitle=The+Special-Relations+Rules+are+Incomplete&rft.btitle=Proc.+CADE+11&rft.series=LNCS&rft.pages=%3Cspan+class%3D%22nowrap%22%3E492-%3C%2Fspan%3E506&rft.pub=Springer&rft.date=1992&rft.au=Zohar+Manna%2C+Richard+Waldinger&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></span> </li> </ol></div></div> <ul><li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFDavidKroening2017" class="citation journal cs1">David, Cristina; Kroening, Daniel (2017-10-13). <a rel="nofollow" class="external text" href="https://royalsocietypublishing.org/doi/10.1098/rsta.2015.0403">"Program synthesis: challenges and opportunities"</a>. <i>Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. <b>375</b> (2104): 20150403. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1098%2Frsta.2015.0403">10.1098/rsta.2015.0403</a>. <a href="/wiki/ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/1364-503X">1364-503X</a>. <a href="/wiki/PMC_(identifier)" class="mw-redirect" title="PMC (identifier)">PMC</a> <span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597726">5597726</a></span>. <a href="/wiki/PMID_(identifier)" class="mw-redirect" title="PMID (identifier)">PMID</a> <a rel="nofollow" class="external text" href="https://pubmed.ncbi.nlm.nih.gov/28871052">28871052</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Philosophical+Transactions+of+the+Royal+Society+A%3A+Mathematical%2C+Physical+and+Engineering+Sciences&rft.atitle=Program+synthesis%3A+challenges+and+opportunities&rft.volume=375&rft.issue=2104&rft.pages=20150403&rft.date=2017-10-13&rft_id=https%3A%2F%2Fwww.ncbi.nlm.nih.gov%2Fpmc%2Farticles%2FPMC5597726%23id-name%3DPMC&rft.issn=1364-503X&rft_id=info%3Apmid%2F28871052&rft_id=info%3Adoi%2F10.1098%2Frsta.2015.0403&rft.aulast=David&rft.aufirst=Cristina&rft.au=Kroening%2C+Daniel&rft_id=https%3A%2F%2Froyalsocietypublishing.org%2Fdoi%2F10.1098%2Frsta.2015.0403&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></li> <li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFAlurSinghFismanSolar-Lezama2018" class="citation journal cs1">Alur, Rajeev; Singh, Rishabh; Fisman, Dana; Solar-Lezama, Armando (2018-11-20). <a rel="nofollow" class="external text" href="https://doi.org/10.1145/3208071">"Search-based program synthesis"</a>. <i>Communications of the ACM</i>. <b>61</b> (12): <span class="nowrap">84–</span>93. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F3208071">10.1145/3208071</a>. <a href="/wiki/ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/0001-0782">0001-0782</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Communications+of+the+ACM&rft.atitle=Search-based+program+synthesis&rft.volume=61&rft.issue=12&rft.pages=%3Cspan+class%3D%22nowrap%22%3E84-%3C%2Fspan%3E93&rft.date=2018-11-20&rft_id=info%3Adoi%2F10.1145%2F3208071&rft.issn=0001-0782&rft.aulast=Alur&rft.aufirst=Rajeev&rft.au=Singh%2C+Rishabh&rft.au=Fisman%2C+Dana&rft.au=Solar-Lezama%2C+Armando&rft_id=https%3A%2F%2Fdoi.org%2F10.1145%2F3208071&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></li> <li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFZohar_Manna,_Richard_Waldinger1975" class="citation journal cs1">Zohar Manna, Richard Waldinger (1975). "Knowledge and Reasoning in Program Synthesis". <i>Artificial Intelligence</i>. <b>6</b> (2): <span class="nowrap">175–</span>208. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2F0004-3702%2875%2990008-9">10.1016/0004-3702(75)90008-9</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Artificial+Intelligence&rft.atitle=Knowledge+and+Reasoning+in+Program+Synthesis&rft.volume=6&rft.issue=2&rft.pages=%3Cspan+class%3D%22nowrap%22%3E175-%3C%2Fspan%3E208&rft.date=1975&rft_id=info%3Adoi%2F10.1016%2F0004-3702%2875%2990008-9&rft.au=Zohar+Manna%2C+Richard+Waldinger&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></li> <li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFSolar-Lezama2008" class="citation thesis cs1">Solar-Lezama, Armando (2008). <a rel="nofollow" class="external text" href="https://people.csail.mit.edu/asolar/papers/thesis.pdf"><i>Program synthesis by sketching</i></a> <span class="cs1-format">(PDF)</span> (Ph.D.). University of California, Berkeley.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adissertation&rft.title=Program+synthesis+by+sketching&rft.inst=University+of+California%2C+Berkeley&rft.date=2008&rft.aulast=Solar-Lezama&rft.aufirst=Armando&rft_id=https%3A%2F%2Fpeople.csail.mit.edu%2Fasolar%2Fpapers%2Fthesis.pdf&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProgram+synthesis" class="Z3988"></span></li></ul>    </div><noscript><img src="https://login.wikimedia.org/wiki/Special:CentralAutoLogin/start?useformat=desktop&type=1x1&usesul3=0" alt="" width="1" height="1" style="border: none; position: absolute;"></noscript> <div class="printfooter" data-nosnippet="">Retrieved from "<a dir="ltr" href="https://en.wikipedia.org/w/index.php?title=Program_synthesis&oldid=1241784157">https://en.wikipedia.org/w/index.php?title=Program_synthesis&oldid=1241784157</a>"</div></div> <div id="catlinks" class="catlinks" data-mw="interface"><div id="mw-normal-catlinks" class="mw-normal-catlinks"><a href="/wiki/Help:Category" title="Help:Category">Category</a>: <ul><li><a href="/wiki/Category:Programming_paradigms" title="Category:Programming paradigms">Programming paradigms</a></li></ul></div><div id="mw-hidden-catlinks" class="mw-hidden-catlinks mw-hidden-cats-hidden">Hidden categories: <ul><li><a href="/wiki/Category:Harv_and_Sfn_no-target_errors" title="Category:Harv and Sfn no-target errors">Harv and Sfn no-target errors</a></li><li><a href="/wiki/Category:Articles_with_short_description" title="Category:Articles with short description">Articles with short description</a></li><li><a href="/wiki/Category:Short_description_is_different_from_Wikidata" title="Category:Short description is different from Wikidata">Short description is different from Wikidata</a></li><li><a href="/wiki/Category:All_articles_with_unsourced_statements" title="Category:All articles with unsourced statements">All articles with unsourced statements</a></li><li><a href="/wiki/Category:Articles_with_unsourced_statements_from_June_2010" title="Category:Articles with unsourced statements from June 2010">Articles with unsourced statements from June 2010</a></li><li><a href="/wiki/Category:Articles_to_be_expanded_from_December_2022" title="Category:Articles to be expanded from December 2022">Articles to be expanded from December 2022</a></li><li><a href="/wiki/Category:All_articles_to_be_expanded" title="Category:All articles to be expanded">All articles to be expanded</a></li><li><a href="/wiki/Category:Articles_with_unsourced_statements_from_May_2016" title="Category:Articles with unsourced statements from May 2016">Articles with unsourced statements from May 2016</a></li></ul></div></div> </div> </main> </div> <div class="mw-footer-container"> <footer id="footer" class="mw-footer" > <ul id="footer-info"> <li id="footer-info-lastmod"> This page was last edited on 23 August 2024, at 03:21<span class="anonymous-show"> (UTC)</span>.</li> <li id="footer-info-copyright">Text is available under the <a href="/wiki/Wikipedia:Text_of_the_Creative_Commons_Attribution-ShareAlike_4.0_International_License" title="Wikipedia:Text of the Creative Commons Attribution-ShareAlike 4.0 International License">Creative Commons Attribution-ShareAlike 4.0 License</a>; additional terms may apply. By using this site, you agree to the <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Terms_of_Use" class="extiw" title="foundation:Special:MyLanguage/Policy:Terms of Use">Terms of Use</a> and <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy" class="extiw" title="foundation:Special:MyLanguage/Policy:Privacy policy">Privacy Policy</a>. Wikipedia® is a registered trademark of the <a rel="nofollow" class="external text" href="https://wikimediafoundation.org/">Wikimedia Foundation, Inc.</a>, a non-profit organization.</li> </ul> <ul id="footer-places"> <li id="footer-places-privacy"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy">Privacy policy</a></li> <li id="footer-places-about"><a href="/wiki/Wikipedia:About">About Wikipedia</a></li> <li id="footer-places-disclaimers"><a href="/wiki/Wikipedia:General_disclaimer">Disclaimers</a></li> <li id="footer-places-contact"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us">Contact Wikipedia</a></li> <li id="footer-places-wm-codeofconduct"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Universal_Code_of_Conduct">Code of Conduct</a></li> <li id="footer-places-developers"><a href="https://developer.wikimedia.org">Developers</a></li> <li id="footer-places-statslink"><a href="https://stats.wikimedia.org/#/en.wikipedia.org">Statistics</a></li> <li id="footer-places-cookiestatement"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Cookie_statement">Cookie statement</a></li> <li id="footer-places-mobileview"><a href="//en.m.wikipedia.org/w/index.php?title=Program_synthesis&mobileaction=toggle_view_mobile" class="noprint stopMobileRedirectToggle">Mobile view</a></li> </ul> <ul id="footer-icons" class="noprint"> <li id="footer-copyrightico"><a href="https://wikimediafoundation.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/static/images/footer/wikimedia-button.svg" width="84" height="29" alt="Wikimedia Foundation" lang="en" loading="lazy"></a></li> <li id="footer-poweredbyico"><a href="https://www.mediawiki.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><picture><source media="(min-width: 500px)" srcset="/w/resources/assets/poweredby_mediawiki.svg" width="88" height="31"><img src="/w/resources/assets/mediawiki_compact.svg" alt="Powered by MediaWiki" width="25" height="25" loading="lazy"></picture></a></li> </ul> </footer> </div> </div> </div> <div class="vector-header-container vector-sticky-header-container"> <div id="vector-sticky-header" class="vector-sticky-header"> <div class="vector-sticky-header-start"> <div class="vector-sticky-header-icon-start vector-button-flush-left vector-button-flush-right" aria-hidden="true"> <button class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-sticky-header-search-toggle" tabindex="-1" data-event-name="ui.vector-sticky-search-form.icon"><span class="vector-icon mw-ui-icon-search mw-ui-icon-wikimedia-search"></span> <span>Search</span> </button> </div> <div role="search" class="vector-search-box-vue vector-search-box-show-thumbnail vector-search-box"> <div class="vector-typeahead-search-container"> <div class="cdx-typeahead-search cdx-typeahead-search--show-thumbnail"> <form action="/w/index.php" id="vector-sticky-search-form" class="cdx-search-input cdx-search-input--has-end-button"> <div class="cdx-search-input__input-wrapper" data-search-loc="header-moved"> <div class="cdx-text-input cdx-text-input--has-start-icon"> <input class="cdx-text-input__input" type="search" name="search" placeholder="Search Wikipedia"> <span class="cdx-text-input__icon cdx-text-input__start-icon"></span> </div> <input type="hidden" name="title" value="Special:Search"> </div> <button class="cdx-button cdx-search-input__end-button">Search</button> </form> </div> </div> </div> <div class="vector-sticky-header-context-bar"> <nav aria-label="Contents" class="vector-toc-landmark"> <div id="vector-sticky-header-toc" class="vector-dropdown mw-portlet mw-portlet-sticky-header-toc vector-sticky-header-toc vector-button-flush-left" > <input type="checkbox" id="vector-sticky-header-toc-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-sticky-header-toc" class="vector-dropdown-checkbox " aria-label="Toggle the table of contents" > <label id="vector-sticky-header-toc-label" for="vector-sticky-header-toc-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-listBullet mw-ui-icon-wikimedia-listBullet"></span> <span class="vector-dropdown-label-text">Toggle the table of contents</span> </label> <div class="vector-dropdown-content"> <div id="vector-sticky-header-toc-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <div class="vector-sticky-header-context-bar-primary" aria-hidden="true" ><span class="mw-page-title-main">Program synthesis</span></div> </div> </div> <div class="vector-sticky-header-end" aria-hidden="true"> <div class="vector-sticky-header-icons"> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only" id="ca-talk-sticky-header" tabindex="-1" data-event-name="talk-sticky-header"><span class="vector-icon mw-ui-icon-speechBubbles mw-ui-icon-wikimedia-speechBubbles"></span> <span></span> </a> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only" id="ca-subject-sticky-header" tabindex="-1" data-event-name="subject-sticky-header"><span class="vector-icon mw-ui-icon-article mw-ui-icon-wikimedia-article"></span> <span></span> </a> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only" id="ca-history-sticky-header" tabindex="-1" data-event-name="history-sticky-header"><span class="vector-icon mw-ui-icon-wikimedia-history mw-ui-icon-wikimedia-wikimedia-history"></span> <span></span> </a> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only mw-watchlink" id="ca-watchstar-sticky-header" tabindex="-1" data-event-name="watch-sticky-header"><span class="vector-icon mw-ui-icon-wikimedia-star mw-ui-icon-wikimedia-wikimedia-star"></span> <span></span> </a> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only" id="ca-edit-sticky-header" tabindex="-1" data-event-name="wikitext-edit-sticky-header"><span class="vector-icon mw-ui-icon-wikimedia-wikiText mw-ui-icon-wikimedia-wikimedia-wikiText"></span> <span></span> </a> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only" id="ca-ve-edit-sticky-header" tabindex="-1" data-event-name="ve-edit-sticky-header"><span class="vector-icon mw-ui-icon-wikimedia-edit mw-ui-icon-wikimedia-wikimedia-edit"></span> <span></span> </a> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only" id="ca-viewsource-sticky-header" tabindex="-1" data-event-name="ve-edit-protected-sticky-header"><span class="vector-icon mw-ui-icon-wikimedia-editLock mw-ui-icon-wikimedia-wikimedia-editLock"></span> <span></span> </a> </div> <div class="vector-sticky-header-buttons"> <button class="cdx-button cdx-button--weight-quiet mw-interlanguage-selector" id="p-lang-btn-sticky-header" tabindex="-1" data-event-name="ui.dropdown-p-lang-btn-sticky-header"><span class="vector-icon mw-ui-icon-wikimedia-language mw-ui-icon-wikimedia-wikimedia-language"></span> <span>4 languages</span> </button> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--action-progressive" id="ca-addsection-sticky-header" tabindex="-1" data-event-name="addsection-sticky-header"><span class="vector-icon mw-ui-icon-speechBubbleAdd-progressive mw-ui-icon-wikimedia-speechBubbleAdd-progressive"></span> <span>Add topic</span> </a> </div> <div class="vector-sticky-header-icon-end"> <div class="vector-user-links"> </div> </div> </div> </div> </div> <div class="vector-settings" id="p-dock-bottom"> <ul></ul> </div><script>(RLQ=window.RLQ||[]).push(function(){mw.config.set({"wgHostname":"mw-web.codfw.main-b766959bd-z7tt6","wgBackendResponseTime":123,"wgPageParseReport":{"limitreport":{"cputime":"0.466","walltime":"0.694","ppvisitednodes":{"value":4235,"limit":1000000},"postexpandincludesize":{"value":60406,"limit":2097152},"templateargumentsize":{"value":5919,"limit":2097152},"expansiondepth":{"value":12,"limit":100},"expensivefunctioncount":{"value":5,"limit":500},"unstrip-depth":{"value":1,"limit":20},"unstrip-size":{"value":90079,"limit":5000000},"entityaccesscount":{"value":0,"limit":400},"timingprofile":["100.00% 491.939 1 -total"," 43.23% 212.645 2 Template:Reflist"," 20.73% 101.969 4 Template:Cite_book"," 13.18% 64.833 1 Template:Short_description"," 10.37% 51.004 10 Template:Cite_journal"," 8.10% 39.865 2 Template:Pagetype"," 7.48% 36.815 2 Template:Citation_needed"," 6.78% 33.355 6 Template:Harv"," 6.32% 31.093 2 Template:Fix"," 6.28% 30.880 20 Template:Color"]},"scribunto":{"limitreport-timeusage":{"value":"0.227","limit":"10.000"},"limitreport-memusage":{"value":7566822,"limit":52428800},"limitreport-logs":"anchor_id_list = table#1 {\n [\"CITEREFAlonzo_Church1957\"] = 1,\n [\"CITEREFAlurSinghFismanSolar-Lezama2018\"] = 1,\n [\"CITEREFAlural.2013\"] = 1,\n [\"CITEREFBasinDevilleFlenerHamfelt2004\"] = 1,\n [\"CITEREFBoyerMoore1983\"] = 1,\n [\"CITEREFDaniele_Nardi1989\"] = 1,\n [\"CITEREFDaniele_Nardi_and_Riccardo_Rosati1992\"] = 1,\n [\"CITEREFDavidKroening2017\"] = 1,\n [\"CITEREFJonathan_Traugott1986\"] = 1,\n [\"CITEREFJonathan_Traugott1989\"] = 1,\n [\"CITEREFNeil_V._Murray1979\"] = 1,\n [\"CITEREFRichard_Büchi,_Lawrence_Landweber1969\"] = 1,\n [\"CITEREFSolar-Lezama2008\"] = 1,\n [\"CITEREFZohar_Manna,_Richard_Waldinger1975\"] = 1,\n [\"CITEREFZohar_Manna,_Richard_Waldinger1980\"] = 1,\n [\"CITEREFZohar_Manna,_Richard_Waldinger1986\"] = 1,\n [\"CITEREFZohar_Manna,_Richard_Waldinger1992\"] = 1,\n [\"CITEREFZohar_Manna_and_Richard_Waldinger1978\"] = 1,\n [\"CITEREFZohar_Manna_and_Richard_Waldinger1987\"] = 1,\n}\ntemplate_list = table#1 {\n [\"=\"] = 2,\n [\"Citation needed\"] = 2,\n [\"Cite book\"] = 4,\n [\"Cite conference\"] = 1,\n [\"Cite journal\"] = 10,\n [\"Cite report\"] = 1,\n [\"Cite tech report\"] = 2,\n [\"Cite thesis\"] = 1,\n [\"Clear\"] = 1,\n [\"Color\"] = 20,\n [\"DEFAULTSORT:Program Synthesis\"] = 1,\n [\"Expand section\"] = 1,\n [\"Harv\"] = 6,\n [\"Math\"] = 22,\n [\"Reflist\"] = 2,\n [\"Short description\"] = 1,\n [\"Sic\"] = 1,\n [\"Var\"] = 26,\n}\narticle_whitelist = table#1 {\n}\nciteref_patterns = table#1 {\n}\nno target: CITEREFAlurSinghFisman\nno target: CITEREFSolar-Lezama\nno target: CITEREFDavidKroening\nno target: CITEREFSolar-Lezama\nno target: CITEREFDavidKroening\nno target: CITEREFSolar-Lezama\n"},"cachereport":{"origin":"mw-web.codfw.main-b766959bd-dx6rg","timestamp":"20250214041210","ttl":2592000,"transientcontent":false}}});});</script> <script type="application/ld+json">{"@context":"https:\/\/schema.org","@type":"Article","name":"Program synthesis","url":"https:\/\/en.wikipedia.org\/wiki\/Program_synthesis","sameAs":"http:\/\/www.wikidata.org\/entity\/Q4117718","mainEntity":"http:\/\/www.wikidata.org\/entity\/Q4117718","author":{"@type":"Organization","name":"Contributors to Wikimedia projects"},"publisher":{"@type":"Organization","name":"Wikimedia Foundation, Inc.","logo":{"@type":"ImageObject","url":"https:\/\/www.wikimedia.org\/static\/images\/wmf-hor-googpub.png"}},"datePublished":"2004-03-02T01:25:37Z","dateModified":"2024-08-23T03:21:28Z","headline":"task to construct a program that provably satisfies a given high-level formal specification"}</script> </body> </html>