******************************************************************************
*                                                                            *
*  DIALOGS - Dialog-based Inductive and Abductive LOGic program Synthesiser  *
*                                                                            *
*              Written in Quintus Prolog by: Pierre Flener  (19 June 1996)   *
*              With: Halime Buyukyildiz and Serap Yilmaz                     *
*                                                                            *
******************************************************************************

Please note that this is just a prototype  implementation  (version 1.0):  the
theory needs to be further developed  (coverage of examples with existentially
quantified  variables, etc.)  and certain parts of the code need to be further
refined.  The code was written for Quintus Prolog version 3.1.4.

Appended are some (ideally  self-explanatory)  annotated sample runs.  Start a
session  (after  loading of file  dialogs.pl)  by typing  "d."  or  "dialogs."
(without the quotes).  Before that, the command "aloud."  may be used to force
aloud  synthesis (the default mode), whereas the command "mute" may be used to
force mute synthesis  (recursively  invoked synthesis is automatically in mute
mode).

Variable names start with an uppercase  letter;  predicate names, functors and
constants start with a lowercase  letter.  Conjunction is expressed by a comma
(,),  disjunction  by a semi-colon  (;),  negation by wrapping the atom with a
prefix  neg/1  functor,  truth by "true" and falsity by "false"  (without  the
quotes).  The available  primitives are:  =/2, \=/2, ~=/2, length/2, append/3,
member/2,  nat/1, list/1, add/3, mult/3, lt/2, gt/2, le/2, ge/2,  partition/4,
and halves/3 (see file  primitives.pl).  Natural numbers should be typed in as
Peano numbers, using 0 for zero and prefix functor s/1 for successor.

During phase 1, answers  should *not* be terminated  by a full-stop  (.).  The
default answer (always between curly braces) can be selected by simply hitting
the RETURN/ENTER key.  You can force backtracking to a previous question using
the answer  "back"  (without  the  quotes).  Note that result  parameters  and
auxiliary  parameters are indicated as lists, using the Prolog  notation; that
means the absence of such  parameters is indicated  using the empty list ([]).
The type  language  can be  inferred  from the sample  runs  hereafter,  or by
looking at file  grammar.pl (see non-terminal type/1) or at file comments.txt.
Similarly for the predicate declaration language.

During phase 2, answers  *should* be terminated  by a full-stop  (.).  You can
express your boredom with the  questions  (or  unwillingness  or  inability to
answer them) by answering "stopit" (without the quotes).

There is no implemented  heuristic so far for deciding  whether DIALOGS should
call itself  recursively or not, so DIALOGS will ask you and thus rely on your
good judgment!

Use file phase2dev.pl instead of phase2.pl  during  compilation if you want to
observe phase 2 thinking aloud.

Feedback to the development team is always welcome.

