diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index 78bb131..f13d1c7 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -57,17 +57,21 @@ } else { Set result = new HashSet<>(); for (List terms: Permutation.permutation(existTerms, missingVariables.size())) { - MatchConstraint constraint = MatchConstraint.createDefault(); + Set constraints = new HashSet<>(); + constraints.add(MatchConstraint.createDefault()); boolean flg = false; for (int i = 0; i < missingVariables.size(); i++) { - if (missingVariables.get(i).isMatchedBy(terms.get(i)).isEmpty()) { + constraints = missingVariables.get(i).isMatchedBy(terms.get(i), constraints); + if (constraints.isEmpty()) { flg = true; break; } - constraint.setBinding(missingVariables.get(i).getVariableName(), terms.get(i)); } if (flg) continue; - result.addAll(derive(assumptions, constraint)); + for (MatchConstraint constraint: constraints) { + if (defaultOrderConstraint != null && (! defaultOrderConstraint.check(constraint.getOrderConstraint()))) continue; + result.addAll(derive(assumptions, constraint)); + } } return result; } diff --git a/src/main/java/inference/ProofState.java b/src/main/java/inference/ProofState.java index 7531106..ba42b0b 100644 --- a/src/main/java/inference/ProofState.java +++ b/src/main/java/inference/ProofState.java @@ -162,6 +162,7 @@ } public void addHistory(List assumptions, InferenceRule usedAxiom, Formula conclusion) { + if (formulaExist(conclusion)) return; InferenceHistoryNode node = new InferenceHistoryNode(assumptions, usedAxiom, conclusion); this.history.addHistory(conclusion, node); } @@ -173,6 +174,15 @@ return result; } + public boolean formulaExist(Formula formula) { + if (formula instanceof EquationFormula eq) { + return this.equationFormulas.contains(eq); + } else if (formula instanceof DependencyFormula df) { + return this.dependencyFormulas.contains(df); + } + return false; + } + record ConclusionMatchedTerm(Set leftSideHands, Set rightSideHands) {}; } diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index d6dd188..cbb0d97 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -29,7 +29,9 @@ import models.terms.Dependency; import models.terms.EvaluatableTerm; import models.terms.RDLTerm; +import models.terms.Resource; import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.OrderConstraint; import utils.Product; public class ProofSystem { @@ -127,6 +129,16 @@ public static final InferenceRule constantMapping = new ConstantMapping(); + public static final InferenceRule constantMapping1 = new InferenceRule( + "Constant Mapping", + List.of(), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("m")) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) + ); + public static final InferenceRule uncurriedMapping = new UncurriedMapping(); public static final InferenceRule dependencyExtension = new DependencyExtension(); @@ -146,7 +158,7 @@ argumentExtension, argumentReduction, compositeMapping, - constantMapping, + constantMapping1, uncurriedMapping, dependencyExtension ); @@ -169,7 +181,7 @@ argumentExtension, argumentReduction, compositeMapping, - constantMapping, + constantMapping1, uncurriedMapping, dependencyExtension ); @@ -181,15 +193,24 @@ public ProofSystem(Set assumptions, Formula conclusion) { + this(assumptions, conclusion, Set.of()); + } + + public ProofSystem(Set assumptions, Formula conclusion, Set existResources) { state = new ProofState(assumptions); this.assumptions = assumptions; this.conclusion = conclusion; + state.getEvaluatableTerms().addAll(existResources); } public void inference() { } - public void dependencyInference() { + public String getInferenceHistoryString() { + return state.getHistory().getHistoryString(conclusion); + } + + public boolean dependencyInference() { if (conclusion instanceof EquationFormula eq) { RDLTerm lhs = eq.getLeftSideHand(); RDLTerm rhs = eq.getRightSideHand(); @@ -198,6 +219,7 @@ while((! state.getDependencies().contains(leftDependency)) && (! state.getDependencies().contains(rightDependency))) { state.addFormuals(dependencyInferenceStep()); } + return true; } else if (conclusion instanceof DependencyFormula dep) { while((! state.getDependencyFormulas().contains(dep))) { Set result = dependencyInferenceStep(); @@ -210,11 +232,13 @@ } } if (sizeConstraintOk.size() == 0) { - break; + return false; } state.addFormuals(sizeConstraintOk); } + return true; } + return false; } public Set dependencyInferenceStep() { @@ -224,16 +248,24 @@ for (Set formulas: state.getMatchedFormulas().get(rule)) { matchedFormulas.add(new ArrayList<>(formulas)); } - for (List formulas: Product.product(matchedFormulas)) { - Set results = rule.derive(formulas, state.getExistTerms()); - for (Formula res: results) { - state.addHistory(formulas, rule, res); + if (rule.getAssumptions().size() == 0) { + result.addAll(dependencyDerive(List.of(), rule)); + } else { + for (List formulas: Product.product(matchedFormulas)) { + result.addAll(dependencyDerive(formulas, rule)); } - for (Formula f: results) { - if (f instanceof DependencyFormula df) { - result.add(df); - } - } + } + } + return result; + } + + private Set dependencyDerive(List assumptions, InferenceRule rule) { + Set result = new HashSet<>(); + for (Formula res: rule.derive(assumptions, state.getExistTerms())) { + if (state.formulaExist(res)) continue; + state.addHistory(List.of(), rule, res); + if (res instanceof DependencyFormula df) { + result.add(df); } } return result; diff --git a/src/main/java/inference/axioms/ArgumentExtension.java b/src/main/java/inference/axioms/ArgumentExtension.java index a314ed1..15d88d1 100644 --- a/src/main/java/inference/axioms/ArgumentExtension.java +++ b/src/main/java/inference/axioms/ArgumentExtension.java @@ -46,6 +46,7 @@ new MetaEvaluatableTermVariable(new Variable("ue")) ) ); + this.missingVariables.add(new MetaEvaluatableTermVariable(new Variable("ue"))); } diff --git a/src/test/java/inference/DependencyInferenceTest.java b/src/test/java/inference/DependencyInferenceTest.java new file mode 100644 index 0000000..f4b03a3 --- /dev/null +++ b/src/test/java/inference/DependencyInferenceTest.java @@ -0,0 +1,101 @@ +package inference; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.Set; + +import org.junit.jupiter.api.Test; + +import models.formulas.DependencyFormula; +import models.formulas.EquationFormula; +import models.terms.Dependency; +import models.terms.DependencyTerm; +import models.terms.Resource; + +public class DependencyInferenceTest { + + 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", 2); + Resource g = new Resource("g", 2); + Resource h = new Resource("h", 3); + Resource i = new Resource("i", 3); + + @Test + void IdentityMappingInferenceTest() { + EquationFormula eq1 = new EquationFormula(a, b); + DependencyFormula d1 = new DependencyFormula(a, b); + ProofSystem ps = new ProofSystem(Set.of(eq1), d1); + assertTrue(ps.dependencyInference()); + } + + @Test + void ArgumentExtensionInferenceTest() { + DependencyFormula d1 = new DependencyFormula(a, b); + DependencyFormula d2 = new DependencyFormula(a, b, c); + DependencyFormula d3 = new DependencyFormula(a, b, c, d, e); + ProofSystem ps = new ProofSystem(Set.of(d1), d2); + assertFalse(ps.dependencyInference()); + ProofSystem ps2 = new ProofSystem(Set.of(d1), d2, Set.of(c)); + assertTrue(ps2.dependencyInference()); + ProofSystem ps3 = new ProofSystem(Set.of(d1), d3, Set.of(c, d, e)); + assertTrue(ps3.dependencyInference()); + } + + @Test + void ArgumentReductionInferenceTest() { + DependencyFormula d1 = new DependencyFormula(a, b, c); + DependencyFormula d2 = new DependencyFormula(b, c); + DependencyFormula d3 = new DependencyFormula(a, c); + ProofSystem ps = new ProofSystem(Set.of(d1, d2), d3); + assertTrue(ps.dependencyInference()); + + DependencyFormula d4 = new DependencyFormula(a, b, b); + EquationFormula eq1 = new EquationFormula(b, b); + DependencyFormula d5 = new DependencyFormula(a, b); + ProofSystem ps2 = new ProofSystem(Set.of(d4, eq1), d5); + assertTrue(ps2.dependencyInference()); + } + + @Test + void CompositeMappingInferenceTest() { + DependencyFormula d1 = new DependencyFormula(a, b); + DependencyFormula d2 = new DependencyFormula(b, c, d); + DependencyFormula d3 = new DependencyFormula(a, c, d); + ProofSystem ps = new ProofSystem(Set.of(d1, d2), d3); + assertTrue(ps.dependencyInference()); + } + + @Test + void ConstantMappingInferenceTest() { + DependencyFormula d1 = new DependencyFormula(a, f); + ProofSystem ps = new ProofSystem(Set.of(), d1, Set.of(a, f)); + assertTrue(ps.dependencyInference()); + + DependencyFormula d2 = new DependencyFormula(a, f, g); + ProofSystem ps2 = new ProofSystem(Set.of(), d2, Set.of(a, b, f, g)); + assertTrue(ps2.dependencyInference()); + } + + @Test + void UncurriedMappingInferenceTest() { + DependencyFormula d1 = new DependencyFormula(new Dependency(f, g), a); + DependencyFormula d2 = new DependencyFormula(new DependencyTerm(f, g, b), a, b); + ProofSystem ps = new ProofSystem(Set.of(d1), d2, Set.of(b)); + assertTrue(ps.dependencyInference()); + + DependencyFormula d3 = new DependencyFormula(new Dependency(new Dependency(h, i), f, g), a); + DependencyFormula d4 = new DependencyFormula(new Dependency(new DependencyTerm(h, i, b), f, g), a, b); + ProofSystem ps2 = new ProofSystem(Set.of(d3), d4, Set.of(b)); + assertTrue(ps2.dependencyInference()); + + DependencyFormula d5 = new DependencyFormula(new Dependency(new Dependency(h, i), f), a); + DependencyFormula d6 = new DependencyFormula(new Dependency(new DependencyTerm(h, i, g), f, g), a); + ProofSystem ps3 = new ProofSystem(Set.of(d5), d6, Set.of(g)); + assertTrue(ps3.dependencyInference()); + } + +} diff --git a/src/test/java/inference/inferencerule/DependencyAxiomTest.java b/src/test/java/inference/inferencerule/DependencyAxiomTest.java index 61494eb..759d5ab 100644 --- a/src/test/java/inference/inferencerule/DependencyAxiomTest.java +++ b/src/test/java/inference/inferencerule/DependencyAxiomTest.java @@ -87,6 +87,14 @@ } @Test + void ConstantMapping1Test() { + Set res = ProofSystem.constantMapping1.derive(List.of(), Set.of(a, m)); + assertTrue(res.contains(new DependencyFormula(a, m))); + Set res2 = ProofSystem.constantMapping1.derive(List.of(), Set.of(a, b)); + assertFalse(res2.contains(new DependencyFormula(a, b))); + } + + @Test void UncurriedMappingTest() { Resource a = new Resource("a", 4); Resource b = new Resource("b", 4);