proofs_propositional/validate_proof.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "# type: ignore\n",
    "try:\n",
    "  import sys\n",
    "  sys.path.append('../')\n",
    "  from modules.validate_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 validate_prop import *\n",
    "\n",
    "from pprint import pprint"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "input_str = ' imp  intro   4-8 '\n",
      "rule: imp intro\n",
      "premise: ['4-8']\n",
      "\n",
      "output from __str__():\n",
      "  imp intro 4-8\n"
     ]
    }
   ],
   "source": [
    "# Construct an Ann object from a string.\n",
    "s = \" imp  intro   4-8 \"\n",
    "try:\n",
    "  ann = Ann(s)\n",
    "  print(f\"input_str = '{ann.input_str}'\")\n",
    "  print(ann.build_str())\n",
    "  print(\"\\noutput from __str__():\")\n",
    "  print(\" \", ann)\n",
    "except Exception as e:\n",
    "    print(e)  "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "type: formula\n",
      "line: A imp B .hyp\n",
      "formula: A imp B\n",
      "ann: hyp \n",
      "is_hyp: True\n",
      "\n",
      "A imp B\t .hyp \n"
     ]
    }
   ],
   "source": [
    "# Construct a NodeLabel object from a string.\n",
    "line = \"A imp B .hyp\"\n",
    "label = NodeLabel(LabelType.FORMULA, line)\n",
    "print(label.build_str())\n",
    "print()\n",
    "print(label)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "│1. A imp B\t .hyp \n",
      "│2. A\t .hyp \n",
      "├─\n",
      "│3. B\t .imp elim 1,2\n",
      "│4. A\t .repeat 2\n",
      "\n"
     ]
    }
   ],
   "source": [
    "# Construct a ProofNode manually. (not by using the parser)\n",
    "line1 = \"A imp B .hyp\"\n",
    "label1 = NodeLabel(LabelType.FORMULA, line1)\n",
    "node1 = ProofNode(label1)\n",
    "line2 = \"A .hyp\"\n",
    "label2 = NodeLabel(LabelType.FORMULA, line2)\n",
    "node2 = ProofNode(label2)\n",
    "line3 = \"B .imp elim 1,2\"\n",
    "label3 = NodeLabel(LabelType.FORMULA, line3)\n",
    "node3 = ProofNode(label3)\n",
    "line4 = \"A .repeat 2\"\n",
    "label4 = NodeLabel(LabelType.FORMULA, line4)\n",
    "node4 = ProofNode(label4)\n",
    "label0 = NodeLabel()\n",
    "node0 = ProofNode(label0, [node1, node2, node3, node4])\n",
    "node0.build_index() # necessary for printing node0\n",
    "print(node0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "│1. A imp B\t .hyp \n",
      "│2. B imp C\t .hyp \n",
      "├─\n",
      "││3. A\t .hyp \n",
      "│├─\n",
      "││4. B\t .imp elim 1,3\n",
      "││5. C\t .imp elim 2,4\n",
      "│6. A imp C\t .imp intro 3-5\n",
      "\n"
     ]
    }
   ],
   "source": [
    "# Another example, similar to the one above.\n",
    "line1 = \"A imp B .hyp\"\n",
    "label1 = NodeLabel(LabelType.FORMULA, line1)\n",
    "node1 = ProofNode(label1)\n",
    "line2 = \"B imp C .hyp\"\n",
    "label2 = NodeLabel(LabelType.FORMULA, line2)\n",
    "node2 = ProofNode(label2)\n",
    "line3 = \"A .hyp\"\n",
    "label3 = NodeLabel(LabelType.FORMULA, line3)\n",
    "node3 = ProofNode(label3)\n",
    "line4 = \"B .imp elim 1,3\"\n",
    "label4 = NodeLabel(LabelType.FORMULA, line4)\n",
    "node4 = ProofNode(label4)\n",
    "line5 = \"C .imp elim 2,4\"\n",
    "label5 = NodeLabel(LabelType.FORMULA, line5)\n",
    "node5 = ProofNode(label5)\n",
    "line6 = \"A imp C .imp intro 3-5\"\n",
    "label6 = NodeLabel(LabelType.FORMULA, line6)\n",
    "node6 = ProofNode(label6)\n",
    "label_root = NodeLabel()\n",
    "label_sub = NodeLabel()\n",
    "node_sub = ProofNode(label_sub, [node3, node4, node5])\n",
    "node_root = ProofNode(label_root, [node1, node2, node_sub, node6])\n",
    "node_root.build_index()\n",
    "print(node_root)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[prf_str1]:\n",
      "A imp B .hyp\n",
      "B imp C .hyp\n",
      "{{\n",
      "  A .hyp\n",
      "  B     .imp elim 1,3\n",
      "  C     .imp elim 2,4\n",
      "}}\n",
      "A imp C .imp intro 3-5\n",
      "\n",
      "[prf_str2]:\n",
      "A imp B\t .hyp\n",
      "B imp C\t .hyp\n",
      "{{\n",
      "  A\t .hyp\n",
      "  B\t .imp elim 1,3\n",
      "  C\t .imp elim 2,4\n",
      "}}\n",
      "A imp C\t .imp intro 3-5\n",
      "\n",
      "[prf_str3]:\n",
      "A imp B .hyp\n",
      "B imp C .hyp\n",
      "{{\n",
      "  A .hyp\n",
      "  B     .imp elim 1,3\n",
      "  C     .imp elim 2,4\n",
      "}}\n",
      "A imp C .imp intro 3-5\n",
      "\n",
      "[prf_str4]:\n",
      "A imp B\t .hyp\n",
      "B imp C\t .hyp\n",
      "{{\n",
      "  A\t .hyp\n",
      "  B\t .imp elim 1,3\n",
      "  C\t .imp elim 2,4\n",
      "}}\n",
      "A imp C\t .imp intro 3-5\n",
      "\n"
     ]
    }
   ],
   "source": [
    "# This is a test for the preprocessing function get_str_li().\n",
    "# The output of get_str_li() is a list of strings \n",
    "# to be fed to the parser.\n",
    "\n",
    "# You may or may not prefix each line with line number.\n",
    "# The parser can assign the correct line number \n",
    "# to each node anyway.\n",
    "# You may also use | instead  of TAB to indent subproofs.\n",
    "# The following 4 input strings are all equivalent---they \n",
    "# are parsed into the same proof tree.\n",
    "\n",
    "prf_str1 = '''\n",
    "1. A imp B .hyp\n",
    "2. B imp C .hyp\n",
    "proves\n",
    "  3. A .hyp\n",
    "  proves\n",
    "  4. B     .imp elim 1,3\n",
    "  5. C     .imp elim 2,4\n",
    "6. A imp C .imp intro 3-5\n",
    "'''\n",
    "# or,\n",
    "prf_str2 = '''\n",
    "│1. A imp B\t .hyp\n",
    "│2. B imp C\t .hyp\n",
    "├─\n",
    "││3. A\t .hyp\n",
    "│├─\n",
    "││4. B\t .imp elim 1,3\n",
    "││5. C\t .imp elim 2,4\n",
    "│6. A imp C\t .imp intro 3-5\n",
    "'''\n",
    "# or, above two without numbering\n",
    "prf_str3 = '''\n",
    "A imp B .hyp\n",
    "B imp C .hyp\n",
    "proves\n",
    "  A .hyp\n",
    "  proves\n",
    "  B     .imp elim 1,3\n",
    "  C     .imp elim 2,4\n",
    "A imp C .imp intro 3-5\n",
    "'''\n",
    "# or,\n",
    "prf_str4 = '''\n",
    "│A imp B\t .hyp\n",
    "│B imp C\t .hyp\n",
    "├─\n",
    "││A\t .hyp\n",
    "│├─\n",
    "││B\t .imp elim 1,3\n",
    "││C\t .imp elim 2,4\n",
    "│A imp C\t .imp intro 3-5\n",
    "'''\n",
    "# Convert either string to the following.\n",
    "'''\n",
    "A imp B\t .hyp\n",
    "B imp C\t .hyp\n",
    "{{\n",
    "  A\t .hyp\n",
    "  B\t .imp elim 1,3\n",
    "  C\t .imp elim 2,4\n",
    "}}\n",
    "A imp C\t .imp intro 3-5\n",
    "'''\n",
    "\n",
    "for i in range(1, 5):\n",
    "  prf_str_name = f\"prf_str{i}\"\n",
    "  prf_str = eval(prf_str_name)\n",
    "  print(f\"[{prf_str_name}]:\")\n",
    "  lines = get_str_li(prf_str, tabsize=2)\n",
    "  print_lines(lines)    \n",
    "  print()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "A imp B .hyp\n",
      "{{\n",
      "  A or C .hyp\n",
      "  {{\n",
      "    A .hyp\n",
      "    B .imp elim 1,3\n",
      "    B or C .or intro 4\n",
      "  }}\n",
      "  {{\n",
      "    C .hyp\n",
      "    B or C .or intro 6\n",
      "  }}\n",
      "  B or C .or elim 2,3-5,6-7\n",
      "}}\n",
      "A or C imp B or C .imp intro 2-8\n"
     ]
    }
   ],
   "source": [
    "# Another example.\n",
    "\n",
    "# This is a Fitch proof for \n",
    "#         A -> B |- (A or C) -> (B or C)\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 .imp elim 1,3\n",
    "    5. B or C .or intro 4\n",
    "    6. C .hyp\n",
    "    proves\n",
    "    7. B or C .or intro 6\n",
    "  8. B or C .or elim 2,3-5,6-7\n",
    "9. A or C imp B or C .imp intro 2-8'''\n",
    "lines = get_str_li(prf_str, tabsize=2)\n",
    "print_lines(lines)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "get_str_li(): same level and right_after_proves, but is_hyp\n",
      "\tPerhaps you should indent the following line:\n",
      "\t5. A\t .hyp\n"
     ]
    }
   ],
   "source": [
    "# A buggy example.\n",
    "\n",
    "prf_str = '''\n",
    "1. A imp B\t .hyp\n",
    "2.\n",
    "proves\n",
    "  3. # subproof may start with a comment\n",
    "  4. A or C\t .hyp \n",
    "  proves\n",
    "  5. A\t .hyp \n",
    "  proves\n",
    "  6. B\t .imp elim 1,5\n",
    "  7. B or C\t .and intro 6\n",
    "  8. C\t .hyp \n",
    "  proves\n",
    "  9. B or C\t .or intro 8\n",
    "  10. # end of subproof\n",
    "  11. B or C\t .or elim 3,5-7,8-10\n",
    "12. A or C imp B or C\t .imp intro 3-11\n",
    "'''\n",
    "try:\n",
    "  lines = get_str_li(prf_str, tabsize=2)\n",
    "  print_lines(lines) \n",
    "except Exception as e:\n",
    "  print(e)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "│1. A\t .hyp \n",
      "│2. B\t .hyp \n",
      "├─\n",
      "│3. A and B\t .and intro 1,2\n",
      "\n"
     ]
    }
   ],
   "source": [
    "# This is the first test for the parser.\n",
    "# Validation is done too within the parser.\n",
    "# Note that we omitted the line numbers and it still works.\n",
    "prf_str = '''\n",
    "A .hyp\n",
    "B  .hyp\n",
    "proves\n",
    "A and B .and intro 1,2\n",
    "'''\n",
    "proof = parse_fitch(prf_str)\n",
    "print(proof)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "│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 .imp elim 1,3\n",
      "│││5. B or C\t .or intro 4\n",
      "│││6. C\t .hyp \n",
      "││├─\n",
      "│││7. B or C\t .or intro 6\n",
      "││8. B or C\t .or elim 2,3-5,6-7\n",
      "│9. A or C imp B or C\t .imp intro 2-8\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": [
    "# Show validation result.\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      .imp  elim   1,3\n",
    "    5. B or C .or intro 4\n",
    "    6. C .hyp\n",
    "    proves\n",
    "    7. B or C .or intro 6\n",
    "  8. B or C .or elim 2,3-5,6-7\n",
    "9. A or C imp B or C .imp intro 2-8\n",
    "'''\n",
    "proof = parse_fitch(prf_str)\n",
    "proof.show_fitch_text(False) # False means no validation\n",
    "proof.show_fitch_text(True) # True means validation"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "% \\usepackage{proofmood}\n",
      "\\begin{fitchproof}\n",
      "& \\pmvert \\pnumb{1} \\pform{A \\rightarrow B} & \\chknull & \\infrul{hyp} & \\pmnl\n",
      "& \\pmproves & & & \\\\\n",
      "& \\pmvert \\pmvert \\pnumb{2} \\pform{A \\vee C} & \\chknull & \\infrul{hyp} & \\pmnl\n",
      "& \\pmvert \\pmproves & & & \\\\\n",
      "& \\pmvert \\pmvert \\pmvert \\pnumb{3} \\pform{A} & \\chknull & \\infrul{hyp} & \\pmnl\n",
      "& \\pmvert \\pmvert \\pmproves & & & \\\\\n",
      "& \\pmvert \\pmvert \\pmvert \\pnumb{4} \\pform{B} & \\chkch & \\infrule{\\rightarrow}{elim}& \\pmprem{1,3} \\pmnl\n",
      "& \\pmvert \\pmvert \\pmvert \\pnumb{5} \\pform{B \\vee C} & \\chkch & \\infrule{\\vee}{intro}& \\pmprem{4} \\pmnl\n",
      "& \\pmvert \\pmvert & & & \\\\\n",
      "& \\pmvert \\pmvert \\pmvert \\pnumb{6} \\pform{C} & \\chknull & \\infrul{hyp} & \\pmnl\n",
      "& \\pmvert \\pmvert \\pmproves & & & \\\\\n",
      "& \\pmvert \\pmvert \\pmvert \\pnumb{7} \\pform{B \\vee C} & \\chkch & \\infrule{\\vee}{intro}& \\pmprem{6} \\pmnl\n",
      "& \\pmvert \\pmvert & & & \\\\\n",
      "& \\pmvert \\pmvert \\pnumb{8} \\pform{B \\vee C} & \\chkch & \\infrule{\\vee}{elim}& \\pmprem{2,3-5,6-7} \\pmnl\n",
      "& \\pmvert & & & \\\\\n",
      "& \\pmvert \\pnumb{9} \\pform{A \\vee C \\rightarrow B \\vee C} & \\chkch & \\infrule{\\rightarrow}{intro}& \\pmprem{2-8} \\pmnl\n",
      "\\end{fitchproof}\n",
      "\n"
     ]
    }
   ],
   "source": [
    "# LaTeX output\n",
    "print(proof.build_fitch_latex(1))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "│1. A imp B\t .hyp\n",
      "├─\n",
      "││2. A or C\t .hyp\n",
      "│├─\n",
      "│││3. # comment in hypothesis\n",
      "│││4. A\t .hyp\n",
      "││├─\n",
      "│││5. B\t\u001b[92m✓\u001b[39m imp elim 1,4\n",
      "│││6. # below is a blank line\n",
      "│││7. \n",
      "│││8. B or C\t\u001b[91mx and intro 5\u001b[39m\n",
      "│││9. C\t .hyp\n",
      "││├─\n",
      "│││10. B or C\t\u001b[91mx\u001b[39m or intro 1\n",
      "││11. B or C\t\u001b[92m✓\u001b[39m or elim 2,3-8,9-10\n",
      "│12. A or C imp B or C\t\u001b[92m✓\u001b[39m imp intro 2-11\n",
      "│1. A imp B\t .hyp\n",
      "├─\n",
      "││2. A or C\t .hyp\n",
      "│├─\n",
      "│││3. # comment in hypothesis\n",
      "│││4. A\t .hyp\n",
      "││├─\n",
      "│││5. B\t\u001b[92m✓\u001b[39m imp elim 1,4\n",
      "│││6. # below is a blank line\n",
      "│││7. \n",
      "│││8. B or C\t\u001b[91mx and intro 5\u001b[39m\n",
      "│││9. C\t .hyp\n",
      "││├─\n",
      "│││10. B or C\t\u001b[91mx\u001b[39m or intro 1\n",
      "││11. B or C\t\u001b[92m✓\u001b[39m or elim 2,3-8,9-10\n",
      "│12. A or C imp B or C\t\u001b[92m✓\u001b[39m imp intro 2-11\n",
      "\n"
     ]
    }
   ],
   "source": [
    "# Show validation result.\n",
    "# Added some comments and blank lines to the above proof.\n",
    "# Gave wrong annotation to some lines intentionally.\n",
    "prf_str = '''\n",
    "1. A imp B .hyp\n",
    "proves\n",
    "  2. A or C .hyp\n",
    "  proves\n",
    "    3. # comment in hypothesis\n",
    "    4. A .hyp\n",
    "    proves\n",
    "    5. B      .imp  elim   1,4\n",
    "    6. # below is a blank line\n",
    "    7. \n",
    "    8. B or C .and intro 5\n",
    "    9. C .hyp\n",
    "    proves\n",
    "    10. B or C .or intro 1\n",
    "  11. B or C .or elim 2,3-8,9-10\n",
    "12. A or C imp B or C .imp intro 2-11\n",
    "'''\n",
    "try:\n",
    "  proof = parse_fitch(prf_str)\n",
    "  proof.show_fitch_text()\n",
    "  proof.show_fitch_text(True)\n",
    "  print()\n",
    "except Exception as e:\n",
    "  print(e)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{'1-12': [0],\n",
      " '1': [0, 0],\n",
      " '2-11': [0, 1],\n",
      " '2': [0, 1, 0],\n",
      " '3-8': [0, 1, 1],\n",
      " '3': [0, 1, 1, 0],\n",
      " '4': [0, 1, 1, 1],\n",
      " '5': [0, 1, 1, 2],\n",
      " '6': [0, 1, 1, 3],\n",
      " '7': [0, 1, 1, 4],\n",
      " '8': [0, 1, 1, 5],\n",
      " '9-10': [0, 1, 2],\n",
      " '9': [0, 1, 2, 0],\n",
      " '10': [0, 1, 2, 1],\n",
      " '11': [0, 1, 3],\n",
      " '12': [0, 2]}\n"
     ]
    }
   ],
   "source": [
    "# proof.index_dict is a dictionary that maps line numbers \n",
    "# to indices.\n",
    "index_dict = proof.build_index_dict()\n",
    "pprint(index_dict, sort_dicts=False)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "1 <= 5\n",
      "1 <= 8\n",
      "1 <= 10\n",
      "1 <= 11\n",
      "1 <= 12\n",
      "2-11 <= 12\n",
      "2 <= 5\n",
      "2 <= 8\n",
      "2 <= 10\n",
      "2 <= 11\n",
      "3-8 <= 10\n",
      "3-8 <= 11\n",
      "3 <= 5\n",
      "3 <= 8\n",
      "4 <= 5\n",
      "4 <= 8\n",
      "5 <= 8\n",
      "6 <= 8\n",
      "7 <= 8\n",
      "9-10 <= 11\n",
      "9 <= 10\n"
     ]
    }
   ],
   "source": [
    "# The order relation between nodes.\n",
    "# proof := parse_fitch(prf_str)\n",
    "# index_dict = proof.build_index_dict()\n",
    "for i in index_dict:\n",
    "  for j in index_dict:\n",
    "    label_j = proof.get_p_node(j).label\n",
    "    if label_j.type == LabelType.FORMULA and not label_j.is_hyp: # conclusion\n",
    "      if proof.is_earlier(i, j, True):\n",
    "        print(f\"{i} <= {j}\") "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "True\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "# FormulaProp.verified_by()\n",
    "\n",
    "fmla = FormulaProp('B1(x)')\n",
    "node1 = parse_ast('(A iff not C_1) imp B1(x)')\n",
    "node2 = parse_ast('A iff not C_1')\n",
    "print(fmla.verified_by(RuleInfer.IMP_ELIM, [node1, node2]))\n",
    "print(fmla.verified_by(RuleInfer.IMP_ELIM, [node2, node1]))\n",
    "print(fmla.verified_by(RuleInfer.AND_INTRO, [node1, node2]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "# FormulaProp.verified()\n",
    "\n",
    "# A imp B proves A or C imp B or C\n",
    "# annotation for line 5 is intentionally wrong\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 .imp elim 1,3\n",
    "    5. B or C .and intro 4\n",
    "    6. C .hyp\n",
    "    proves\n",
    "    7. B or C .or intro 6\n",
    "  8. B or C .or elim 2,3-5,6-7\n",
    "9. A or C imp B or C .imp intro 2-8\n",
    "'''\n",
    "proof = parse_fitch(prf_str)\n",
    "print(proof.verified(\"4\"))\n",
    "print(proof.verified(\"5\"))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "proof.verified_all()\n",
    "#^ This gives false because there is a line with wrong \n",
    "# annotation: namely, line 5."
   ]
  }
 ],
 "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
}