+++ /dev/null
-package com.example.furt.myapplication;
-
-import android.graphics.Paint;
-
-import java.util.ArrayList;
-import java.util.List;
-
-public class FormulaNot extends GenericFormula implements Formula{
- Paint p=new Paint();
- Formula Operand;
- int priority;
- int argPriority;
- FormulaNot(Formula F)
- {
- Operand=F;
- priority=20;
- argPriority=100;
- }
- @Override
- public String Draw(int p)
- {
- if (priority >= p)
- return "¬"+Operand.Draw(20);
- else
- return("¬("+Operand.Draw(20)+")");
- }
-
- public List<IntroductionRule> introductionRules(){
- List<IntroductionRule> nodes=new ArrayList<IntroductionRule>();
-
- //Introduzione del not (NOTA: il not non eredita la regola di riduzione ad assurdo)
- RuleIntroduction notIntro=new RuleIntroduction("¬i",4);
- Node notN=new Node(new FormulaBOT());
- List<Formula> notHP=new ArrayList<Formula>();
- notHP.add(Operand);
- notN.addHPFormula(notHP,true);
- Node thisNode=new Node(this);
- thisNode.addChild(notN);
- notIntro.tempRule=thisNode;
- nodes.add(notIntro);
- return nodes;
- }
- public List<EliminationRule> EliminationRules()
- {
- List<EliminationRule> nodes=new ArrayList<EliminationRule>();
- nodes.add(new RuleNotElimination(this));
- return nodes;
- }
-
- @Override
- public boolean Fill(Formula Filler) {
- if(Operand.toString().equals("_")) {
- Operand = Filler;
- return true;
- }
- return Operand.Fill(Filler);
- }
-
- @Override
- public boolean setCursor() {
- return Operand.setCursor();
- }
-
- @Override
- public Formula duplicate() {
- return new FormulaNot(Operand.duplicate());
- }
-}