diff --git a/src/main/java/Main.java b/src/main/java/Main.java index 79908d4..f8508b2 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -1,19 +1,13 @@ -import com.google.common.collect.TreeMultimap; - import java.util.HashMap; -import java.util.List; import java.util.Map; +import com.google.common.collect.TreeMultimap; + import constants.Types; -import inference.axioms.RightSubstitution; import models.algebra.Constant; import models.algebra.Expression; import models.algebra.Type; import models.algebra.Variable; -import models.formulas.DependencyFormula; -import models.formulas.EquationFormula; -import models.terms.DependencyTerm; -import models.terms.Resource; import models.terms.meta.MetaDynamicDependency; import models.terms.meta.MetaDynamicDependencyTerm; import models.terms.meta.MetaRDLTerm; @@ -30,7 +24,6 @@ sandbox2(); sandbox3(); sandbox4(); - sandbox5(); } @@ -84,30 +77,4 @@ System.out.println(t1.generate(0, 5, 0, null)); System.out.println(t2.generate(0, 3, 2, null)); } - - static void sandbox5() { - RightSubstitution rs = new RightSubstitution(); - Resource a = new Resource("a", 1); - Resource b = new Resource("b", 1); - Resource c = new Resource("c", 1); - Resource d = new Resource("d", 1); - Resource e = new Resource("e", 1); - Resource f = new Resource("f", 1); - Resource g = new Resource("f", 1); - Resource h = new Resource("h", 1); - Resource i = new Resource("i", 1); - Resource j = new Resource("j", 1); - Resource k = new Resource("k", 1); - Resource l = new Resource("l", 1); - EquationFormula eq = new EquationFormula(a, b); - DependencyFormula dep = new DependencyFormula(c, d); - EquationFormula eq2 = new EquationFormula(new DependencyTerm(d, e, f), a); - System.out.println(rs.apply(List.of(eq, dep, eq2))); - DependencyTerm t1 = new DependencyTerm(c, d, a); - System.out.println(rs.generateRightSideHand(List.of(eq, dep, eq2), t1)); - DependencyFormula dep2 = new DependencyFormula(c, g); - EquationFormula eq3 = new EquationFormula(new DependencyTerm(g, h, i), j); - System.out.println(rs.apply(List.of(eq, eq2, eq3, dep, dep2))); - } - } diff --git a/src/main/java/inference/EquationAxiom.java b/src/main/java/inference/EquationAxiom.java new file mode 100644 index 0000000..33b79b4 --- /dev/null +++ b/src/main/java/inference/EquationAxiom.java @@ -0,0 +1,53 @@ +package inference; + +import java.util.List; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import models.formulas.Formula; +import models.formulas.meta.MetaEquationFormula; +import models.formulas.meta.MetaFormula; +import models.terms.RDLTerm; +import models.terms.meta.MatchConstraint; +import utils.Permutation; + +public class EquationAxiom extends InferenceRule{ + + public EquationAxiom(String name) { + super(name); + } + + public EquationAxiom( + String name, + List assumptions, + List repetitionAssumptions, + MetaFormula conclusion, + InferenceOrderConstraint constraint, + ConclusionSizeCalculator conclusionMaxIndexCalculator, + ConclusionSizeCalculator conclusionMaxDepthCalculator, + AssumptionSizeCalculator assumptionSizeCalculator + ) { + super(name, assumptions, repetitionAssumptions, conclusion, constraint, conclusionMaxIndexCalculator, conclusionMaxDepthCalculator, assumptionSizeCalculator); + } + + public RDLTerm generateRightSideHand(List assumptions, RDLTerm leftSideHand) { + if (! (this.conclusion instanceof MetaEquationFormula)) return null; + if (this.assumptions.size() > assumptions.size()) return null; + MetaEquationFormula metaFormula = (MetaEquationFormula) this.conclusion; + Set constraints = metaFormula.getLeftSideHand().isMatchedBy(leftSideHand); + for (List assumptionList: Permutation.permutation(assumptions, assumptions.size())) { + for (int i = 0; i < getAssumptionSize(); i++) { + constraints = this.assumptions.get(i).isMatchedBy(assumptionList.get(i), constraints); + } + for (MatchConstraint constraint: constraints) { + try { + return metaFormula.getRightSideHand().substitute(constraint.getBinding()); + } catch (SubstituteFailedException e) { + continue; + } + } + } + return null; + } + +} diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index eb955e1..c7f09c7 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -1,7 +1,6 @@ package inference; import java.util.ArrayList; -import java.util.Collection; import java.util.HashMap; import java.util.HashSet; import java.util.List; @@ -10,11 +9,8 @@ import exceptions.SubstituteFailedException; import lombok.Getter; -import models.algebra.Variable; import models.formulas.Formula; -import models.formulas.meta.MetaEquationFormula; import models.formulas.meta.MetaFormula; -import models.terms.RDLTerm; import models.terms.meta.MatchConstraint; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaVariable; @@ -26,12 +22,12 @@ protected String name; @Getter - protected List assumptions; + protected List assumptions = new ArrayList<>(); @Getter protected MetaFormula conclusion; protected InferenceOrderConstraint defaultOrderConstraint; - protected List repetitionAssumptions; + protected List repetitionAssumptions = new ArrayList<>(); protected ConclusionSizeCalculator conclusionMaxIndexCalculator; protected ConclusionSizeCalculator conclusionMaxDepthCalculator; protected AssumptionSizeCalculator assumptionRepetitionSizeCalculator; @@ -79,110 +75,29 @@ this("undefined", assumptions, conclusion, null); } - public boolean check(Collection assumptions, Formula conclusion) { - - if (this.assumptions.size() > assumptions.size()) { - return false; - } - - for(List assumption : Permutation.permutation(assumptions, this.assumptions.size())) { - if (check(assumption, conclusion)) { - return true; - } - } - return false; - } - private boolean check(List assumptions, Formula conclusion) { - Set matchResult = this.assumptions.get(0).isMatchedBy(assumptions.get(0)); - for (int i = 1; i < assumptions.size(); i++) { - matchResult = this.assumptions.get(i).isMatchedBy(assumptions.get(i), matchResult); - if (matchResult.isEmpty()) { - return false; - } - } - - if (this.conclusion.isMatchedBy(conclusion, matchResult).isEmpty()) { - return false; - } - if (this.defaultOrderConstraint != null) { - for (MatchConstraint constraint: matchResult) { - if (defaultOrderConstraint.check(constraint.getOrderConstraint())) { - return true; - } - } - return false; - } - return true; - } - - - public Set apply(List assumptions, Set existTerms) { - Set result = new HashSet<>(); - Set assumptionVariables = new HashSet<>(); - Set conclusionVariables = new HashSet<>(); - for (MetaFormula assumption: this.assumptions) { - assumptionVariables.addAll(assumption.getSubTerms(MetaVariable.class)); - } - conclusionVariables.addAll(conclusion.getSubTerms(MetaVariable.class)); - - conclusionVariables.removeAll(assumptionVariables); - List leftVariables = new ArrayList<>(conclusionVariables); - - if (! conclusionVariables.isEmpty()) { - for (List variables: Permutation.permutation(existTerms, leftVariables.size())) { - Map binding = new HashMap<>(); - for (int i = 0; i < variables.size(); i++) { - binding.put(leftVariables.get(i).getVariableName(), variables.get(i)); - } - try { - Formula res = apply(assumptions, new MatchConstraint(binding, new HashMap<>())); - if (res != null) { - // ??? - Set constraints = conclusion.isMatchedBy(res); - boolean flg = true; - for (MatchConstraint constraint : constraints) { - if (defaultOrderConstraint != null && ! defaultOrderConstraint.check(constraint.getOrderConstraint())) { - flg = false; - break; - } - } - if (flg) { - result.add(res); - } - } - } catch (SubstituteFailedException e) { - continue; - } - } - } - return result; - } - - public Formula apply(Formula ...assumptions) { + public Set apply(Formula ...assumptions) { return apply(Set.of(assumptions)); } - public Formula apply(Collection assumptions) { + public Set apply(Set assumptions) { if (assumptions.size() < getAssumptionSize()) { - return null; + return new HashSet<>(); } + Set result = new HashSet<>(); for (List assumptionList : Permutation.permutation(assumptions, assumptions.size())) { - Formula result = apply(assumptionList); - if (result != null) { - return result; - } + result.addAll(apply(assumptionList)); } - return null; + return result; } - protected Formula apply(List assumptions) { + protected Set apply(List assumptions) { return apply(assumptions, MatchConstraint.createDefault()); } - protected Formula apply(List assumptions, MatchConstraint constraint) { + protected Set apply(List assumptions, MatchConstraint constraint) { if (assumptions.size() < getAssumptionSize()) { - return null; + return new HashSet<>(); } Set result = new HashSet<>(); @@ -190,22 +105,31 @@ for (int i = 0; i < getAssumptionSize(); i++) { result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result); if (result.isEmpty()) { - return null; + return new HashSet<>(); } } -// if (hasDynamicAssumption) { -// for (int i = 0; i < assumptions.size() - getAssumptionSize(); i++) { -// int j = getAssumptionSize() + i; -// result = this.generator.generate(i).isMatchedBy(assumptions.get(j), result); -// if (result.isEmpty()) { -// return null; -// } -// } -// } - Formula subRes = null; + if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) { + return new HashSet<>(); + } + if (this.repetitionAssumptions.size() != 0) { + for (int i = 0; i < (assumptions.size() - this.assumptions.size()) / this.repetitionAssumptions.size(); i++) { + List metaAssumptions = repetitionAssumptionGenerate(i); + for (int j = 0; j < this.repetitionAssumptions.size(); j++) { + Formula assumption = assumptions.get(this.assumptions.size() + i * this.repetitionAssumptions.size() + j); + MetaFormula metaAssumption = metaAssumptions.get(j); + result = metaAssumption.isMatchedBy(assumption, result); + if (result.isEmpty()) { + return new HashSet<>(); + } + } + } + } + Set subRes = new HashSet<>(); for (MatchConstraint con: result) { try { - subRes = conclusion.substitution(con.getBinding(), new HashMap<>()); + int maxIndex = conclusionMaxIndexCalculator != null ? conclusionMaxIndexCalculator.calculate(assumptions) : 0; + int maxDepth = conclusionMaxDepthCalculator != null ? conclusionMaxDepthCalculator.calculate(assumptions) : 0; + subRes.add(conclusion.substitution(con.getBinding(), Map.of("maxIndex", maxIndex, "maxDepth", maxDepth))); } catch (SubstituteFailedException e) { continue; } @@ -214,36 +138,25 @@ } - public RDLTerm generateRightSideHand(List assumptions, RDLTerm leftSideHand) { - if (! (this.conclusion instanceof MetaEquationFormula)) return null; - if (this.assumptions.size() > assumptions.size()) return null; - MetaEquationFormula metaFormula = (MetaEquationFormula) this.conclusion; - Set constraints = metaFormula.getLeftSideHand().isMatchedBy(leftSideHand); - for (List assumptionList: Permutation.permutation(assumptions, assumptions.size())) { - for (int i = 0; i < getAssumptionSize(); i++) { - constraints = this.assumptions.get(i).isMatchedBy(assumptionList.get(i), constraints); - } -// if (hasDynamicAssumption) { -// for (int i = 0; i < assumptions.size() - getAssumptionSize(); i++) { -// int j = getAssumptionSize() + i; -// constraints = this.generator.generate(i).isMatchedBy(assumptions.get(j), constraints); -// } -// } - for (MatchConstraint constraint: constraints) { - try { - return metaFormula.getRightSideHand().substitute(constraint.getBinding()); - } catch (SubstituteFailedException e) { - continue; - } - } - } - return null; - } - public int getAssumptionSize() { return this.assumptions.size(); } + protected List repetitionAssumptionGenerate(int i) { + if (i == 0) { + return new ArrayList<>(this.repetitionAssumptions); + } + List result = new ArrayList<>(); + for (MetaFormula metaFormula : this.repetitionAssumptions) { + Map mapping = new HashMap<>(); + for (MetaVariable variable : metaFormula.getAllVariables()) { + mapping.put(variable, variable.cloneWithName(variable.getVariableName().getName() + i)); + } + result.add(metaFormula.replace(mapping)); + } + return result; + } + public String toString() { StringBuilder sb = new StringBuilder(); @@ -269,21 +182,6 @@ return sb.toString(); } - protected List repetitionAssumptionGenerate(int i) { - if (i == 0) { - return new ArrayList<>(this.repetitionAssumptions); - } - List result = new ArrayList<>(); - for (MetaFormula metaFormula : this.repetitionAssumptions) { - Map mapping = new HashMap<>(); - for (MetaVariable variable : metaFormula.getAllVariables()) { - mapping.put(variable, variable.cloneWithName(variable.getVariableName().getName() + i)); - } - result.add(metaFormula.replace(mapping)); - } - return result; - } - @Override public boolean equals(Object another) { if (! (another instanceof InferenceRule)) { diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 26eaad3..d68fac9 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -12,14 +12,20 @@ import java.util.Set; import java.util.stream.Collectors; +import inference.axioms.RightSubstitution; import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; import models.formulas.meta.MetaEquationFormula; import models.terms.EvaluatableTerm; import models.terms.RDLTerm; +import models.terms.meta.MetaDependencyTerm; +import models.terms.meta.MetaDynamicDependencyTerm; import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; import utils.Product; public class ProofSystem { @@ -68,6 +74,131 @@ ); + public static final InferenceRule rightSubstitution = new RightSubstitution(); + + public static final InferenceRule leftSubstitution = new EquationAxiom( + "Left Substitution", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ), + List.of( + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re")) + ), + new MetaEquationFormula( + new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("re")), + new MetaEvaluatableTermVariable(new Variable("x")), + new MetaEvaluatableTermVariable(new Variable("y")) + ), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ), + new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("re")); + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); + } + if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("ue")); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")) + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("re")); + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); + } + if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("ue")); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ), + null, + (assumptions) -> (assumptions.size() - 1) / 2 * 2 + 1, + (assumptions) -> 1, + (conclusion) -> (conclusion.getMaxIndex() - 1) / 2 + ); + + + public static final InferenceRule identity = new EquationAxiom( + "Identity", + List.of(), + List.of( + new MetaEquationFormula( + new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("x")), + new MetaEvaluatableTermVariable(new Variable("y")) + ), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ), + new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("se")); + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("se" + curIndex / 2)); + } + if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("te")); + } + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); + } + + }, + new MetaEvaluatableTermVariable(new Variable("se")) + ), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + null, + (assumptions) -> assumptions.size() * 2 + 1, + (assumptions) -> 1, + (conclusion) -> (conclusion.getMaxIndex() - 1) / 2 + ); + + public static final InferenceRule mapComposition = new EquationAxiom( + "Map Composition", + List.of(), + List.of(), + null, + null, + null, + null, + null + ); + + // // //======================Dependency Axioms============================= // @@ -208,7 +339,7 @@ } for(List applyFormulas : Product.product(matchedFormulas)) { if (appliedFormulas.contains(applyFormulas)) continue; - Set applied = axiom.apply(applyFormulas, existTerms); + Set applied = axiom.apply(applyFormulas); if (applied != null) { for (Formula formula : applied) { if (! formulas.contains(formula)) { diff --git a/src/main/java/inference/axioms/RightSubstitution.java b/src/main/java/inference/axioms/RightSubstitution.java index b8f3929..f3219d0 100644 --- a/src/main/java/inference/axioms/RightSubstitution.java +++ b/src/main/java/inference/axioms/RightSubstitution.java @@ -6,7 +6,7 @@ import java.util.Set; import exceptions.SubstituteFailedException; -import inference.InferenceRule; +import inference.EquationAxiom; import models.algebra.Variable; import models.formulas.Formula; import models.formulas.meta.MetaDependencyFormula; @@ -20,7 +20,7 @@ import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaTermGenerator; -public class RightSubstitution extends InferenceRule { +public class RightSubstitution extends EquationAxiom { public RightSubstitution() { super("Right Substitution"); @@ -88,7 +88,7 @@ } @Override - protected Formula apply(List assumptions, MatchConstraint constraint) { + protected Set apply(List assumptions, MatchConstraint constraint) { Set result = new HashSet<>(); result.add(constraint); for (int i = 0; i < this.assumptions.size(); i++) { @@ -96,11 +96,11 @@ Formula assumption = assumptions.get(i); result = metaAssumption.isMatchedBy(assumption, result); if (result.isEmpty()) { - return null; + return new HashSet<>(); } } if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) { - return null; + return new HashSet<>(); } for (int i = 0; i < (assumptions.size() - this.assumptions.size()) / this.repetitionAssumptions.size(); i++) { List metaAssumptions = repetitionAssumptionGenerate(i); @@ -109,16 +109,16 @@ MetaFormula metaAssumption = metaAssumptions.get(j); result = metaAssumption.isMatchedBy(assumption, result); if (result.isEmpty()) { - return null; + return new HashSet<>(); } } } - Formula subRes = null; + Set subRes = new HashSet<>(); for (MatchConstraint con: result) { try { int maxIndex = conclusionMaxIndexCalculator != null ? conclusionMaxIndexCalculator.calculate(assumptions) : 0; int maxDepth = conclusionMaxDepthCalculator != null ? conclusionMaxDepthCalculator.calculate(assumptions) : 0; - subRes = conclusion.substitution(con.getBinding(), Map.of("maxIndex", maxIndex, "maxDepth", maxDepth)); + subRes.add(conclusion.substitution(con.getBinding(), Map.of("maxIndex", maxIndex, "maxDepth", maxDepth))); } catch (SubstituteFailedException e) { continue; } diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java index a3e0efa..198fb85 100644 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -1,6 +1,18 @@ package inferencerule; +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; +import java.util.Set; + +import org.junit.jupiter.api.Test; + +import inference.ProofSystem; +import inference.axioms.RightSubstitution; +import models.formulas.DependencyFormula; +import models.formulas.EquationFormula; +import models.formulas.Formula; +import models.terms.DependencyTerm; import models.terms.Resource; -import utils.Utils; public class EqualityAxiomTest { @@ -11,10 +23,72 @@ Resource e = new Resource("e", 1); Resource f = new Resource("f", 1); Resource g = new Resource("g", 1); - Resource h = new Resource("h", 2); - Resource i = new Resource("i", 2); - Resource j = new Resource("j", 2); - Resource k = new Resource("k", 2); + Resource h = new Resource("h", 1); + Resource i = new Resource("i", 1); + Resource j = new Resource("j", 1); + Resource k = new Resource("k", 1); Resource l = new Resource("l", 1); + @Test + void ReflexivityTest() { + } + + @Test + void SymmetryTest() { + EquationFormula eq1 = new EquationFormula(a, b); + Set result = ProofSystem.symmetry.apply(eq1); + assertTrue(result.contains(new EquationFormula(b, a))); + } + + @Test + void TransitivityTest() { + EquationFormula eq1 = new EquationFormula(a, b); + EquationFormula eq2 = new EquationFormula(b, c); + EquationFormula eq3 = new EquationFormula(a, c); + Set result = ProofSystem.transitivity.apply(eq1, eq2); + assertTrue(result.contains(eq3)); + + } + + @Test + void RightSubTest() { + RightSubstitution rs = new RightSubstitution(); + EquationFormula eq = new EquationFormula(a, b); + DependencyFormula dep = new DependencyFormula(c, d); + DependencyTerm t1 = new DependencyTerm(c, d, a); + DependencyTerm t2 = new DependencyTerm(c, d, b); + EquationFormula eq2 = new EquationFormula(new DependencyTerm(d, e, f), a); + Set result = rs.apply(Set.of(eq, dep, eq2)); + assertTrue(result.contains(new EquationFormula(t1, t2))); + + assertEquals(rs.generateRightSideHand(List.of(eq, dep, eq2), t1), t2); + DependencyFormula dep2 = new DependencyFormula(c, g); + EquationFormula eq3 = new EquationFormula(new DependencyTerm(g, h, i), j); + DependencyTerm t3 = new DependencyTerm(c, d, a, g, j); + DependencyTerm t4 = new DependencyTerm(c, d, b, g, j); + result = rs.apply(Set.of(eq, eq2, eq3, dep, dep2)); + assertTrue(result.contains(new EquationFormula(t3, t4))); + } + + @Test + void LeftSubTest() { + EquationFormula eq1 = new EquationFormula(a, b); + DependencyFormula d1 = new DependencyFormula(a, c); + EquationFormula eq2 = new EquationFormula(new DependencyTerm(c, d, e), f); + Set result = ProofSystem.leftSubstitution.apply(eq1, d1, eq2); + assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, c, f), new DependencyTerm(b, c, f)))); + } + + @Test + void IdentityTest() { + EquationFormula eq1 = new EquationFormula(new DependencyTerm(a, b, c), d); + Set result = ProofSystem.identity.apply(eq1); + assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, a, d), d))); + + EquationFormula eq2 = new EquationFormula(new DependencyTerm(a, b, c), d); + EquationFormula eq3 = new EquationFormula(new DependencyTerm(e, f, g), h); + result = ProofSystem.identity.apply(eq2, eq3); + assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, a, d, e, h), d))); + } + }