Editing Program synthesis (section)

===Example===
{| class="wikitable" style="float:right;"
|+ Example synthesis of maximum function
|-
! Nr !! Assertions !! Goals !! Program !! Origin
|-
| 1 || <math>A=A</math> || ||  || Axiom
|-
| 2 || <math>A \leq A</math>  ||  || || Axiom
|-
| 3 || <math>A \leq B \lor B \leq A</math>  || ||  || Axiom
|-
| 10 || || <math>x \leq M \land y \leq M \land (x = M \lor y = M)</math> || M || Specification
|-
| 11 || || <math>(x \leq M \land y \leq M \land x = M) \lor (x \leq M \land y \leq M \land y = M)</math> || M || Distr(10)
|-
| 12 || || <math>x \leq M \land y \leq M \land x = M</math> || M || Split(11)
|-
| 13 || || <math>x \leq M \land y \leq M \land y = M</math> || M || Split(11)
|-
| 14 || || <math>x \leq x \land y \leq x</math> || x || Resolve(12,1)
|-
| 15 || || <math>y \leq x</math> || x || Resolve(14,2)
|-
| 16 || || <math>\lnot (x \leq y)</math> || x || Resolve(15,3)
|-
| 17 || || <math>x \leq y \land y \leq y</math> || y || Resolve(13,1)
|-
| 18 || || <math>x \leq y</math> || y || Resolve(17,2)
|-
| 19 || || <math>\textit{true}</math> || x<y [[?:|?]] y [[?:|:]] x || Resolve(18,16)
|}
As a toy example, a functional program to compute the maximum <math>M</math> of two numbers <math>x</math> and <math>y</math> can be derived as follows.{{citation needed|date=May 2016}}

Starting from the requirement description "''The maximum is larger than or equal to any given number, and is one of the given numbers''", the first-order formula <math>\forall X \forall Y \exists M: X \leq M \land Y \leq M \land (X=M \lor Y=M)</math> is obtained as its formal translation. This formula is to be proved. By reverse [[Skolemization]],<ref group=note>While ordinary Skolemization preserves satisfiability, reverse Skolemization, i.e. replacing universally quantified variables by functions, preserves validity.</ref> the specification in line 10 is obtained, an upper- and lower-case letter denoting a variable and a [[Skolem constant]], respectively.

After applying a transformation rule for the [[distributive law]] in line 11, the proof goal is a disjunction, and hence can be split into two cases, viz. lines 12 and 13.

Turning to the first case, resolving line 12 with the axiom in line 1 leads to [[Substitution (logic)#First-order logic|instantiation]] of the program variable <math>M</math> in line 14. Intuitively, the last conjunct of line 12 prescribes the value that <math>M</math> must take in this case. Formally, the non-clausal resolution rule shown in line 57 above is applied to lines 12 and 1, with <!---Using {{math}} here to make the color template work--->
* {{color|#008000|{{math|p}}}} being the common instance {{color|#008000|{{math|1=x=x}}}} of {{color|#408000|{{math|1=A=A}}}} and {{color|#008040|{{math|1=x=M}}}}, obtained by syntactically [[unification (computer science)#Syntactic unification of first-order terms|unifying]] the latter formulas,
* {{color|#800000|{{math|F[}}}}{{color|#008000|{{math|p}}}}{{color|#800000|{{math|]}}}} being {{color|#800000|{{math|''true'' ∧ }}}}{{color|#008000|{{math|1=x=x}}}}, obtained from [[Substitution (logic)#First-order logic|instantiated]] line 1 (appropriately padded to make the context {{color|#800000|{{math|F[⋅]}}}} around {{color|#008000|{{math|p}}}} visible), and 
* {{color|#000080|{{math|G[}}}}{{color|#008000|{{math|p}}}}{{color|#000080|{{math|]}}}} being {{color|#000080|{{math|x ≤ x ∧ y ≤ x ∧ }}}}{{color|#008000|{{math|1=x = x}}}}, obtained from instantiated line 12,
yielding
<math>\lnot (</math>{{color|#800000|{{math|''true'' ∧ }}}}{{color|#008000|{{math|''false''}}}}{{math|) ∧ (}}{{color|#000080|{{math|x ≤ x ∧ y ≤ x ∧ }}}}{{color|#008000|{{math|''true''}}}}<math>)</math>,
which simplifies to <math>x \leq x \land y \leq x</math>.

In a similar way, line 14 yields line 15 and then line 16 by resolution. Also, the second case, <math>x \leq M \land y \leq M \land y = M</math> in line 13, is handled similarly, yielding eventually line 18.

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&rarr;16 was needed. Intuitively, line 18 could be read as "in case <math>x \leq y</math>, the output <math>y</math> is valid (with respect to the original specification), while line 15 says "in case <math>y \leq x</math>, the output <math>x</math> is valid; the step 15&rarr;16 established that both cases 16 and 18 are complementary.<ref group=note>Axiom 3 was needed for that; in fact, if <math>\leq</math> wasn't a [[total order]], no maximum could be computed for uncomparable inputs <math>x,y</math>.</ref> Since both line 16 and 18 comes with a program term, a [[?:|conditional expression]] results in the program column. Since the goal formula <math>\textit{true}</math> has been derived, the proof is done, and the program column of the "<math>\textit{true}</math>" line contains the program.