Skip to content

Commit

Permalink
Agrego ejercicios de PLP
Browse files Browse the repository at this point in the history
  • Loading branch information
@joangq
joangq committed Apr 29, 2024
1 parent 966e54f commit 73c6c5c
Showing 1 changed file with 299 additions and 0 deletions.
299 changes: 299 additions & 0 deletions COMP930015-PLP/practicas/3/plp_p3.ipynb
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,299 @@
{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"from IPython.display import display, Math\n",
"\n",
"# https://github.com/joangq/pyquent\n",
"from pyquent import Pyquent\n",
"from pyquent.natural_deduction import dict_to_latex\n",
"from pyquent.transformer import *\n",
"from pyquent.utils import LATEX_FONT_SIZE\n",
"\n",
"pyquent = Pyquent()"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
"parse_to_latex = lambda s: '' if not s else pyquent.transform(s).to_latex()"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [],
"source": [
"def display_math(s, size=7):\n",
" # Size between 1 and 10\n",
" display(Math(LATEX_FONT_SIZE[size-1]+'{'+s+'}'))\n",
"\n",
"size = 0\n",
"implication_introduction = r'\\Rightarrow_i'\n",
"negation_elimination = r'\\neg_e'\n",
"PBC = '{' +LATEX_FONT_SIZE[max(0, size-2)]+ '\\\\text{\\\\textcolor{pink}{PBC}}}'\n",
"bottom = r'\\bot'\n",
"axiom = '{'+LATEX_FONT_SIZE[max(0, size-2)]+'\\\\text{ax}}'\n",
"double_negation_introduction = '\\\\textcolor{pink}{\\\\neg\\\\neg_i}'\n",
"disjunction_introduction_left = r'\\vee_{i_1}'\n",
"disjunction_introduction_right = r'\\vee_{i_2}'\n",
"negation_introduction = r'\\neg_i'\n",
"conjunction_introduction = r'\\wedge_i'\n",
"conjunction_elimination_left = r'\\wedge_{e_1}'\n",
"conjunction_elimination_right = r'\\wedge_{e_2}'"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$\\displaystyle \\tiny{\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q)\\;\\vdash \\neg (P \\land Q)}{\\tiny\\text{ax}}},\\;\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P\\;\\vdash \\neg (P \\land Q)}{\\tiny\\text{ax}}},\\;\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P\\;\\vdash \\neg (\\neg P \\lor \\neg Q)}{\\tiny\\text{ax}}},\\;\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P,\\;Q\\;\\vdash Q}{\\tiny\\text{ax}}},\\;\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P,\\;Q\\;\\vdash \\neg (P \\land Q)}{\\tiny\\text{ax}}},\\;\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P,\\;Q\\;\\vdash P}{\\tiny\\text{ax}}},\\;\\displaystyle{\\frac{}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P,\\;Q\\;\\vdash Q}{\\tiny\\text{ax}}}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P,\\;Q\\;\\vdash (P \\land Q)}\\wedge_i}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P,\\;Q\\;\\vdash \\neg \\neg (P \\land Q)}\\textcolor{pink}{\\neg\\neg_i}}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P,\\;Q\\;\\vdash \\bot}\\neg_e}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P,\\;Q\\;\\vdash \\neg Q}\\neg_i}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P,\\;Q\\;\\vdash \\bot}\\neg_e}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P\\;\\vdash \\neg Q}\\neg_i}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P\\;\\vdash \\neg P \\lor \\neg Q}\\vee_{i_2}}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P\\;\\vdash \\bot}\\neg_e}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P\\;\\vdash P \\land Q}{\\tiny\\text{\\textcolor{pink}{PBC}}}}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P\\;\\vdash \\neg \\neg (P \\land Q)}\\textcolor{pink}{\\neg\\neg_i}}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P\\;\\vdash \\bot}\\neg_e}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q),\\;P\\;\\vdash \\bot}\\neg_i}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q)\\;\\vdash (\\neg P \\lor \\neg Q)}\\vee_{i_1}},\\;\\displaystyle{\\frac{}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q)\\;\\vdash \\neg (\\neg P \\lor \\neg Q)}{\\tiny\\text{ax}}}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q)\\;\\vdash \\bot}\\neg_e}}{\\neg P \\land Q,\\;\\neg (\\neg P \\lor \\neg Q)\\;\\vdash (P \\land Q)}{\\tiny\\text{\\textcolor{pink}{PBC}}}}}{\\neg (P \\land Q),\\;\\neg (\\neg P \\lor \\neg Q)\\;\\vdash \\neg \\neg (P \\land Q)}\\textcolor{pink}{\\neg\\neg_i}}}{\\neg (P \\land Q),\\;\\neg P \\lor \\neg Q\\;\\vdash \\bot}\\neg_e}}{\\neg (P \\land Q) \\vdash \\neg (\\neg P \\lor \\neg Q)}{\\tiny\\text{\\textcolor{pink}{PBC}}}}}{\\neg (P \\land Q) \\Rightarrow \\neg P \\lor \\neg Q}\\Rightarrow_i}}$"
],
"text/plain": [
"<IPython.core.display.Math object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"size = 1\n",
"\n",
"\n",
"d = {\n",
" 'rule': implication_introduction,\n",
" 'not (P and Q) => not P or not Q': {\n",
" 'rule': PBC,\n",
" 'not (P and Q) |- not (not P or not Q)': {\n",
" 'rule': negation_elimination,\n",
" ('not (P and Q)', 'not P or not Q', '|- bottom'): [\n",
" {'rule': axiom, \n",
" ('not (P and Q)', 'not (not P or not Q)', '|- not (P and Q)'): ''},\n",
"\n",
" {'rule': double_negation_introduction, \n",
" ('not (P and Q)', 'not (not P or not Q)', '|- not not (P and Q)'): {\n",
" 'rule': PBC,\n",
" ('not P and Q', 'not (not P or not Q)', '|- (P and Q)'): {\n",
" 'rule': negation_elimination,\n",
" ('not (P and Q)', 'not (not P or not Q)', '|- bottom') : [\n",
" {\n",
" 'rule': disjunction_introduction_left,\n",
" ('not (P and Q)', 'not (not P or not Q)', '|- (not P or not Q)'): {\n",
" 'rule': negation_introduction,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', '|- bottom'): { \n",
" 'rule': negation_elimination,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', '|- bottom'): [\n",
" {'rule': axiom, \n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', '|- not (P and Q)'): ''},\n",
"\n",
" {'rule': double_negation_introduction,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', '|- not not (P and Q)'): {\n",
" 'rule': PBC,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', '|- P and Q'): {\n",
" 'rule': negation_elimination,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', '|- bottom'): [\n",
" {'rule': axiom,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', '|- not (not P or not Q)'): ''},\n",
" \n",
" {'rule': disjunction_introduction_right,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', '|- not P or not Q'): {\n",
" 'rule': negation_introduction,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', '|- not Q'): {\n",
" 'rule': negation_elimination,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- bottom'): [\n",
" {'rule': axiom,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- Q'): ''},\n",
"\n",
" {'rule': negation_introduction,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- not Q'): {\n",
" 'rule': negation_elimination,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- bottom'): [\n",
" {'rule': axiom,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- not (P and Q)'): ''},\n",
"\n",
" {'rule': double_negation_introduction,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- not not (P and Q)'): {\n",
" 'rule': conjunction_introduction,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- (P and Q)'): [\n",
" {'rule': axiom,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- P'): ''},\n",
" \n",
" {'rule': axiom,\n",
" ('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- Q'): ''},\n",
" ]\n",
" }\n",
" }\n",
" ]\n",
" }\n",
" }\n",
" ]\n",
" }\n",
" }\n",
" }\n",
" ]\n",
" }\n",
" }\n",
" }\n",
" ]\n",
" }\n",
" }},\n",
"\n",
" {'rule': axiom,\n",
" ('not (P and Q)', 'not (not P or not Q)', '|- not (not P or not Q)'): ''}\n",
" ]\n",
" }\n",
" }\n",
" }\n",
" ]\n",
" }\n",
" }\n",
"}\n",
"\n",
"latex = dict_to_latex(d, parser=parse_to_latex)\n",
"display_math(latex, size=size)"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Code length: 1791\n",
"Latex length: 2874\n",
"Compression ratio (python/latex): 62.32%\n",
"Which means that the python code is 1.60 times smaller than the latex code\n"
]
}
],
"source": [
"code_length = len(str(d))\n",
"latex_length = len(latex)\n",
"print(f'Code length: {code_length}')\n",
"print(f'Latex length: {latex_length}')\n",
"print(f'Compression ratio (python/latex): {100 * code_length/latex_length:.2f}%')\n",
"print('Which means that the python code is {:.2f} times smaller than the latex code'.format(latex_length/code_length))"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/latex": [
"$\\displaystyle \\normalsize{\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{}{\\neg P \\lor \\neg Q,\\;P \\land Q\\;\\vdash \\neg P \\lor \\neg Q}{\\tiny\\text{ax}}},\\;\\displaystyle{\\frac{\\displaystyle{\\frac{}{\\neg P \\lor \\neg Q,\\;P \\land Q\\;\\vdash \\neg P \\lor \\neg Q}{\\tiny\\text{ax}}},\\;\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{}{\\neg P \\lor \\neg Q,\\;P \\land Q,\\;\\neg P\\;\\vdash \\neg P}{\\tiny\\text{ax}}},\\;\\displaystyle{\\frac{\\displaystyle{\\frac{}{\\neg P \\lor \\neg Q,\\;P \\land Q,\\;\\neg P\\;\\vdash P \\land Q}{\\tiny\\text{ax}}}}{\\neg P \\lor \\neg Q,\\;P \\land Q,\\;\\neg P\\;\\vdash P}\\wedge_{e_1}}}{\\neg P \\lor \\neg Q,\\;P \\land Q,\\;\\neg P\\;\\vdash \\bot}\\neg_e}}{\\neg P \\lor \\neg Q,\\;P \\land Q,\\;\\neg P\\;\\vdash \\neg (\\neg P \\lor \\neg Q)}\\neg_i},\\;\\displaystyle{\\frac{\\displaystyle{\\frac{\\displaystyle{\\frac{}{\\neg P \\lor \\neg Q,\\;P \\land Q,\\;\\neg Q\\;\\vdash \\neg Q}{\\tiny\\text{ax}}},\\;\\displaystyle{\\frac{\\displaystyle{\\frac{}{\\neg P \\lor \\neg Q,\\;P \\land Q,\\;\\neg Q\\;\\vdash P \\land Q}{\\tiny\\text{ax}}}}{\\neg P \\lor \\neg Q,\\;P \\land Q,\\;\\neg Q\\;\\vdash Q}\\wedge_{e_1}}}{\\neg P \\lor \\neg Q,\\;P \\land Q,\\;\\neg Q\\;\\vdash \\bot}\\neg_e}}{\\neg P \\lor \\neg Q,\\;P \\land Q,\\;\\neg Q\\;\\vdash \\neg (\\neg P \\lor \\neg Q)}\\neg_i}}{\\neg P \\lor \\neg Q\\;P \\land Q \\vdash \\neg P \\lor \\neg Q}\\neg_e}}{\\neg P \\lor \\neg Q,\\;P \\land Q\\;\\vdash \\bot}\\neg_e}}{\\neg P \\lor \\neg Q \\vdash \\neg (P \\land Q)}\\neg_i}}{\\neg P \\lor \\neg Q \\Rightarrow \\neg (P \\land Q)}\\Rightarrow_i}}$"
],
"text/plain": [
"<IPython.core.display.Math object>"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"size = 5\n",
"\n",
"d = {'rule': implication_introduction,\n",
" 'not P or not Q => not (P and Q)': {\n",
" 'rule': negation_introduction,\n",
" 'not P or not Q |- not (P and Q)': {\n",
" 'rule': negation_elimination,\n",
" ('not P or not Q', 'P and Q', '|- bottom'): [\n",
" {'rule': axiom, \n",
" ('not P or not Q', 'P and Q', '|- not P or not Q'): ''},\n",
" {'rule': negation_elimination,\n",
" ('not P or not Q','P and Q |- not P or not Q'): [\n",
" {'rule': axiom,\n",
" ('not P or not Q', 'P and Q', '|- not P or not Q'): ''},\n",
"\n",
" # Este paso está raro, la eliminación de la negación tiene dos premisas,\n",
" # que Gamma valide tau y no tau. Acá hay tres. (?)\n",
" # Lo dejo porque probablemente se pueda loopear hasta la misma conclusión,\n",
" # y hacer el camino del arbol derecho (con Q), y terminar con la misma deducción.\n",
"\n",
" {'rule': negation_introduction,\n",
" ('not P or not Q', 'P and Q', 'not P', '|- not (not P or not Q)'): \n",
" {'rule': negation_elimination,\n",
" ('not P or not Q', 'P and Q', 'not P', '|- bottom'): [\n",
" {'rule': axiom,\n",
" ('not P or not Q', 'P and Q', 'not P', '|- not P'): ''},\n",
" \n",
" {'rule': conjunction_elimination_left,\n",
" ('not P or not Q', 'P and Q', 'not P', '|- P'): {\n",
" 'rule': axiom,\n",
" ('not P or not Q', 'P and Q', 'not P', '|- P and Q'): '',\n",
" }\n",
" }\n",
" ]\n",
" }\n",
" },\n",
" \n",
" {'rule': negation_introduction,\n",
" ('not P or not Q', 'P and Q', 'not Q', '|- not (not P or not Q)'): \n",
" {'rule': negation_elimination,\n",
" ('not P or not Q', 'P and Q', 'not Q', '|- bottom'): [\n",
" {'rule': axiom,\n",
" ('not P or not Q', 'P and Q', 'not Q', '|- not Q'): ''},\n",
" \n",
" {'rule': conjunction_elimination_left,\n",
" ('not P or not Q', 'P and Q', 'not Q', '|- Q'): {\n",
" 'rule': axiom,\n",
" ('not P or not Q', 'P and Q', 'not Q', '|- P and Q'): '',\n",
" }\n",
" }\n",
" ]\n",
" }\n",
" },\n",
" ]\n",
" }\n",
" ]\n",
" }\n",
" }\n",
"}\n",
"\n",
"latex = dict_to_latex(d, parser=parse_to_latex)\n",
"display_math(latex, size=size)"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"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.10.12"
}
},
"nbformat": 4,
"nbformat_minor": 2
}

0 comments on commit 73c6c5c

Please sign in to comment.