Ported to latest version of Android SDK

[logicplayer.git] / mainActivity / app / src / main / java / com / example / furt / myapplication / RuleOrElimination.java

diff --git a/mainActivity/app/src/main/java/com/example/furt/myapplication/RuleOrElimination.java b/mainActivity/app/src/main/java/com/example/furt/myapplication/RuleOrElimination.java
new file mode 100644 (file)
index 0000000..75d1a77
--- /dev/null
+++ b/mainActivity/app/src/main/java/com/example/furt/myapplication/RuleOrElimination.java
@@ -0,0 +1,38 @@
+package com.example.furt.myapplication;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class RuleOrElimination implements EliminationRule
+{
+    String ruleName;
+    FormulaOr Fn;
+    RuleOrElimination(FormulaOr F)
+    {
+        Fn=F;
+        ruleName="∨e";
+    }
+    public Node createNodes(Formula F,askFormula ask)
+    {
+        Formula C;
+        if (F==null)
+            C=ask.Ask();
+        else
+            C=F;
+            Node elNode=new Node(Fn);
+            Node c1Node=new Node(C);
+            Node c2Node=new Node(C);
+            List<Formula> HP1=new ArrayList<Formula>();
+            List<Formula> HP2=new ArrayList<Formula>();
+            HP1.add(Fn.leftF);
+            HP2.add(Fn.rightF);
+            c1Node.addHPFormula(HP1,true);
+            c2Node.addHPFormula(HP2,true);
+            Node rNode=new Node(C);
+            rNode.addChild(elNode);
+            rNode.addChild(c1Node);
+            rNode.addChild(c2Node);
+            rNode.ruleName=ruleName;
+            return rNode;
+    }
+}