]> matita.cs.unibo.it Git - logicplayer.git/blobdiff - mainActivity/src/com/example/furt/myapplication/RuleOrElimination.java
Ported to latest version of Android SDK
[logicplayer.git] / mainActivity / src / com / example / furt / myapplication / RuleOrElimination.java
diff --git a/mainActivity/src/com/example/furt/myapplication/RuleOrElimination.java b/mainActivity/src/com/example/furt/myapplication/RuleOrElimination.java
deleted file mode 100755 (executable)
index 75d1a77..0000000
+++ /dev/null
@@ -1,38 +0,0 @@
-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;
-    }
-}