Axioms and Transformations

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);