proofs_propositional/search_ann.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "try:\n",
    "  import sys\n",
    "  sys.path.append('../')\n",
    "  from modules.search_prop import *\n",
    "except ImportError:\n",
    "  url = 'https://raw.githubusercontent.com/jhjeong314/Proofmood/main/modules'\n",
    "  import httpimport\n",
    "  with httpimport.remote_repo(url):\n",
    "    from search_prop import *"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This script `search_ann.ipynb` handles all 14 propositional inference rules, including:\n",
    "\n",
    "- LEM\n",
    "- Repeat\n",
    "- 6 introduction rules\n",
    "- 6 elimination rules\n",
    "\n",
    "As implied by the name `search_ann.ipynb,` each cell in this Jupyter notebook serves the following purposes:\n",
    "\n",
    "- When supplied with a proof text, it accurately annotates any lines that lack proper annotations within the conclusion formulas, assuming the requisite formulas or subproofs already exist.\n",
    "- Hypotheses, comments, and blank lines remain unaltered.\n",
    "- This process does not involve the creation or deletion of formulas or subproofs.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "│1. B or A\t .hyp\n",
      "│2. A imp B\t .hyp\n",
      "├─\n",
      "│3. (C imp D) or not (C imp D)\t\u001b[91mx\u001b[39m \n",
      "│4. B or A\t\u001b[91mx\u001b[39m \n",
      "\n",
      "(('4', [0, 3]), <Connective.OR: 'or'>)\n"
     ]
    }
   ],
   "source": [
    "# 'LEM' and 'repeat' rule example.\n",
    "\n",
    "prf_str = '''\n",
    "1. B or A  .hyp\n",
    "2. A imp B .hyp\n",
    "proves\n",
    "3. (C imp D) or not (C imp D)\n",
    "4. B or A\n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "\n",
    "proof.show_fitch_text()\n",
    "print()\n",
    "# Look for the last formula to validate. Among all invalidated formulas,\n",
    "#   we will first try to validate the last one.\n",
    "# We want the position of the node and also the principal connective if\n",
    "#   the formula is non-prime.\n",
    "print(ret_val := proof.fmla_to_validate())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "<class 'list'>\n",
      "[0, 3]\n",
      "<class 'str'>\n",
      "4\n",
      "<enum 'Connective'>\n",
      "Connective.OR\n"
     ]
    }
   ],
   "source": [
    "# Delve into the return value of fmla_to_validate().\n",
    "((conc_ln, conc_index), p_conn) = ret_val\n",
    "print(type(conc_index))\n",
    "print(conc_index)\n",
    "print(type(conc_ln))\n",
    "print(conc_ln)\n",
    "print(type(p_conn))\n",
    "print(p_conn)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'LEM' rule for line 4 failed.\n",
      "│1. B or A\t .hyp\n",
      "│2. A imp B\t .hyp\n",
      "├─\n",
      "│3. (C imp D) or not (C imp D)\t\u001b[91mx\u001b[39m \n",
      "│4. B or A\t\u001b[91mx\u001b[39m \n",
      "\n"
     ]
    }
   ],
   "source": [
    "# Try 'LEM' rule first.\n",
    "ans = proof.try_LEM(ret_val, verbosity=2)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'repeat' rule successfully applied to line 4.\n",
      "│1. B or A\t .hyp\n",
      "│2. A imp B\t .hyp\n",
      "├─\n",
      "│3. (C imp D) or not (C imp D)\t\u001b[91mx\u001b[39m \n",
      "│4. B or A\t\u001b[92m✓\u001b[39m repeat 1\n",
      "\n"
     ]
    }
   ],
   "source": [
    "# Next try the 'repeat' rule.\n",
    "ans = proof.try_repeat(ret_val, verbosity=2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(('3', [0, 2]), <Connective.OR: 'or'>)\n"
     ]
    }
   ],
   "source": [
    "print(ret_val := proof.fmla_to_validate())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'LEM' rule successfully applied to line 3.\n"
     ]
    }
   ],
   "source": [
    "# Try 'LEM' rule first, again.\n",
    "ans = proof.try_LEM(ret_val, verbosity=1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'repeat' rule successfully applied to line 4.\n",
      "'LEM' rule successfully applied to line 3.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. B and A\t .hyp\n",
      "│2. A imp B\t .hyp\n",
      "├─\n",
      "│3. (C imp D) or not (C imp D)\t\u001b[92m✓\u001b[39m LEM \n",
      "│4. B and A\t\u001b[92m✓\u001b[39m repeat 1\n"
     ]
    }
   ],
   "source": [
    "# Use proof.search_proof() to automate above.\n",
    "\n",
    "prf_str = '''\n",
    "1. B and A  .hyp\n",
    "2. A imp B .hyp\n",
    "proves\n",
    "3. (C imp D) or not (C imp D)\n",
    "4. B and A\n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Within the context of premises, a subproof with the hypothesis $\\alpha$ and the last conclusion $\\beta$ can be thought of as equivalent to the formula $\\alpha \\to \\beta$.\n",
    "\n",
    "This equivalence is especially convenient in the following 3 rules:\n",
    "* or elim\n",
    "* imp elim\n",
    "* iff intro\n",
    "\n",
    "From this point forward, for instance, the following validation is a legitimate application of the 'or elim' rule:\n",
    "\n",
    ">  {A imp C, B proves C, A or B} \\proves C\n",
    "\n",
    "We updated the code to reflect this change accordingly. (in `Ann.parse()`)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'repeat' rule for line 4 failed.\n",
      "'bot intro' rule successfully applied to line 4.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. not A\t .hyp\n",
      "│├─\n",
      "│││3. A\t .hyp\n",
      "││├─\n",
      "│││4. bot\t\u001b[92m✓\u001b[39m bot intro 2,3\n",
      "│││5. B\t\u001b[92m✓\u001b[39m bot elim 4\n",
      "││6. A imp B\t\u001b[92m✓\u001b[39m imp intro 3-5\n",
      "│7. not A imp A imp B\t\u001b[92m✓\u001b[39m imp intro 2-6\n"
     ]
    }
   ],
   "source": [
    "# bot intro (line 4)\n",
    "\n",
    "# The annotation of line 4 is not blank. \n",
    "# Wrong annotation occupies there.\n",
    "# We fix the wrong annotation of line 4\n",
    "\n",
    "prf_str = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  2. not A .hyp\n",
    "  proves\n",
    "    3. A .hyp\n",
    "    proves\n",
    "    4. bot .imp elim 1,2\n",
    "    5. B .bot elim 4\n",
    "  6. A imp B .imp intro 3-5\n",
    "7. not A imp (A imp B) .imp intro 2-6\n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(verbosity=1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'repeat' rule for line 7 failed.\n",
      "'not intro' rule successfully applied to line 7.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. # comment line takes up a line\n",
      "││3. not (A or not A)\t .hyp\n",
      "│├─\n",
      "│││4. A\t .hyp\n",
      "││├─\n",
      "│││5. A or not A\t\u001b[92m✓\u001b[39m or intro 4\n",
      "│││6. bot\t\u001b[92m✓\u001b[39m bot intro 5,3\n",
      "││7. not A\t\u001b[92m✓\u001b[39m not intro 4-6\n",
      "││8. A or not A\t\u001b[92m✓\u001b[39m or intro 7\n",
      "││9. bot\t\u001b[92m✓\u001b[39m bot intro 8,3\n",
      "│10. A or not A\t\u001b[92m✓\u001b[39m not elim 2-9\n"
     ]
    }
   ],
   "source": [
    "# not intro (line 7)\n",
    "\n",
    "prf_str = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  # comment line takes up a line\n",
    "  3. not(A or not A) .hyp\n",
    "  proves\n",
    "    4. A .hyp\n",
    "    proves\n",
    "    5. A or not A .or intro 4\n",
    "    6. bot .bot intro 5,3\n",
    "  7. not A .bot elim 6\n",
    "  8. A or not A .or intro 7\n",
    "  9. bot .bot intro 8,3\n",
    "10. A or not A .not elim 2-9\n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'repeat' rule for line 6 failed.\n",
      "'imp intro' rule successfully applied to line 6.\n",
      "'LEM' rule for line 5 failed.\n",
      "'repeat' rule for line 5 failed.\n",
      "'or intro' rule successfully applied to line 5.\n",
      "'repeat' rule for line 4 failed.\n",
      "'and intro' rule successfully applied to line 4.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. A\t .hyp\n",
      "│2. B\t .hyp\n",
      "├─\n",
      "││3. C\t .hyp\n",
      "│├─\n",
      "││4. A and B\t\u001b[92m✓\u001b[39m and intro 1,2\n",
      "││5. (A and B) or C\t\u001b[92m✓\u001b[39m or intro 4\n",
      "│6. C imp (A and B) or C\t\u001b[92m✓\u001b[39m imp intro 3-5\n"
     ]
    }
   ],
   "source": [
    "# and intro (line 4)\n",
    "# or intro (line 5)\n",
    "# imp intro (line 6)\n",
    "\n",
    "prf_str = '''\n",
    "A .hyp\n",
    "B .hyp\n",
    "proves\n",
    "  C .hyp\n",
    "  proves\n",
    "  4. A and B\n",
    "  5. (A and B) or C\n",
    "6. C imp (A and B) or C\n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'repeat' rule for line 5 failed.\n",
      "'iff intro' rule successfully applied to line 5.\n",
      "'repeat' rule successfully applied to line 4.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. A\t .hyp\n",
      "│2. A imp B\t .hyp\n",
      "├─\n",
      "││3. B\t .hyp\n",
      "│├─\n",
      "││4. A\t\u001b[92m✓\u001b[39m repeat 1\n",
      "│5. A iff B\t\u001b[92m✓\u001b[39m iff intro 2,3-4\n"
     ]
    }
   ],
   "source": [
    "# iff intro (line 4)\n",
    "\n",
    "prf_str = '''\n",
    "A .hyp\n",
    "A imp B .hyp\n",
    "proves\n",
    "  B .hyp\n",
    "  proves\n",
    "  A\n",
    "A iff B\n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'repeat' rule for line 5 failed.\n",
      "'imp intro' rule successfully applied to line 5.\n",
      "'repeat' rule for line 4 failed.\n",
      "'bot elim' rule successfully applied to line 4.\n",
      "'repeat' rule for line 3 failed.\n",
      "'bot intro' rule successfully applied to line 3.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. A\t .hyp\n",
      "├─\n",
      "││2. not A\t .hyp\n",
      "│├─\n",
      "││3. bot\t\u001b[92m✓\u001b[39m bot intro 1,2\n",
      "││4. B\t\u001b[92m✓\u001b[39m bot elim 3\n",
      "│5. not A imp B\t\u001b[92m✓\u001b[39m imp intro 2-4\n"
     ]
    }
   ],
   "source": [
    "# bot elim (line 4)\n",
    "\n",
    "prf_str = '''\n",
    "A .hyp\n",
    "proves\n",
    "  not A .hyp\n",
    "  proves\n",
    "  bot\n",
    "  B\n",
    "not A imp B\n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'repeat' rule for line 9 failed.\n",
      "'imp intro' rule successfully applied to line 9.\n",
      "'repeat' rule for line 8 failed.\n",
      "'imp intro' rule successfully applied to line 8.\n",
      "'repeat' rule for line 7 failed.\n",
      "'bot elim' rule for line 7 failed.\n",
      "'not elim' rule successfully applied to line 7.\n",
      "'repeat' rule for line 6 failed.\n",
      "'bot intro' rule successfully applied to line 6.\n",
      "'repeat' rule for line 5 failed.\n",
      "'not intro' rule for line 5 failed.\n",
      "'bot elim' rule for line 5 failed.\n",
      "'not elim' rule for line 5 failed.\n",
      "'imp elim' rule successfully applied to line 5.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. \t .hyp\n",
      "├─\n",
      "││2. not B imp not A\t .hyp\n",
      "│├─\n",
      "│││3. A\t .hyp\n",
      "││├─\n",
      "││││4. not B\t .hyp\n",
      "│││├─\n",
      "││││5. not A\t\u001b[92m✓\u001b[39m imp elim 2,4\n",
      "││││6. bot\t\u001b[92m✓\u001b[39m bot intro 3,5\n",
      "│││7. B\t\u001b[92m✓\u001b[39m not elim 4-6\n",
      "││8. A imp B\t\u001b[92m✓\u001b[39m imp intro 3-7\n",
      "│9. (not B imp not A) imp A imp B\t\u001b[92m✓\u001b[39m imp intro 2-8\n"
     ]
    }
   ],
   "source": [
    "# not elim (line 7)\n",
    "# imp elim (line 5)\n",
    "\n",
    "prf_str = '''\n",
    "1. .hyp\n",
    "proves\n",
    "  2. not B imp not A .hyp\n",
    "  proves\n",
    "    3. A .hyp\n",
    "    proves\n",
    "      4. not B .hyp\n",
    "      proves\n",
    "      5. not A \n",
    "      6. bot \n",
    "    7. B\n",
    "  8. A imp B \n",
    "9. (not B imp not A) imp (A imp B) \n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'repeat' rule for line 2 failed.\n",
      "'bot elim' rule for line 2 failed.\n",
      "'not elim' rule for line 2 failed.\n",
      "'imp elim' rule for line 2 failed.\n",
      "'iff elim' rule for line 2 failed.\n",
      "'and elim' rule successfully applied to line 2.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. A and B\t .hyp\n",
      "├─\n",
      "│2. B\t\u001b[92m✓\u001b[39m and elim 1\n"
     ]
    }
   ],
   "source": [
    "# and elim (line 2)\n",
    "\n",
    "prf_str = '''\n",
    "1. A and B .hyp\n",
    "proves\n",
    "2. B\n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()\n",
    "  "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'repeat' rule for line 9 failed.\n",
      "'imp intro' rule successfully applied to line 9.\n",
      "'LEM' rule for line 8 failed.\n",
      "'repeat' rule for line 8 failed.\n",
      "'or intro' rule for line 8 failed.\n",
      "'bot elim' rule for line 8 failed.\n",
      "'not elim' rule for line 8 failed.\n",
      "'imp elim' rule for line 8 failed.\n",
      "'iff elim' rule for line 8 failed.\n",
      "'and elim' rule for line 8 failed.\n",
      "'or elim' rule successfully applied to line 8.\n",
      "'LEM' rule for line 7 failed.\n",
      "'repeat' rule for line 7 failed.\n",
      "'or intro' rule successfully applied to line 7.\n",
      "'LEM' rule for line 5 failed.\n",
      "'repeat' rule for line 5 failed.\n",
      "'or intro' rule successfully applied to line 5.\n",
      "'repeat' rule for line 4 failed.\n",
      "'bot elim' rule for line 4 failed.\n",
      "'not elim' rule for line 4 failed.\n",
      "'imp elim' rule successfully applied to line 4.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. A imp B\t .hyp\n",
      "├─\n",
      "││2. A or C\t .hyp\n",
      "│├─\n",
      "│││3. A\t .hyp\n",
      "││├─\n",
      "│││4. B\t\u001b[92m✓\u001b[39m imp elim 1,3\n",
      "│││5. B or C\t\u001b[92m✓\u001b[39m or intro 4\n",
      "│││6. C\t .hyp\n",
      "││├─\n",
      "│││7. B or C\t\u001b[92m✓\u001b[39m or intro 6\n",
      "││8. B or C\t\u001b[92m✓\u001b[39m or elim 2,3-5,6-7\n",
      "│9. A or C imp B or C\t\u001b[92m✓\u001b[39m imp intro 2-8\n"
     ]
    }
   ],
   "source": [
    "# or elim (line 8)\n",
    "\n",
    "prf_str = '''\n",
    "1. A imp B .hyp\n",
    "proves\n",
    "  2. A or C .hyp\n",
    "  proves\n",
    "    3. A .hyp\n",
    "    proves\n",
    "    4. B\n",
    "    5. B or C\n",
    "    6. C .hyp\n",
    "    proves\n",
    "    7. B or C\n",
    "  8. B or C\n",
    "9. A or C imp B or C\n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'repeat' rule for line 3 failed.\n",
      "'bot elim' rule for line 3 failed.\n",
      "'not elim' rule for line 3 failed.\n",
      "'imp elim' rule for line 3 failed.\n",
      "'iff elim' rule successfully applied to line 3.\n",
      "\n",
      "All formulas have been validated.\n",
      "\n",
      "│1. B\t .hyp\n",
      "│2. A iff B\t .hyp\n",
      "├─\n",
      "│3. A\t\u001b[92m✓\u001b[39m iff elim 1,2\n"
     ]
    }
   ],
   "source": [
    "# iff elim \n",
    "\n",
    "prf_str = '''\n",
    "1. B .hyp\n",
    "2. A iff B .hyp\n",
    "proves\n",
    "3. A\n",
    "'''\n",
    "proof = ProofNodeS(parse_fitch(prf_str))\n",
    "assert isinstance(proof, ProofNodeS)\n",
    "proof.search_proof(1)\n",
    "proof.show_fitch_text()"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "mlenv",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.11.2"
  },
  "orig_nbformat": 4
 },
 "nbformat": 4,
 "nbformat_minor": 2
}