%******************************************************************************
%*				 comments.pl				      *
%******************************************************************************

/*

%%% Logic algorithms are represented as follows:

LA ::=
	iff(Head,Body)

Head ::=	
	{ ... compound term whose arguments are different variables ... }

Body ::=
	or(MinCase,NRecCase,RecCase,Eqsss)

MinCase ::=
%	non-empty list (disjunction) of
		and(Minimal,Solve,MinEqsss)
	|
	undefined

NRecNMinCase ::=
%	non-empty list (disjunction) of
		and(NMinimal,Decompose,Discriminate,SolveNMin,NRecEqsss)
	|
	undefined

RecNMinCase ::=
	non-empty list (disjunction) of 
		and(NMinimal,Decompose,Discriminate,Recur,ProcComp,RecEqsss)
	|
	undefined

Minimal	
NMinimal,
Solve,
Decompose,
Discriminate,
SolveNMin,
Recur,
ProcComp ::=
	non-empty list (conjunction) of
		Literal
	|
	undefined

Literal ::=
	["~"] Atom

Atom ::=
	{ ... encoded compound Prolog term ... }

Eqsss,
MinEqsss,
NRecEqsss,
RecEqsss ::=
	list (disjunction) of
		non-empty list (conjunction) of
			non-empty list (conjunction) of
				Equation

Equation ::=
	=(EncodedVariable,Value)
	|
	in(EncodedVariable,list (set) of Value)

EncodedVariable ::=
	'$VAR'(Name,Quantifier)

Value ::=
	{ ... encoded Prolog term ... }

Name ::=
	'_'Integer
	|
	Prolog atom

Quantifier ::=
	existential
	|
	universal
	|
	dontKnow

%%% Each element Eqss of MinEqsss, NRecEqsss, or RecEqsss is
	(after Step 4) (and only if applicable):

	[Eqs1,Eqs3,Eqs4]

where:

	Eqs1 are equations for the variables X and Y introduced at Step 1;
	Eqs3 are equations for the variables HX and TX introduced at Step 
	Eqs4 are equations for the variables TY introduced at Step 4

*/

/*

%%% Examples and properties are represented as encoded definite clauses:

Example ::=
	HeadC ":-" true

Clause,
Property ::=
	HeadC ":-" BodyC

HeadC ::=
	{ ... encoded compound Prolog term ... }

BodyC ::=
	true
	|
	Atoms

Atoms ::=
	Atom
	|
	Atom "," Atoms

*/

/*

%%% Implicative goals are represented as follows:

ImplicativeGoal ::=
	if(Conclusion,Hypothesis)

Conclusion,
Hypothesis  ::=
	list (conjunction) of
		Atom

*/

/*

%%% Discriminants are represented as follows during Step 7:

Discriminant ::=
	list (conjunction) of Clause

*/

/*

%%% The variable Variables is a compound term defined as follows:

   Variables = variables(Params,IP,AuxParams,OtherParams,
   				DecVars,IPheads,IPtails,OtherTails)

where:
	Params are all the parameters;
	IP is the induction parameter of Params;
	AuxParams are the auxiliary parameters of Params;
	OtherParams are the other parameters of Params;
	DecVars are the heads and tails of IP;
	IPheads are the heads among DecVars;
	IPtails are the tails among DecVars;
	OtherTailss are the tailss of OtherParams;

such that the following invariants hold:

	 perm( [IP] <> AuxParams <> OtherParams , Params )
	 perm( IPheads <> IPtails , DecVars )			% sure?


%%% The variable Positions is a compound term defined as follows:

   Positions=positions(PosIP,PosAuxParams,PosOtherParams,PosIPheads,PosIPtails)

where:
	PosIP is the position of IP within Params;
	PosAuxParams are the positions of AuxParams within Params;
	PosOtherParams are the positions of OtherParams within Params;
	PosIPheads are the positions of IPheads within DecVars;
	PosIPtails are the positions of IPtails within DecVars;

such that the following invariant holds:

	 perm( [PosIP] <> PosAuxParams <> PosOtherParams , [1,2,...,n] )

*/