Sincerely,
Pierre Flener (http://user.it.uu.se/~pierref/)


APPENDIX: SAMPLE RUNS

*** sort/2 ***
Predicate declaration?
s(L:list(int),S:list(int))
Induction Parameter? {L} L
Result Parameter(s)? {[S]} [S]
Decomposition Operator? {L=[HL|TL]} L=[HL|TL]
What conditions on <A> must hold such that s([],A) holds?
A=[].
What conditions on <A,B> must hold such that s([A],B) holds?
B=[A].
What conditions on <A,B,C> must hold such that s([A,B],C) holds?
C=[A,B],le(A,B);C=[B,A],gt(A,B).
What conditions on <A,B,C,D> must hold such that s([A,B,C],D) holds,
assuming le(B,C)?
D=[A,B,C],le(A,B);D=[B,A,C],gt(A,B),le(A,C);D=[B,C,A],gt(A,B),gt(A,C).
Need for recursive synthesis? [y/n] y
Need for recursive synthesis detected!
So far, the synthesized program is:
   s([],[])
   s([A|B],C) <-- s(B,D),dpcS(A,D,C)			CORRECT SO FAR!
Calling DIALOGS with the predicate declaration
   dpcS(HL:int,TS:list(int),S:list(int))
Induction Parameter? {TS} TS
Result Parameter(s)? {[S]} [S]
Auxiliary Parameter(s)? {[HL]} [HL]
Decomposition Operator? {TS=[HTS|TTS]} TS=[HTS|TTS]
... PROBLEM WITH PHASE 2 ...


*** length/2 ***
Predicate declaration?
len(L:list(term),N:nat)
Induction Parameter? {L} L
Result Parameter(s)? {[N]} [N]
Decomposition Operator? {L=[HL|TL]} L=[HL|TL]
What conditions on <A> must hold such that len([],A) holds?
A=0.
What conditions on <A,B> must hold such that len([A],B) holds?
B=s(0).
What conditions on <A,B,C> must hold such that len([A,B],C) holds?
C=s(s(0)).
What conditions on <A,B,C,D> must hold such that len([A,B,C],D) holds?
D=s(s(s(0))).
Need for recursive synthesis? [y/n] n
A possible program is:
   len([],0)
   len([A|B],s(C)) <-- len(B,C)				CORRECT PROGRAM!
Do you want another logic program? {yes} yes
Backtracking...
Decomposition Operator? {L=[H1,H2|T],halves(L,TL1,TL2)} back	BACKTRACKING
Decomposition Operator? back					BACKTRACKING
Induction Parameter? {N} N
Result Parameter(s)? {[L]} [L]
Decomposition Operator? {N=s(TN),HN=N} N=s(TN),HN=N
Need for recursive synthesis? [y/n] n
...EXISTENTIAL VARIABLES APPEAR IN THE DPClen/3 EVIDENCE,
   SUCH AS DPClen(2,[A],[B,C]) INSTEAD OF DPClen(2,[A],[B,A])
   --> NEED FOR IMPLEMENTATION OF EXISTENTIAL CASE! ...


*** length/2 again ***
Predicate declaration?
len(L:list(term),N:nat)
Induction Parameter? {L} N		THE USER DID NOT ACCEPT DEFAULT ANSWER
Result Parameter(s)? {[L]} [L]
Decomposition Operator? {N=s(TN),HN=N} N=s(TN),HN=N
What conditions on <A> must hold such that len(A,0) holds?
A=[].
What conditions on <A> must hold such that len(A,s(0)) holds?
A=[Z].
What conditions on <A> must hold such that len(A,s(s(0))) holds?
A=[X,Y].
What conditions on <A> must hold such that len(A,s(s(s(0)))) holds?
A=[U,V,W].
Need for recursive synthesis? [y/n] n
...EXISTENTIAL VARIABLES APPEAR IN THE DPClen/3 EVIDENCE,
   SUCH AS DPClen(2,[A],[B,C]) INSTEAD OF DPClen(2,[A],[B,A])
   --> NEED FOR IMPLEMENTATION OF EXISTENTIAL CASE! ...


*** delOdds/2 ***
Predicate declaration?
delOdds(L:list(int),R:list(int))
Induction Parameter? {L} L
Result Parameter(s)? {[R]} [R]
Decomposition Operator? {L=[HL|TL]} L=[HL|TL]
What conditions on <A> must hold such that delOdds([],A) holds?
A=[].
What conditions on <A,B> must hold such that delOdds([A],B) holds?
B=[],odd(A);B=[A],even(A).
What conditions on <A,B,C> must hold such that delOdds([A,B],C) holds,
assuming even(B)?
C=[B],odd(A);C=[A,B],even(A).
What conditions on <A,B,C,D> must hold such that delOdds([A,B,C],D) holds,
assuming even(B),even(C)?
stopit.			THE USER IS BORED
What conditions on <A,B,C,D> must hold such that delOdds([A,B,C],D) holds?
stopit.			THE USER IS STILL BORED
Need for recursive synthesis? [y/n] n
A possible program is:
   delOdds([],[])
   delOdds([D|E],F) <-- delOdds(E,F),odd(D)
   delOdds([A|B],[A|C]) <-- delOdds(B,C),even(A)	CORRECT PROGRAM!
Do you want another logic program? {yes} no
No (more) programs.


*** member/2 ***
Predicate declaration?
mem(L:list(atom),E:atom)
Induction Parameter? {L} L
Auxiliary Parameter(s)? {[E]} [E]
Decomposition Operator? {L=[HL|TL]} L=[HL|TL]
What conditions on <A> must hold such that mem([],A) holds?
false.
What conditions on <A,B> must hold such that mem([A],B) holds?
B=A.
What conditions on <A,B,B> must hold such that mem([A,B],B) holds?
true.
What conditions on <A,B,C,D> must hold such that mem([A,B,C],D) holds?
D=A;D=B;D=C.
Need for recursive synthesis? [y/n] n
... PROBLEM WITH PHASE 2 ...


*** compress/2 ***
Predicate declaration?
compress(L:list(atom),R:list(atom))
Induction Parameter? {L} L
Result Parameter(s)? {[R]} [R]
Decomposition Operator? {L=[HL|TL]} L=[HL|TL]
What conditions on <A> must hold such that compress([],A) holds?
A=[].
What conditions on <A,B> must hold such that compress([A],B) holds?
B=[A,s(0)].
What conditions on <A,B,C> must hold such that compress([A,B],C) holds?
C=[A,s(s(0))],eq(A,B);C=[A,s(0),B,s(0)],diff(A,B).
What conditions on <A,B,C,D> must hold such that compress([A,B,C],D) holds,
assuming eq(B,C)?
D=[A,s(s(s(0)))],eq(A,B);D=[A,s(0),B,s(s(0))],diff(A,B).
What conditions on <A,B,C,D> must hold such that compress([A,B,C],D) holds,
assuming diff(B,C)?
D=[A,s(s(0)),C,s(0)],eq(A,B);D=[A,s(0),B,s(0),C,s(0)],diff(A,B).
Need for recursive synthesis? [y/n] n
A possible program is:
   compress([],[])					CORRECT PROGRAM!
   compress([K],[K,s(0)])
   compress([F|G],[F,s(s(H))|I]) <-- compress(G,[J,s(H)|I]),eq(F,J)
   compress([A|B],[A,s(0),C,s(D)|E]) <-- compress(B,[C,s(D)|E]),diff(A,C)
Do you want another logic program? {yes} yes
Backtracking...
Decomposition Operator? {L=[H1,H2|T],halves(L,TL1,TL2)} back
Decomposition Operator? back
Induction Parameter? {R} R
Result Parameter(s)? {[L]} [L]
Decomposition Operator? {R=[HR|TR]} R=[HR1,HR2|TR]
What conditions on <A,B> must hold such that compress(A,[B]) holds?
... PROBLEM WITH PHASE 2 ...
