diff --git a/src/Main.java b/src/Main.java index 37bea9c..72f2f12 100644 --- a/src/Main.java +++ b/src/Main.java @@ -82,13 +82,16 @@ DependencyFormula f1 = new DependencyFormula(d1); InFormula f2 = new InFormula(t2, t3); EquationFormula f3 = new EquationFormula(t4, C); + DependencyFormula f4 = new DependencyFormula(new Dependency(new SetEvaluatableTerm(followee), aid)); + InFormula f5 = new InFormula(A, new SetEvaluatableTerm(aid)); InFormula conclusion = new InFormula(C, new SetEvaluatableTerm(new SetEvaluatableTerm(followee))); System.out.println(f1); System.out.println(f2); System.out.println(f3); System.out.println(conclusion); - boolean result = ProofSystem.check(List.of(f1, f2, f3), conclusion); + System.out.println(); + boolean result = ProofSystem.check(List.of(f1, f2, f3, f4, f5), conclusion); System.out.println(result); } diff --git a/src/inference/InferenceRule.java b/src/inference/InferenceRule.java index ccbdd84..3a369f6 100644 --- a/src/inference/InferenceRule.java +++ b/src/inference/InferenceRule.java @@ -176,4 +176,18 @@ return sb.toString(); } + @Override + public boolean equals(Object another) { + if (! (another instanceof InferenceRule)) { + return false; + } + InferenceRule anotherRule = (InferenceRule) another; + return getName().equals(anotherRule.getName()); + } + + @Override + public int hashCode() { + return getName().hashCode(); + } + } diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java index be922d1..261f200 100644 --- a/src/inference/ProofSystem.java +++ b/src/inference/ProofSystem.java @@ -8,7 +8,9 @@ import java.util.HashSet; import java.util.List; import java.util.Map; +import java.util.Queue; import java.util.Set; +import java.util.stream.Collectors; import models.algebra.Variable; import models.formulas.EquationFormula; @@ -258,10 +260,36 @@ ) ) ); + + private static final InferenceRule codomainMembership2 = new InferenceRule( + "Codomain Membership2", + List.of( + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r1")) + ), + new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("t1")), + new MetaRDLTerm( + new MetaResourceVariable(new Variable("r1")) + ) + ) + ), + new MetaInFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("r1")), + new MetaEvaluatableTermVariable(new Variable("t1")) + ), + new MetaRDLTerm( + new MetaResourceVariable(new Variable("se")) + ) + ) + ); private static final List axioms = List.of( reflexivity, - symmetry, +// symmetry, transitivity, rightSubstitution, leftSubstitution, @@ -269,7 +297,8 @@ mapComposition, memberSubstitution, membershipChain, - codomainMembership + codomainMembership, + codomainMembership2 ); public static void debug() { @@ -279,20 +308,22 @@ } } + record AxiomResult(InferenceRule axiom, List formulas) {} public static boolean check(Collection assumptions, Formula conclusion) { -// if (equationTransitionCheck(assumptions, conclusion)) { -// return true; -// } + + Map proofGraph = new HashMap<>(); + Map>> appliedFormulas = new HashMap<>(); + for (InferenceRule axiom : axioms) { + appliedFormulas.put(axiom, new HashSet<>()); + } Set appearFormulas = new HashSet<>(assumptions); int prevAppearFormulasSize = appearFormulas.size(); while (! appearFormulas.contains(conclusion)) { Set derivedFormulas = new HashSet<>(); - System.out.println("========================================="); - System.out.println(appearFormulas); for(InferenceRule axiom : axioms) { - derivedFormulas.addAll(applyAxiom(axiom, appearFormulas)); + derivedFormulas.addAll(applyAxiom(axiom, appearFormulas, appliedFormulas.get(axiom), proofGraph)); } if (derivedFormulas.size() == 0) { return false; @@ -304,10 +335,52 @@ prevAppearFormulasSize = appearFormulas.size(); } + Queue formulaQueue = new ArrayDeque<>(); + Queue depthQueue = new ArrayDeque<>(); + List formulaResult = new ArrayList<>(); + List depthResult = new ArrayList<>(); + Map> usedAxioms = new HashMap<>(); + + formulaQueue.add(conclusion); + depthQueue.add(0); + + while (formulaQueue.size() != 0) { + Formula currentFormula = formulaQueue.poll(); + int currentDepth = depthQueue.poll(); + formulaResult.add(currentFormula); + depthResult.add(currentDepth); + if (! proofGraph.containsKey(currentFormula)) continue; + for (Formula nextFormula : proofGraph.get(currentFormula).formulas) { + formulaQueue.add(nextFormula); + depthQueue.add(currentDepth + 1); + if (! usedAxioms.containsKey(currentDepth + 1)) { + usedAxioms.put(currentDepth + 1, new HashSet<>()); + } + usedAxioms.get(currentDepth + 1).add(proofGraph.get(currentFormula).axiom); + } + } + int prevDepth = depthResult.get(depthResult.size() - 1); + List sameDepthFormulas = new ArrayList<>(); + for (int i = formulaResult.size() - 1; i >= 0; i--) { + int currentDepth = depthResult.get(i); + Formula currentFormula = formulaResult.get(i); + if (currentDepth != prevDepth) { + String out = sameDepthFormulas.stream().map(String::valueOf).collect(Collectors.joining(", ")); + String axioms = usedAxioms.get(prevDepth).stream().map(InferenceRule::getName).collect(Collectors.joining(", ")); + System.out.println(out); + System.out.println("==============================================================(" + axioms + ")"); + sameDepthFormulas.clear(); + } + prevDepth = currentDepth; + sameDepthFormulas.add(currentFormula); + + } + String out = sameDepthFormulas.stream().map(String::valueOf).collect(Collectors.joining(",")); + System.out.println(out); return true; } - private static Set applyAxiom(InferenceRule axiom, Set formulas) { + private static Set applyAxiom(InferenceRule axiom, Set formulas, Set> appliedFormulas, Map proofGraph) { Set result = new HashSet<>(); List> matchedFormulas = new ArrayList<>(); for (int i = 0; i < axiom.getAssumptionSize(); i++) { @@ -319,11 +392,13 @@ } } for(List applyFormulas : Product.product(matchedFormulas)) { - result.add(axiom.apply(applyFormulas)); - } - if (result.size() != 0) { - System.out.println(axiom.getName()); - System.out.println(result); + if (appliedFormulas.contains(applyFormulas)) continue; + Formula applied = axiom.apply(applyFormulas); + if (applied != null) { + result.add(axiom.apply(applyFormulas)); + appliedFormulas.add(applyFormulas); + proofGraph.put(applied, new AxiomResult(axiom, applyFormulas)); + } } return result; } diff --git a/src/tests/terms/meta/MetaEvaluatableTermVariableTest.java b/src/tests/terms/meta/MetaEvaluatableTermVariableTest.java new file mode 100644 index 0000000..7f527c2 --- /dev/null +++ b/src/tests/terms/meta/MetaEvaluatableTermVariableTest.java @@ -0,0 +1,31 @@ +package tests.terms.meta; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.Test; + +import models.algebra.Variable; +import models.terms.DependencyTerm; +import models.terms.ResourceConstant; +import models.terms.ResourceVariable; +import models.terms.meta.MetaEvaluatableTermVariable; +import tests.Utils; + +public class MetaEvaluatableTermVariableTest { + + @Test + void isMatchedByTest() { + MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se")); + + ResourceVariable a = new ResourceVariable("a", Utils.INT, 1); + ResourceVariable b = new ResourceVariable("b", Utils.INT, 1); + ResourceVariable c = new ResourceVariable("c", Utils.INT, 1); + ResourceConstant one = new ResourceConstant("1"); + DependencyTerm t1 = new DependencyTerm(a, b, c); + + assertTrue(se.isMatchedBy(a)); + assertTrue(se.isMatchedBy(one)); + assertTrue(se.isMatchedBy(t1)); + } + +}