Skip to content

Commit 4937016

Browse files
joangqjoangq
authored
Agrego ejercicios
1 parent 73c6c5c commit 4937016

File tree

4 files changed

+151
-0
lines changed

4 files changed

+151
-0
lines changed

‎COMP930015-PLP/practicas/3/ej8a.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
$$
2+
\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}
3+
$$

‎COMP930015-PLP/practicas/3/ej8a.py

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
{
2+
'rule': implication_introduction,
3+
'not (P and Q) => not P or not Q': {
4+
'rule': PBC,
5+
'not (P and Q) |- not (not P or not Q)': {
6+
'rule': negation_elimination,
7+
('not (P and Q)', 'not P or not Q', '|- bottom'): [
8+
{'rule': axiom,
9+
('not (P and Q)', 'not (not P or not Q)', '|- not (P and Q)'): ''},
10+
11+
{'rule': double_negation_introduction,
12+
('not (P and Q)', 'not (not P or not Q)', '|- not not (P and Q)'): {
13+
'rule': PBC,
14+
('not P and Q', 'not (not P or not Q)', '|- (P and Q)'): {
15+
'rule': negation_elimination,
16+
('not (P and Q)', 'not (not P or not Q)', '|- bottom') : [
17+
{
18+
'rule': disjunction_introduction_left,
19+
('not (P and Q)', 'not (not P or not Q)', '|- (not P or not Q)'): {
20+
'rule': negation_introduction,
21+
('not (P and Q)', 'not (not P or not Q)', 'P', '|- bottom'): {
22+
'rule': negation_elimination,
23+
('not (P and Q)', 'not (not P or not Q)', 'P', '|- bottom'): [
24+
{'rule': axiom,
25+
('not (P and Q)', 'not (not P or not Q)', 'P', '|- not (P and Q)'): ''},
26+
27+
{'rule': double_negation_introduction,
28+
('not (P and Q)', 'not (not P or not Q)', 'P', '|- not not (P and Q)'): {
29+
'rule': PBC,
30+
('not (P and Q)', 'not (not P or not Q)', 'P', '|- P and Q'): {
31+
'rule': negation_elimination,
32+
('not (P and Q)', 'not (not P or not Q)', 'P', '|- bottom'): [
33+
{'rule': axiom,
34+
('not (P and Q)', 'not (not P or not Q)', 'P', '|- not (not P or not Q)'): ''},
35+
36+
{'rule': disjunction_introduction_right,
37+
('not (P and Q)', 'not (not P or not Q)', 'P', '|- not P or not Q'): {
38+
'rule': negation_introduction,
39+
('not (P and Q)', 'not (not P or not Q)', 'P', '|- not Q'): {
40+
'rule': negation_elimination,
41+
('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- bottom'): [
42+
{'rule': axiom,
43+
('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- Q'): ''},
44+
45+
{'rule': negation_introduction,
46+
('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- not Q'): {
47+
'rule': negation_elimination,
48+
('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- bottom'): [
49+
{'rule': axiom,
50+
('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- not (P and Q)'): ''},
51+
52+
{'rule': double_negation_introduction,
53+
('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- not not (P and Q)'): {
54+
'rule': conjunction_introduction,
55+
('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- (P and Q)'): [
56+
{'rule': axiom,
57+
('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- P'): ''},
58+
59+
{'rule': axiom,
60+
('not (P and Q)', 'not (not P or not Q)', 'P', 'Q', '|- Q'): ''},
61+
]
62+
}
63+
}
64+
]
65+
}
66+
}
67+
]
68+
}
69+
}
70+
}
71+
]
72+
}
73+
}
74+
}
75+
]
76+
}
77+
}},
78+
79+
{'rule': axiom,
80+
('not (P and Q)', 'not (not P or not Q)', '|- not (not P or not Q)'): ''}
81+
]
82+
}
83+
}
84+
}
85+
]
86+
}
87+
}
88+
}

‎COMP930015-PLP/practicas/3/ej8b.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
$$
2+
\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}
3+
$$

‎COMP930015-PLP/practicas/3/ej8b.py

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
{'rule': implication_introduction,
2+
'not P or not Q => not (P and Q)': {
3+
'rule': negation_introduction,
4+
'not P or not Q |- not (P and Q)': {
5+
'rule': negation_elimination,
6+
('not P or not Q', 'P and Q', '|- bottom'): [
7+
{'rule': axiom,
8+
('not P or not Q', 'P and Q', '|- not P or not Q'): ''},
9+
{'rule': negation_elimination,
10+
('not P or not Q','P and Q |- not P or not Q'): [
11+
{'rule': axiom,
12+
('not P or not Q', 'P and Q', '|- not P or not Q'): ''},
13+
14+
# Este paso está raro, la eliminación de la negación tiene dos premisas,
15+
# que Gamma valide tau y no tau. Acá hay tres. (?)
16+
# Lo dejo porque probablemente se pueda loopear hasta la misma conclusión,
17+
# y hacer el camino del arbol derecho (con Q), y terminar con la misma deducción.
18+
19+
{'rule': negation_introduction,
20+
('not P or not Q', 'P and Q', 'not P', '|- not (not P or not Q)'):
21+
{'rule': negation_elimination,
22+
('not P or not Q', 'P and Q', 'not P', '|- bottom'): [
23+
{'rule': axiom,
24+
('not P or not Q', 'P and Q', 'not P', '|- not P'): ''},
25+
26+
{'rule': conjunction_elimination_left,
27+
('not P or not Q', 'P and Q', 'not P', '|- P'): {
28+
'rule': axiom,
29+
('not P or not Q', 'P and Q', 'not P', '|- P and Q'): '',
30+
}
31+
}
32+
]
33+
}
34+
},
35+
36+
{'rule': negation_introduction,
37+
('not P or not Q', 'P and Q', 'not Q', '|- not (not P or not Q)'):
38+
{'rule': negation_elimination,
39+
('not P or not Q', 'P and Q', 'not Q', '|- bottom'): [
40+
{'rule': axiom,
41+
('not P or not Q', 'P and Q', 'not Q', '|- not Q'): ''},
42+
43+
{'rule': conjunction_elimination_left,
44+
('not P or not Q', 'P and Q', 'not Q', '|- Q'): {
45+
'rule': axiom,
46+
('not P or not Q', 'P and Q', 'not Q', '|- P and Q'): '',
47+
}
48+
}
49+
]
50+
}
51+
},
52+
]
53+
}
54+
]
55+
}
56+
}
57+
}

0 commit comments

Comments
 (0)