diff --git a/src/main/java/inference/EquationAxiom.java b/src/main/java/inference/EquationAxiom.java index 91a2bab..0959493 100644 --- a/src/main/java/inference/EquationAxiom.java +++ b/src/main/java/inference/EquationAxiom.java @@ -78,19 +78,6 @@ return result; } - protected Set assumptionMatch(Listassumptions, MatchConstraint constraint) { - Set matchResult = new HashSet<>(); - matchResult.add(constraint); - for (int i = 0; i < assumptions.size(); i++) { - Formula assumption = assumptions.get(i); - MetaFormula metaAssumption = this.assumptions.get(i); - matchResult = metaAssumption.isMatchedBy(assumption, matchResult); - if (matchResult.isEmpty()) { - return new HashSet<>(); - } - } - return matchResult; - } protected Set conclusionLeftSideHandMatch(EvaluatableTerm term, Set matchResult) { MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index ffe0934..97e0056 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -1,11 +1,15 @@ package inference; import java.util.ArrayList; +import java.util.HashSet; import java.util.List; import java.util.Set; +import exceptions.SubstituteFailedException; import lombok.Getter; +import models.formulas.Formula; import models.formulas.meta.MetaFormula; +import models.terms.meta.MatchConstraint; import models.terms.meta.MetaVariable; public class InferenceRule { @@ -41,6 +45,41 @@ this(name, assumptions, conclusion, null); } + public Set derive(List assumptions) { + return derive(assumptions, MatchConstraint.createDefault()); + } + + 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 { + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + + protected Set assumptionMatch(Listassumptions, MatchConstraint constraint) { + Set matchResult = new HashSet<>(); + matchResult.add(constraint); + for (int i = 0; i < assumptions.size(); i++) { + Formula assumption = assumptions.get(i); + MetaFormula metaAssumption = this.assumptions.get(i); + matchResult = metaAssumption.isMatchedBy(assumption, matchResult); + if (matchResult.isEmpty()) { + return new HashSet<>(); + } + } + return matchResult; + } + // public Set apply(Set formulas, Set existTerms) { // List> matchFormulas = new ArrayList<>(); // List> matchTerms = new ArrayList<>(); diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 8f6caf8..cf776c8 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -4,6 +4,7 @@ import java.util.List; import java.util.Set; +import inference.axioms.ArgumentExtension; import inference.axioms.Constantness; import inference.axioms.Identity; import inference.axioms.LeftSubstitution; @@ -15,6 +16,7 @@ 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.RDLTerm; import models.terms.meta.MetaEvaluatableTermVariable; @@ -90,24 +92,21 @@ // //======================Dependency Axioms============================= // -// public static final InferenceRule identityMapping = new InferenceRule( -// "Identity Mapping", -// List.of( -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaEvaluatableTermVariable(new Variable("se")) -// ) -// ), -// List.of(), -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaEvaluatableTermVariable(new Variable("se")) -// ), -// null, -// null, -// null, -// null -// ); + public static final InferenceRule identityMapping = new InferenceRule( + "Identity Mapping", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("se")) + ) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("se")) + ) + ); + + public static final InferenceRule argumentExtension = new ArgumentExtension(); // public static final InferenceRule compositeMapping = new CompositeMapping(); diff --git a/src/main/java/inference/axioms/ArgumentExtension.java b/src/main/java/inference/axioms/ArgumentExtension.java new file mode 100644 index 0000000..a314ed1 --- /dev/null +++ b/src/main/java/inference/axioms/ArgumentExtension.java @@ -0,0 +1,70 @@ +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 ArgumentExtension extends InferenceRule { + + public ArgumentExtension() { + super("Argument 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 MetaEvaluatableTermVariable(new Variable("se")) + ) + )); + + conclusion = 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("te" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ); + } + + + 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/test/java/inferencerule/DependencyAxiomTest.java b/src/test/java/inferencerule/DependencyAxiomTest.java index 19b756c..2333d25 100644 --- a/src/test/java/inferencerule/DependencyAxiomTest.java +++ b/src/test/java/inferencerule/DependencyAxiomTest.java @@ -3,15 +3,16 @@ import org.junit.jupiter.api.Test; +import java.util.List; import java.util.Set; import inference.ProofSystem; +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.meta.MatchConstraint; public class DependencyAxiomTest { @@ -29,17 +30,20 @@ @Test void IdentityMappingTest() { - Set res = ProofSystem.identityMapping.apply(new EquationFormula(a, b)); + Set res = ProofSystem.identityMapping.derive(List.of(new EquationFormula(a, b))); assertTrue(res.contains(new DependencyFormula(a, b))); } @Test + void ArgumentExtensionTest() { + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.setBinding(new Variable("ue"), d); + Set res = ProofSystem.argumentExtension.derive(List.of(new DependencyFormula(a, b, c)), constraint); + assertTrue(res.contains(new DependencyFormula(a, b, c, d))); + } + + @Test void CompositeMappingTest() { - Set res = ProofSystem.compositeMapping.apply(new DependencyFormula(a, b), new DependencyFormula(b, c)); - assertTrue(res.contains(new DependencyFormula(a, c))); - - res = ProofSystem.compositeMapping.apply(new DependencyFormula(a, b, c), new DependencyFormula(c, d, e, f)); - assertTrue(res.contains(new DependencyFormula(a, b, d, e, f))); } @Test @@ -49,35 +53,6 @@ @Test void UncurriedMappingTest() { - Set res = ProofSystem.uncurriedMapping.apply( - new DependencyFormula(new Dependency(i, j), a), - new EquationFormula(new DependencyTerm(j, h, c), b) - ); - assertTrue(res.contains(new DependencyFormula(new DependencyTerm(i, j, b), a, b))); - - Resource a4 = new Resource("a4", 4); - Resource b4 = new Resource("b4", 4); - Resource x= new Resource("y", 4); - Resource y = new Resource("x", 4); - Resource a3 = new Resource("a3", 3); - Resource a2 = new Resource("a2", 2); - Resource a1 = new Resource("a1", 1); - Resource c2 = new Resource("c2", 2); - - Dependency d4 = new Dependency(b4, a4); - Dependency d3 = new Dependency(d4, a3); - Dependency d2 = new Dependency(d3, a2); - Dependency d1 = new Dependency(d2, a1); - - res = ProofSystem.uncurriedMapping.apply( - new DependencyFormula(d1), - new EquationFormula(new DependencyTerm(a4, x, y), c2) - ); - DependencyTerm t1 = new DependencyTerm(b4, a4, c2); - Dependency d33 = new Dependency(t1, a3); - Dependency d22 = new Dependency(d33, a2, c2); - Dependency d11 = new Dependency(d22, a1); - assertTrue(res.contains(new DependencyFormula(d11))); } @Test @@ -87,11 +62,6 @@ @Test void RedundancyEliminationTest() { - Set result = ProofSystem.redundancyElimination.apply(new DependencyFormula(a, b), new DependencyFormula(c, a, b, d)); - assertTrue(result.contains(new DependencyFormula(c, a, d))); - - result = ProofSystem.redundancyElimination.apply(new DependencyFormula(a, b, c, d), new DependencyFormula(c, a, b, c, d, e, f, g)); - assertTrue(result.contains(new DependencyFormula(c, a, e, f, g))); } } diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java index 8e083ef..91955f8 100644 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -8,6 +8,7 @@ import java.util.Set; import inference.ProofSystem; +import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; import models.terms.Dependency; @@ -15,6 +16,7 @@ import models.terms.EvaluatableTerm; import models.terms.RDLTerm; import models.terms.Resource; +import models.terms.meta.MatchConstraint; public class EqualityAxiomTest { @@ -124,8 +126,10 @@ DependencyFormula d1 = new DependencyFormula(new Dependency(new Dependency(o, p, q), n, m), a, b, c); DependencyTerm dt1 = new DependencyTerm(new DependencyTerm(new DependencyTerm(o, p, d, q, e), n, f, m ,g), a, h, b, i, c, j); DependencyTerm dt2 = new DependencyTerm(new DependencyTerm(new DependencyTerm(o, p, k, q, e), n, f, m ,g), a, h, b, i, c, j, k, d); - Set terms = ProofSystem.uncurrying.apply(List.of(d1), dt1); -// assertTrue(terms.contains(dt2)); + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.setBinding(new Variable("ve"), k); + Set terms = ProofSystem.uncurrying.apply(List.of(d1), dt1, constraint); + assertTrue(terms.contains(dt2)); terms = ProofSystem.uncurrying.apply(List.of(d1), dt2); assertTrue(terms.contains(dt1)); }