]> matita.cs.unibo.it Git - logicplayer.git/blobdiff - mainActivity/src/com/example/furt/myapplication/RuleNotElimination.java
Ported to latest version of Android SDK
[logicplayer.git] / mainActivity / src / com / example / furt / myapplication / RuleNotElimination.java
diff --git a/mainActivity/src/com/example/furt/myapplication/RuleNotElimination.java b/mainActivity/src/com/example/furt/myapplication/RuleNotElimination.java
deleted file mode 100755 (executable)
index 7c7aaca..0000000
+++ /dev/null
@@ -1,29 +0,0 @@
-package com.example.furt.myapplication;
-
-public class RuleNotElimination implements EliminationRule
-{
-    String ruleName;
-    FormulaNot Fn;
-    RuleNotElimination(FormulaNot F)
-    {
-        Fn=F;
-        ruleName="¬e";
-    }
-    public Node createNodes(Formula F,askFormula ask)
-    {
-        Formula C=ask.Ask();
-        if ((C.toString().equals("⊥"))&&(F==null ||F==Fn.Operand)) //top-down con nodo attuale bottom o bottom-up con nodi attuali Fn e !Fn
-        {
-            Node elNode=new Node(Fn);
-            Node cNode=new Node(Fn.Operand);
-            Node rNode=new Node(C);
-            rNode.addChild(elNode);
-            rNode.addChild(cNode);
-            rNode.ruleName=ruleName;
-            return rNode;
-        }
-        else
-            return null;
-    }
-}
-