]> matita.cs.unibo.it Git - logicplayer.git/blobdiff - mainActivity/app/src/main/java/com/example/furt/myapplication/RuleNotElimination.java
Ported to latest version of Android SDK
[logicplayer.git] / mainActivity / app / src / main / java / com / example / furt / myapplication / RuleNotElimination.java
diff --git a/mainActivity/app/src/main/java/com/example/furt/myapplication/RuleNotElimination.java b/mainActivity/app/src/main/java/com/example/furt/myapplication/RuleNotElimination.java
new file mode 100644 (file)
index 0000000..7c7aaca
--- /dev/null
@@ -0,0 +1,29 @@
+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;
+    }
+}
+