Christelle Scharff

BaCCS

Constrained equalities: eqconstrained.eln
This application permits to do:

Standard Completion with Standard Simplification compstandardstandard.eln

Basic Completion with Standard Simplification compbasicstandard.eln

Basic Completion with Basic Simplification with Retraction compbasicbasic.eln

Basic Completion with Basic Simplification without Retraction compbasicsr.eln

Basic Completion with E-cycle Simplification compbasicecycle.eln

An example of strategy in cpbasicbasic.eln:

strategies for eqconstrained
implicit
	[.] Main_BCP_a	=> dk(BCPRule1, BCPRule2, BCPRule3, BCPRule4, 
		BCPRule5, BCPRule6, BCPRule7, BCPRule8)
	end 

	[.] Main_BCP_b	=> dk(BCPRule1, BCPRule2, BCPRule3, BCPRule4)
	end 

	[.] BCP_compute	=> dk(BCP)
	end 
end

strategies for tuple[eqconstrained,eqconstrained]
implicit
	[.] Main_BSimp	=> first one(BSimprule1, BSimprule2, BSimprule3)
	end

	[.] BSimp	=> 
		first one(BBlockingLeft, BBlockingRight, 
		BSimpLeft, BSimpRight)
	end
end