Uses of Class
dev.civl.sarl.prove.IF.ProverFunctionInterpretation

Packages that use ProverFunctionInterpretation

Package	Description
dev.civl.sarl.IF	This package and its subpackages provide the "public interface" to SARL.
dev.civl.sarl.prove.IF	Module "prove" constitutes the interface between SARL and (possibly external) theorem provers.
dev.civl.sarl.reason.IF	The internal interface for the "reason" module, which deals with Reasoners --- objects used to prove theorems and simplify symbolic expressions.

Uses of ProverFunctionInterpretation in dev.civl.sarl.IF

Methods in dev.civl.sarl.IF with parameters of type ProverFunctionInterpretation

Modifier and Type	Method	Description
void	SymbolicUniverse.setLogicFunctions(ProverFunctionInterpretation[] logicFunctions)	Set a list of logic functions with their definitions to the universe so that Reasoners created by this universe can take use of the definitions of the given logic functions.

Uses of ProverFunctionInterpretation in dev.civl.sarl.prove.IF

Methods in dev.civl.sarl.prove.IF that return ProverFunctionInterpretation

Modifier and Type	Method	Description
static ProverFunctionInterpretation	ProverFunctionInterpretation.newProverPredicate(SymbolicUniverse universe, String identifier, SymbolicConstant[] parameters, SymbolicExpression definition)

Methods in dev.civl.sarl.prove.IF with parameters of type ProverFunctionInterpretation

Modifier and Type	Method	Description
int	ProverFunctionInterpretation.compareTo(ProverFunctionInterpretation o)
TheoremProver	TheoremProverFactory.newProver(BooleanExpression context, ProverFunctionInterpretation[] logicFunctions)	Returns a new instance of TheoremProver with the given context.

Uses of ProverFunctionInterpretation in dev.civl.sarl.reason.IF

Methods in dev.civl.sarl.reason.IF with parameters of type ProverFunctionInterpretation

Modifier and Type	Method	Description
Reasoner	ReasonerFactory.getReasoner(BooleanExpression context, boolean useBackwardSubstitution, ProverFunctionInterpretation[] proverPredicates)	Gets a Reasoner for the given context.
Reasoner	ReasonerFactory.getReasoner(List<BooleanExpression> contextStack, boolean useBackwardSubstitution, ProverFunctionInterpretation[] proverPredicates)