program-synthesis

At the moment, synthesis can take "hints" about auxiliary functions, which can be used for synthesing the main one. For instance, this is a specification for tree flattening that takes an auxiliary function:

{ lseg(x1, s1) ** lseg(x2, s2) ** ret :-> x2 }
void lseg_append (loc x1, loc ret)
{ s =i s1 ++ s2 ; lseg(y, s) ** ret :-> y }

{ z :-> x ** tree(x, s) }
void flatten(loc z)
{ z :

Suppose Popper generates this rule:

f(A):-
    has_car(A,B),
    has_car(A,C),
    long(B),
    long(C).

Then Popper's subsumption check will detect that two of the body literals are logically redundant.

Popper will then generate a generalisation co

[ ] - Syntax highlighting uses a slightly off-white background color. I see two options to fix this:

• Download the current styling sheet and modify it. https://highlightjs.org/static/demo/styles/github.css
• Find a different style with a white bg: https://highlightjs.org/static/demo/ Then edit the index.html file to use that style sheet instead.