]> matita.cs.unibo.it Git - logicplayer.git/blobdiff - mainActivity/src/com/example/furt/myapplication/FormulaImpl.java
New version (to be tested).
[logicplayer.git] / mainActivity / src / com / example / furt / myapplication / FormulaImpl.java
index 9761a0e58384ce57322d9f7bf6e18e24415f20c8..efe17147ec0749845cb06cc68285372e3cf17212 100755 (executable)
@@ -28,7 +28,10 @@ public class FormulaImpl extends GenericFormula implements Formula
 
     public List<IntroductionRule> introductionRules(){
         List<IntroductionRule> nodes=new ArrayList<IntroductionRule>();
-        nodes.addAll(super.introductionRules());
+        nodes.addAll(super.introductionRules()); //aggiunge la regola di R.A.A.
+
+        //Regola di introduzione dell'implicazione
+
         RuleIntroduction implIntro=new RuleIntroduction("⇒i",10);
         Node ImplN=new Node(rightF);
         List<Formula> implHP=new ArrayList<Formula>();
@@ -38,6 +41,7 @@ public class FormulaImpl extends GenericFormula implements Formula
         thisNode.addChild(ImplN);
         implIntro.tempRule=thisNode;
         nodes.add(implIntro);
+
         return nodes;
     }
     public List<EliminationRule> EliminationRules()