]> matita.cs.unibo.it Git - logicplayer.git/blobdiff - mainActivity/src/com/example/furt/myapplication/RuleImplElimination.java
Ported to latest version of Android SDK
[logicplayer.git] / mainActivity / src / com / example / furt / myapplication / RuleImplElimination.java
diff --git a/mainActivity/src/com/example/furt/myapplication/RuleImplElimination.java b/mainActivity/src/com/example/furt/myapplication/RuleImplElimination.java
deleted file mode 100755 (executable)
index f2fd1ff..0000000
+++ /dev/null
@@ -1,31 +0,0 @@
-package com.example.furt.myapplication;
-
-public class RuleImplElimination implements EliminationRule
-{
-    String ruleName;
-    FormulaImpl Fn;
-    RuleImplElimination(FormulaImpl F)
-    {
-        Fn=F;
-        ruleName="⇒e";
-    }
-    public Node createNodes(Formula F,askFormula ask)
-    {
-        Formula C;
-        if (F==null) {
-            C=ask.Ask();
-            if (!(C.toString().equals(Fn.rightF.toString())))
-                return null;
-        }
-        else
-            if (!(F.toString().equals(Fn.rightF.toString())))
-                return null;
-            Node elNode=new Node(Fn);
-            Node lNode=new Node(Fn.leftF);
-            Node bNode=new Node(Fn.rightF);
-            bNode.addChild(elNode);
-            bNode.addChild(lNode);
-            bNode.ruleName=ruleName;
-            return bNode;
-    }
-}