May 20, 2013 at 5:39 PM
Edited May 26, 2013 at 9:11 PM

Hi,
I'm just wondering how I can define Axioms based on Inference Rules.
Wikipedia: Rule of inference
I guess there should be something like Expression Tree matching and Transformation.
That is, to define a new Axiom like the commutative property by defining a matching filter and a transformation:
// defining a matching filter function that gets applied on a node of the expression tree
var match = (IExpressionTree tree) => { tree.Where(subtree =>
subtree as Power != null &&
(subtree as Power).Left as AbelianGroup != null &&
(subtree as Power).Right != null);
};
// add an transformation that transforms an ExpressionTree
// into another ExpressionTree by transforming the matched Subtree
var axioms = new AxiomSet();
axioms.Map<ExpressionTree, ExpressionTree>(match, (subtree) => new (subtree as Power).Right.Power((subtree as Power).Right), "commutative" );
// define an equation
var equation1 = QsInteger(5).Power(QsInteger(6));
var equation2 = QsInteger(6).Power(QsInteger(5));
// find an solution by applying transfomations
// the search algorithm goes through the possible states
// of transformed equations to find a solution
// each transformation has an associated cost to determine the most efficient path
var result = Engine.Solve(SearchAlgorithm.AStar, equation1, equation2);

