diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index cf776c8..51fda3f 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -4,13 +4,19 @@ import java.util.List; import java.util.Set; +import inference.axioms.ArgumentConstraint; import inference.axioms.ArgumentExtension; +import inference.axioms.ArgumentReduction; +import inference.axioms.CompositeMapping; +import inference.axioms.ConstantMapping; import inference.axioms.Constantness; +import inference.axioms.DependencyExtension; import inference.axioms.Identity; import inference.axioms.LeftSubstitution; import inference.axioms.MapComposition; import inference.axioms.PseudoConstantness; import inference.axioms.RightSubstitution; +import inference.axioms.UncurriedMapping; import inference.axioms.Uncurrying; import models.algebra.Variable; import models.formulas.DependencyFormula; @@ -108,38 +114,17 @@ public static final InferenceRule argumentExtension = new ArgumentExtension(); -// public static final InferenceRule compositeMapping = new CompositeMapping(); + public static final InferenceRule argumentReduction = new ArgumentReduction(); -// public static final InferenceRule constantMapping = new InferenceRule( -// "Constant Mapping", -// List.of(), -// List.of(), -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), -// new MetaEvaluatableTermVariable(new Variable("re"), new Variable("m")) -// ), -// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")), -// null, -// null, -// null -// ); + public static final InferenceRule argumentConstraint = new ArgumentConstraint(); -// public static final InferenceRule uncurriedMapping = new UncurriedMapping(); + public static final InferenceRule compositeMapping = new CompositeMapping(); -// public static final InferenceRule redundantDependency = new InferenceRule( -// "Redundant Dependency", -// List.of( -// new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n"))) -// ), -// List.of(), -// new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")), new MetaEvaluatableTermVariable(new Variable("p"), ExpressionUtils.parse("n - 1"))), -// null, -// null, -// null, -// null -// ); + public static final InferenceRule constatnMapping = new ConstantMapping(); -// public static final InferenceRule redundancyElimination = new RedundancyElimination(); + public static final InferenceRule uncurriedMapping = new UncurriedMapping(); + + public static final InferenceRule dependencyExtension = new DependencyExtension(); /* * new InferenceRule( diff --git a/src/main/java/inference/axioms/ArgumentConstraint.java b/src/main/java/inference/axioms/ArgumentConstraint.java new file mode 100644 index 0000000..46ccd6e --- /dev/null +++ b/src/main/java/inference/axioms/ArgumentConstraint.java @@ -0,0 +1,97 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.InferenceRule; +import models.Position; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaConstant; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class ArgumentConstraint extends InferenceRule { + + public ArgumentConstraint() { + super("Argument Constraint"); + + assumptions.add(new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 3; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ye")) + ), + new MetaConstant(new Variable("c")) + )); + + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + )); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaEvaluatableTermVariable(new Variable("ye")) + ); + } + + @Override + public Set derive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (this.assumptions.size() != assumptions.size()) { + return new HashSet<>(); + } + Set matchResult = assumptionMatch(assumptions, constraint); + + for (MatchConstraint res: matchResult) { + try { + res.getContext().put(new Position(), (Integer) res.getContext().get(new Position()) * 2 - 1); + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/ArgumentReduction.java b/src/main/java/inference/axioms/ArgumentReduction.java new file mode 100644 index 0000000..40b47ec --- /dev/null +++ b/src/main/java/inference/axioms/ArgumentReduction.java @@ -0,0 +1,87 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.InferenceRule; +import models.Position; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class ArgumentReduction extends InferenceRule { + + public ArgumentReduction() { + super("Argument Reduction"); + + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + context.put("k", curIndex); + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + )); + + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 2; + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + )); + + conclusion = new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")) + ) + ); + + } + + public Set derive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (this.assumptions.size() != assumptions.size()) { + return new HashSet<>(); + } + + Set matchResult = assumptionMatch(assumptions, constraint); + + for (MatchConstraint res: matchResult) { + try { + res.getContext().put(new Position(), (Integer) res.getContext().get(new Position()) - 1); + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/CompositeMapping.java b/src/main/java/inference/axioms/CompositeMapping.java new file mode 100644 index 0000000..8406ca1 --- /dev/null +++ b/src/main/java/inference/axioms/CompositeMapping.java @@ -0,0 +1,99 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.InferenceRule; +import models.Position; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class CompositeMapping extends InferenceRule { + + public CompositeMapping() { + super("Composite Mapping"); + + assumptions.add( + new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + context.put("k", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ); + + assumptions.add( + new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 2; + context.put("n", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ); + + conclusion = new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + int k = (Integer) context.get("k"); + if (curIndex < k) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + curIndex -= k; + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")) + ) + ); + } + + @Override + public Set derive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (this.assumptions.size() != assumptions.size()) { + return new HashSet<>(); + } + + Set matchResult = assumptionMatch(assumptions, constraint); + + for (MatchConstraint res: matchResult) { + try { + int k = (Integer) res.getContext().get("k"); + int n = (Integer) res.getContext().get("n"); + res.getContext().put(new Position(), k + n + 1); + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/ConstantMapping.java b/src/main/java/inference/axioms/ConstantMapping.java new file mode 100644 index 0000000..633a497 --- /dev/null +++ b/src/main/java/inference/axioms/ConstantMapping.java @@ -0,0 +1,34 @@ +package inference.axioms; + +import java.util.Map; + +import inference.InferenceOrderConstraint; +import inference.InferenceRule; +import models.algebra.Variable; +import models.formulas.meta.MetaDependencyFormula; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; +import models.terms.meta.OrderConstraint; + +public class ConstantMapping extends InferenceRule { + + public ConstantMapping() { + super("Constant Mapping"); + defaultOrderConstraint = new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")); + conclusion = new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex), new Variable("m")); + } + }, + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ) + ); + } + +} diff --git a/src/main/java/inference/axioms/DependencyExtension.java b/src/main/java/inference/axioms/DependencyExtension.java new file mode 100644 index 0000000..8e403e4 --- /dev/null +++ b/src/main/java/inference/axioms/DependencyExtension.java @@ -0,0 +1,85 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.InferenceRule; +import models.Position; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; +import utils.ExpressionUtils; + +public class DependencyExtension extends InferenceRule { + + public DependencyExtension() { + super("Dependency Extension"); + + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex), new Variable("n")); + } + }, + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ) + )); + + conclusion = new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex), ExpressionUtils.parse("n-1")); + } + }, + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex), new Variable("n")); + } + }, + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ) + ) + ); + } + + @Override + public Set derive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (this.assumptions.size() != assumptions.size()) { + return new HashSet<>(); + } + Set matchResult = assumptionMatch(assumptions, constraint); + + for (MatchConstraint res: matchResult) { + try { + res.getContext().put(new Position(List.of(0, 0)), (Integer) res.getContext().get(new Position())); + if (res.getContext().containsKey("j")) { + res.getContext().put(new Position(), (Integer) res.getContext().get("j") + 1); + } + res.getContext().put("maxDepth", 2); + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/UncurriedMapping.java b/src/main/java/inference/axioms/UncurriedMapping.java new file mode 100644 index 0000000..407f48e --- /dev/null +++ b/src/main/java/inference/axioms/UncurriedMapping.java @@ -0,0 +1,99 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.InferenceRule; +import models.Position; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDependencyTerm; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; +import utils.ExpressionUtils; + +public class UncurriedMapping extends InferenceRule{ + + public UncurriedMapping() { + super("Uncurried Mapping"); + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + int i = maxDepth - curDepth; + context.put("i", Math.max(i, (Integer) context.getOrDefault("i", 0))); + if (curDepth == maxDepth) { + if (curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")); + } else if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")); + } + curIndex -= 1; + } else if (curIndex == 0) { + return new MetaDynamicDependency(this); + } + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex), ExpressionUtils.parse("n-" + i)); + } + } + ) + )); + + conclusion = new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + int i = (Integer) context.get("i"); + if (curDepth == maxDepth - 1 && curIndex == 0) { + return new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i)) + ); + } else if (curIndex == 0) { + return new MetaDynamicDependency(this); + } if (curDepth == 1) { + if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i)); + } + curIndex -= 1; + } + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex), ExpressionUtils.parse("n-" + i)); + } + } + ) + ); + + } + + @Override + public Set derive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (this.assumptions.size() != assumptions.size()) { + return new HashSet<>(); + } + Set matchResult = assumptionMatch(assumptions, constraint); + + for (MatchConstraint res: matchResult) { + try { + int maxDepth = (Integer) res.getContext().get("maxDepth"); + res.getContext().put(new Position(), (Integer) res.getContext().get(new Position()) + 1); + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/test/java/inferencerule/DependencyAxiomTest.java b/src/test/java/inferencerule/DependencyAxiomTest.java index 2333d25..e262457 100644 --- a/src/test/java/inferencerule/DependencyAxiomTest.java +++ b/src/test/java/inferencerule/DependencyAxiomTest.java @@ -1,17 +1,21 @@ package inferencerule; import static org.junit.jupiter.api.Assertions.*; -import org.junit.jupiter.api.Test; - import java.util.List; import java.util.Set; +import org.junit.jupiter.api.Test; + import inference.ProofSystem; +import models.Position; import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; import models.formulas.Formula; +import models.terms.Dependency; +import models.terms.DependencyTerm; import models.terms.Resource; +import models.terms.ResourceConstant; import models.terms.meta.MatchConstraint; public class DependencyAxiomTest { @@ -24,9 +28,11 @@ Resource f = new Resource("f", 1); Resource g = new Resource("g", 1); Resource h = new Resource("h", 1); - Resource i = new Resource("i", 2); - Resource j = new Resource("j", 2); - Resource k = new Resource("k", 2); + Resource i = new Resource("i", 1); + Resource j = new Resource("j", 1); + Resource k = new Resource("k", 1); + Resource l = new Resource("l", 2); + Resource m = new Resource("m", 2); @Test void IdentityMappingTest() { @@ -43,25 +49,78 @@ } @Test + void ArgumentReductionTest() { + DependencyFormula d1 = new DependencyFormula(a, b, c); + DependencyFormula d2 = new DependencyFormula(d, a, b, c, e, f); + Set res = ProofSystem.argumentReduction.derive(List.of(d1, d2)); + assertTrue(res.contains(new DependencyFormula(d, b, c, e, f))); + } + + @Test + void ArgumentConstraintTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c, d, e, f, g, h, i); + EquationFormula eq1 = new EquationFormula(t1, new ResourceConstant("0")); + DependencyFormula d1 = new DependencyFormula(b, d, f); + Set res = ProofSystem.argumentConstraint.derive(List.of(eq1, d1)); + DependencyTerm t2 = new DependencyTerm(b, d, e, f, g); + assertTrue(res.contains(new EquationFormula(t2, c))); + } + + @Test void CompositeMappingTest() { + DependencyFormula d1 = new DependencyFormula(a, b, c, d); + DependencyFormula d2 = new DependencyFormula(e, a, f, g, h); + Set res = ProofSystem.compositeMapping.derive(List.of(d1, d2)); + assertTrue(res.contains(new DependencyFormula(e, b, c, d, f, g, h))); } @Test void ConstantMappingTest() { - //todo + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.getContext().put(new Position(), 3); + constraint.setBinding(new Variable("se"), a); + constraint.setBinding(new Variable("te0"), l); + constraint.setBinding(new Variable("te1"), m); + constraint.getContext().put("maxDepth", 1); + Set res = ProofSystem.constatnMapping.derive(List.of(), constraint); + assertTrue(res.contains(new DependencyFormula(a, l, m))); } @Test void UncurriedMappingTest() { + Resource a = new Resource("a", 4); + Resource b = new Resource("b", 4); + Resource d = new Resource("d", 3); + Resource e = new Resource("e", 3); + Resource f = new Resource("f", 3); + Resource g = new Resource("g", 3); + Resource h = new Resource("h", 2); + Resource i = new Resource("i", 2); + Resource x = new Resource("x", 2); + DependencyFormula d1 = new DependencyFormula(new Dependency(new Dependency(new Dependency(a, b), d, e, f, g), h, i)); + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.setBinding(new Variable("ve"), x); + Set res = ProofSystem.uncurriedMapping.derive(List.of(d1), constraint); + DependencyFormula d2 = new DependencyFormula(new Dependency(new Dependency(new DependencyTerm(a, b, x), d, e, f, g), h, i, x)); + assertTrue(res.contains(d2)); } @Test - void RedundantDependencyTest() { - //todo + void DependencyExtensionTest() { + Resource a = new Resource("a", 4); + Resource b = new Resource("b", 4); + Resource d = new Resource("d", 4); + Resource e = new Resource("e", 3); + Resource f = new Resource("f", 3); + DependencyFormula d1 = new DependencyFormula(a, b, d); + DependencyFormula d2 = new DependencyFormula(d1.getDependency(), e, f); + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.getContext().put("j", 2); + constraint.setBinding(new Variable("ue0"), e); + constraint.setBinding(new Variable("ue1"), f); + Set res = ProofSystem.dependencyExtension.derive(List.of(d1), constraint); + assertTrue(res.contains(d2)); } - @Test - void RedundancyEliminationTest() { - } }