SHARE
TWEET

Untitled

a guest Apr 20th, 2019 90 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. vector<string> Generator::step_generateMP() {
  2.     vector <string> deduc1;
  3.     deduc1.emplace_back("!B->(A->B)->!B");
  4.     deduc1.emplace_back("!B");
  5.     deduc1.emplace_back("(A->B)->!B");
  6.     deduc1.emplace_back("((A->B)->!B)->((A->B)->!!B)->!(A->B))");
  7.     deduc1.emplace_back("((A->B)->!!B)->!(A->B))");
  8.     vector <string> deduc;
  9.     deduc.emplace_back("(A->B)->(A->!B)->!A");
  10.     deduc.emplace_back("A->B");
  11.     deduc.emplace_back("(A->!B)->!A");
  12.     deduc.emplace_back("!B->(A->!B)");
  13.     deduc.emplace_back("!B");
  14.     deduc.emplace_back("A->!B");
  15.     deduc.emplace_back("!A");
  16.     deduction(deduc, "!B", "!A");
  17.     deduction(deduc, "A->B", "!B->!A");
  18.     vector<string> deduc2;
  19.     deduc2.emplace_back("((!B->!A)->(!B->!!A)->!!B)");
  20.     deduc2.emplace_back("(!B->!A)");
  21.     deduc2.emplace_back("((!B->!!A)->!!B)");
  22.     deduc2.emplace_back("(!!A->(!B->!!A))");
  23.     deduc2.emplace_back("(!!A)");
  24.     deduc2.emplace_back("(!B->!!A)");
  25.     deduc2.emplace_back("(!!B)");
  26.     deduction(deduc2, "!!A", "!!B");
  27.     deduction(deduc2, "(!B -> !A)", "(!!A->!!B)");
  28.     deduc.emplace_back("(A->B)");
  29.     deduc.emplace_back("(!B->!A)");
  30.     for (auto& st: deduc2) {
  31.         deduc.emplace_back(st);
  32.     }
  33.     deduc.emplace_back("(!!A->!!B)");
  34.     deduc.emplace_back("!!A");
  35.     deduc.emplace_back("!!B");
  36.     deduction(deduc, "A->B", "!!B");
  37.     for (auto& st: deduc) {
  38.         deduc1.emplace_back(st);
  39.     }
  40.     deduc1.emplace_back("!(A->B)");
  41.     deduction(deduc1, "!B", "!(A->B)");
  42.     vector<string> final_mp;
  43.     final_mp.emplace_back("!!(A->B)");
  44.     final_mp.emplace_back("!!A");
  45.     final_mp.emplace_back("((!(B)->(!(A->B)))->(!(B)->!!(A->B))->!!B)");
  46.     final_mp.emplace_back("(!!(A->B)->!B->!!(A->B))");
  47.     final_mp.emplace_back("!(B)->!(!(A->B))");
  48.     for (auto& st: deduc1) {
  49.         final_mp.emplace_back(st);
  50.     }
  51.     final_mp.emplace_back("(!(B)->!!(A->B))->!!B");
  52.     final_mp.emplace_back("!!B");
  53.     return final_mp;
  54. }
  55.  
  56. void Generator::deduction(vector<string> &proof, string A, string B) {
  57.     vector<string> ans;
  58.     ProofCherker checker;
  59.     ExpressionParser parser;
  60.     A = "(" + A + ")";
  61.     string strA = parser.parse(A)->toString();
  62.     vector<string> parsed;
  63.     parsed.reserve(proof.size());
  64.     for (int i = 0; i < proof.size(); i++) {
  65.         parsed.push_back(parser.parse(proof[i])->toString());
  66.     }
  67.     for (int i = 0; i < proof.size(); i++) {
  68.         if (parsed[i] == strA) {
  69.             string help3 = "((" + A + ")->(" + A + "))";
  70.             string help1 = "((" + A + ")->(" + help3 + "))";
  71.             string help2 = "((" + A + ")->((" + help3 + ")->(" + A + ")))";
  72.             ans.emplace_back("((" + A + ")->(" + help3 + "))");
  73.             ans.emplace_back("((" + help1 + ")->(" + help2 + ")->(" + help3 + "))");
  74.             ans.emplace_back("((" + help2 + ")->(" + help3 + "))");
  75.             ans.emplace_back(help2);
  76.             ans.emplace_back(help3);
  77.         } else {
  78.             bool flag = false;
  79.             for (int j = 0; j < i; j++) {
  80.                 string modus = "(" + parsed[j] + "->" + parsed[i] + ")";
  81.                 //modus = parser.parse(modus)->toString();
  82.                 for (int q = 0; q < i; q++) {
  83.                     if (modus == parsed[q]) {
  84.                         flag = true;
  85.                         string b;
  86.                         ans.emplace_back("(((" + A + ")->(" + parsed[j] + "))->(((" + A + ")->((" + parsed[j] + ")->(" + parsed[i] +
  87.                                          ")))->((" + A + ")->(" + parsed[i] + "))");
  88.                         ans.emplace_back("((((" + A + ")->((" + parsed[j] + ")->(" + parsed[i] + ")))->((" + A + ")->(" + parsed[i] + "))))");
  89.                         ans.emplace_back("((" + A + ")->(" + parsed[i] + "))");
  90.                         break;
  91.                     }
  92.                 }
  93.                 if (flag) break;
  94.             }
  95.             if (!flag) {
  96.                 string b;
  97.                 ans.emplace_back(parsed[i]);
  98.                 ans.emplace_back("((" + parsed[i] + ")->((" + A + ")->(" + parsed[i] + ")))");
  99.                 ans.emplace_back("((" + A + ")->(" + parsed[i] + "))");
  100.             }
  101.         }
  102.     }
  103.     proof = ans;
  104. }
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!
 
Top