Editing Program synthesis (section)

===Proof rules===
Proof rules include:
*Non-clausal [[Resolution (logic)|resolution]] (see table).
:For example, line 55 is obtained by resolving Assertion formulas <math>E</math> from 51 and <math>F</math> from 52 which both share some common subformula <math>p</math>. The resolvent is formed as the disjunction of <math>E</math>, with <math>p</math> replaced by <math>\it true</math>, and <math>F</math>, with <math>p</math> replaced by <math>\it false</math>. This resolvent logically follows from the conjunction of <math>E</math> and <math>F</math>. More generally, <math>E</math> and <math>F</math> need to have only two unifiable subformulas <math>p_1</math> and <math>p_2</math>, respectively; their resolvent is then formed from <math>E \theta</math> and <math>F \theta</math> as before, where <math>\theta</math> is the [[most general unifier]] of <math>p_1</math> and <math>p_2</math>. This rule generalizes [[Resolution (logic)#Resolution in first order logic|resolution of clauses]].<ref>Manna, Waldinger (1980), p.99</ref>
:Program terms of parent formulas are combined as shown in line 58 to form the output of the resolvent. In the general case, <math>\theta</math> is applied to the latter also. Since the subformula <math>p</math> appears in the output, care must be taken to resolve only on subformulas corresponding to [[computable]] properties.
*Logical transformations.
:For example, <math>E \land (F \lor G)</math> can be transformed to <math>(E \land F) \lor (E \land G)</math>) in Assertions as well as in Goals, since both are equivalent.
*Splitting of conjunctive assertions and of disjunctive goals.
:An example is shown in lines 11 to 13 of the toy example below.
*[[Structural induction]].
:This rule allows for synthesis of [[recursive function (programming)|recursive functions]]. For a given pre- and postcondition "Given <math>x</math> such that <math>\textit{pre}(x)</math>, find <math>f(x) = y</math> such that <math>\textit{post}(x,y)</math>", and an appropriate user-given [[well-ordering]] <math>\prec</math> of the domain of <math>x</math>, it is always sound to add an Assertion "<math>x' \prec x \land \textit{pre}(x') \implies \textit{post}(x',f(x'))</math>".<ref>Manna, Waldinger (1980), p.104</ref> Resolving with this assertion can introduce a recursive call to <math>f</math> in the Program term.
: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 <math>(n',d') \prec (n,d)</math> defined by <math>0 \leq n' < n</math> (p.110).

Murray has shown these rules to be [[Completeness (logic)|complete]] for [[first-order logic]].<ref>Manna, Waldinger (1980), p.103, referring to: {{cite tech report| author=Neil V. Murray| title=A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic|date=Feb 1979| number=2-79| institution=Syracuse Univ.| url=http://surface.syr.edu/cgi/viewcontent.cgi?article=1005&context=eecs_techreports}}</ref>
In 1986, Manna and Waldinger added generalized E-resolution and [[paramodulation]] rules to handle also equality;<ref>{{cite journal| author=Zohar Manna, Richard Waldinger| title=Special Relations in Automated Deduction| journal=Journal of the ACM| volume=33|date=Jan 1986| pages=1–59|doi=10.1145/4904.4905 | s2cid=15140138| doi-access=free}}</ref> later, these rules turned out to be incomplete (but nevertheless [[soundness|sound]]).<ref>{{cite book| author=Zohar Manna, Richard Waldinger| chapter=The Special-Relations Rules are Incomplete| title=Proc. CADE 11| year=1992| volume=607| pages=492–506| publisher=Springer| series=LNCS}}</ref>

{{clear}}