package inference;

import java.util.List;

import models.algebra.Variable;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResourceVariable;

public class ProofSystem {

	private final static InferenceRule REFLEXIVE_LAW = new InferenceRule("relfexive law", List.of(), 
			new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("te"))));
	
	private final static InferenceRule SYMMETRIC_LAW = new InferenceRule("symmetric law", 
		List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("se")))),
		new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te"))));
	
	private final static InferenceRule TRANSITIVE_LAW = new InferenceRule("transitive law", 
			List.of(
					new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te"))),
					new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("ue")))
			),
			new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("ue")))
	);
	
	private final static InferenceRule IDENTITY_MAPPING = new InferenceRule("identity mapping", 
			List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v")))),
			new MetaDependencyFormula(new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v"))))
	);
	
	
	public ProofSystem() {
	}
	
	
}