From 337d6fcd4788b9a16353f05f6c1ef13e9722ac85 Mon Sep 17 00:00:00 2001 From: David Doret Date: Tue, 22 Aug 2023 23:34:35 +0200 Subject: [PATCH] issue #143: enhance disjunction-introduction (left and right) inference-rules + empty restructured pages to prepare the documentation of interence-rules --- .../biconditional_elimination_left.doctree | Bin 0 -> 2543 bytes .../biconditional_elimination_right.doctree | Bin 0 -> 2548 bytes .../biconditional_introduction.doctree | Bin 0 -> 2523 bytes .../conjunction_elimination_left.doctree | Bin 0 -> 2533 bytes .../conjunction_elimination_right.doctree | Bin 0 -> 2538 bytes .../double_negation_elimination.doctree | Bin 0 -> 2528 bytes docs/build/.doctrees/elimination_rule.doctree | Bin 0 -> 11515 bytes .../build/.doctrees/introduction_rule.doctree | Bin 0 -> 12247 bytes .../biconditional_elimination_left.rst.txt | 2 + .../biconditional_elimination_right.rst.txt | 2 + .../biconditional_introduction.rst.txt | 2 + .../conjunction_elimination_left.rst.txt | 2 + .../conjunction_elimination_right.rst.txt | 2 + .../double_negation_elimination.rst.txt | 2 + docs/build/_sources/elimination_rule.rst.txt | 28 ++ docs/build/_sources/introduction_rule.rst.txt | 33 +++ .../build/biconditional_elimination_left.html | 231 +++++++++++++++ .../biconditional_elimination_right.html | 231 +++++++++++++++ docs/build/biconditional_introduction.html | 231 +++++++++++++++ docs/build/conjunction_elimination_left.html | 233 +++++++++++++++ docs/build/conjunction_elimination_right.html | 233 +++++++++++++++ docs/build/double_negation_elimination.html | 233 +++++++++++++++ docs/build/elimination_rule.html | 266 +++++++++++++++++ docs/build/introduction_rule.html | 272 ++++++++++++++++++ 24 files changed, 2003 insertions(+) create mode 100644 docs/build/.doctrees/biconditional_elimination_left.doctree create mode 100644 docs/build/.doctrees/biconditional_elimination_right.doctree create mode 100644 docs/build/.doctrees/biconditional_introduction.doctree create mode 100644 docs/build/.doctrees/conjunction_elimination_left.doctree create mode 100644 docs/build/.doctrees/conjunction_elimination_right.doctree create mode 100644 docs/build/.doctrees/double_negation_elimination.doctree create mode 100644 docs/build/.doctrees/elimination_rule.doctree create mode 100644 docs/build/.doctrees/introduction_rule.doctree create mode 100644 docs/build/_sources/biconditional_elimination_left.rst.txt create mode 100644 docs/build/_sources/biconditional_elimination_right.rst.txt create mode 100644 docs/build/_sources/biconditional_introduction.rst.txt create mode 100644 docs/build/_sources/conjunction_elimination_left.rst.txt create mode 100644 docs/build/_sources/conjunction_elimination_right.rst.txt create mode 100644 docs/build/_sources/double_negation_elimination.rst.txt create mode 100644 docs/build/_sources/elimination_rule.rst.txt create mode 100644 docs/build/_sources/introduction_rule.rst.txt create mode 100644 docs/build/biconditional_elimination_left.html create mode 100644 docs/build/biconditional_elimination_right.html create mode 100644 docs/build/biconditional_introduction.html create mode 100644 docs/build/conjunction_elimination_left.html create mode 100644 docs/build/conjunction_elimination_right.html create mode 100644 docs/build/double_negation_elimination.html create mode 100644 docs/build/elimination_rule.html create mode 100644 docs/build/introduction_rule.html diff --git a/docs/build/.doctrees/biconditional_elimination_left.doctree b/docs/build/.doctrees/biconditional_elimination_left.doctree new file mode 100644 index 0000000000000000000000000000000000000000..1491617bd3db79c78a8b91f1b6d57a9da48c290a GIT binary patch literal 2543 zcma)8-)mbp6mFB+juYES`eO{*bd=F`WsS3i4MtzPx3EygHW;`F`AW95=t_5zZt6S~ zwuiz3daL#y?ho0gd#`V7zjT3+tD~dy<2&CuCx3SS`L}cQNcR zla)EwK7NSL|BCP8m!WUzTW3m}@fdDFBNI|F%XNGc!zihHsoc1E-*Y_k(&+ZN=!mZ9 zy@{e9I$nCkS8l@NsmzRKGQFVcm@An}P1EUE@tKd!!#h9oMGEMn`tM^Ma<`xe5bqB| zpR^f??a*x!IS+S~)I6S-QyO-u_f}3z4**ia+mgAITrX49ISBFH(KN5Wc34^59Hun8 zuzZ$u%Fy$4p01+U7Z1fiJQCaDDE#*7<>VK~t(*KnFD0A2zRCo(`D<%_2Uc!Ulp2sJ zX-YRitZq`rI9bDntYAYDHe>6M-{Z3_WFS66*y0Jo{1~8Ae2!8){a>2Tp!pnWiLb;i z(%G)l5id5KE=`K&K?|~Y5$=0SwNq6|Nny?0a#w@g@y1gX&u)d?r4DB}mdW4kFv?1s zN=Vv*4VIF+aAC)B@1>rDw1+JVXVz%XHH)G9D^(>b*3!6ZN?(*do{RnS(4TY7E%nAm z92iCEJ~2+7ESX$8qlo_fr|cm7 z!u$Ho#?x?+G62(@06+>E#V}M<&r3Szz?FpiVemla1cPcEgCH9_|Yla5YRN~DRhw`>eF*#OBnv_jQoFgk41$V{qwW_^;r z-~>}B4OdhqSz{>p9)^2+1VIl|cY!y04jQI$?BkCI&%&tS1pz1=J(*R24U%L^5qoNl z@Tu^=a4%0zAa>*8$_t~%#?DV-c#t%!0H8@c&ru$aa_m5U{PgQ@f#=B1vJLY|a%29B zrFpa}O@zJRb}YG{RX))EC&K3n&ibBC(L>COc(xOcz{s4m&DkbET#*=Z9S+=;_H;pn zoC}3tu=kEKiTDGTQ?%J1CA!)HsC(79J`!az+CY1hhB?hp_`2JGas?q?Uz7!0q!n2$ zzGezsgFPmbdIkhm!{xv@QtG zsZ<2pJdN2Z?89asgRE*+54G#C&GltkePO2_Cg@&JQDPCJIXv;y&N+q?w!|TV0<}DL zJZQtxqI-vNw9%d3HPwru{mZY9s>eXScN@_g>kK*Q2quTmcs`od9t#*ISVt?tidUSWqK8CCH zX_`OSwAI{Tr(t4brcCo7hP})v1z?c_c1G`2BmaQp-^ZW8e*CwBKEnSO4)v}bwu56$ fyw{4WlI=;Isgfm%%u}^?S(H7xrx_WU&}i#tO~2jbVrB z%;&st@k4z6S9}-041Gi2TJ257W4Hy4Oi0BHFXEdRMoHaCWyj6?p5>X7x@ez^j_8Ws zn<)CBX!^m>`1)XUpy28@knfoqww3Smy=&CH+J#^y_9V7`YIFDI2^P`wj@j1%z^#7?ogX(i+CcYB8 z$Y{IHNW9o|yR<2q2QALxMY!(_Ev%~QN=l>WhT9tFj?<2+cy=r7E_FD=(IUa%Otzf$Ef&Fa2h(DkyQ0`3&$NqXs%+oJJZ?~+VPdkv)f^qI->A7 zS1$OI-$e()X(8=^p=_es6oSUnnThD{25P4#lOQy7Ql$`BGU|7G4#Eg z9e;mpCB7f6UlMMNHbl^ZDQ>v?AJ)ISm{(&VmR8k*)SpAgi&quCV*~MeslWW zDZH=WY&;DIDFZOg3IL>#Q4B*xi@B$B4!jx8TNqs7p5d7`j4)n;C-5UdlJn5TFq$Dr z;2{~9%4c#BMK_G7cbeRY!j=TNhRo+BX$c5eD}e;}45nE!xL-*sYNz7gh)T;n(`1n+ zLLKl$sVyg~FDs5@j$BGBYl7|*CM}(+lt>e0Z`l}VvH_B@XoafFV0751k(pHW*!m=W z!3hRYny{!$vc^#GJxuua2!bA_?gDR$IcS(>vWq_+JPV_emjs}2^kh~6Hb{~wMeM0H z!l%Ny(!M-7f!L1AD<^a@)@FVZ!-J$*1prOrc#iTolw$|-u_MN3P%@2 zVCAT4?O-?PMErrxDcbB0kFK@=>RxrOk3{K=HqaiWc}_DFzV0@lTtSG}7rumxv?r_W z*Gz$Hut#UIn1KV!v2ZsH3hSpEdNNPsRhrhln6}nM1ZVOoXK3IngdjL~aPlC7)&=1? zm5N}cr!iZFeb_8zkX6m

`d%d2yMxU)ZUK3Az_ll-R~-4o4g{bB^JJHF1cbKrM$w z58AM_>)v79tx4;B2r;b9+Cw+B5LPMVy(Fx^#i=;4p`QfqszikEqBy;_;tBqrh=C2m z)nZkzhnYmllY3aKC8;NudUcqql3EYJqqzB0tG51?>irF2tKDC-*k5|B9^GBDkKt-u zn&uBSZ8bO8X_y$9_Guo(u$O7204#FA&gi{r{5NT{#nEh4HAx4M) zbe6A@*cA`Ows<7g#X)@i^2OO}$E`d2iC#!{_Uf__)RwQT`5iTKXI0S1R7n%u8De#3 zO^jztH6b@^GPVx6eSWfr=*1TZSv*FFA1fjiU!wF+{#WZMw4Naq@r~F-3hPY@;`yqx zg*nka=n5;I$NSz=?G(+;B$YKY%Ux60o;RMVbaE?hE_671A`~}ZRrN84yYSf5uT^I(f6oYlnrhA{_ux)>;5wa*Lsr4er*G8rr$}*P_btzzms}8BlwCUKz(T zqq~~LmcL|e@PE<~$jdHLc21vGzWE`kavkXReS~W72s+m)tS^(hDw&wr=Rzp#!twvlW)IAJx6w0teDS|Yx7?%%!8^l z1NNNTvE+VQ`vCoqgfA7G4LzNJL(GeGvJnq}$dYvA>=GcZ$_TlNd+t(uIwwNTgu*Y- zdqobZxLMX$O_(<&jUIwWbIXZQUH@y<`zyjud$?qAxbRv(y1Qf_!`1pc%^$4V zYHzU9Ffj@fGOJVEDvVMnEONlk7`$xdACUa}^b63B|4_gq{7>P~@5W&_IF`g)ow#n< Zmehp`EJI|LyS2&kY-`6rUe{qV{tsnC_N@Q_ literal 0 HcmV?d00001 diff --git a/docs/build/.doctrees/conjunction_elimination_left.doctree b/docs/build/.doctrees/conjunction_elimination_left.doctree new file mode 100644 index 0000000000000000000000000000000000000000..9e944296e08cf891011c4b66f435cf8f5f5041fe GIT binary patch literal 2533 zcma)8OK%%D5Kin!vTRAV^C$`=ZV?n|8Z?$$qXmjw)06k6LrdQ}Q`wBia0?QdkcwHZvx#fA1 zslve1d3uUsS3DFW@knfngYfIi7iT{^Zr$1U^g^<;SC^Tfws>XD8`R02m38t;n#!Fa zR(ICKc(zg(vQih4>N2$s*?n@df%wIz2wFTwkpEsvDn3ICp8OBFr;vMwgv6I(8;NW- ziHPUx4wnW+tI(BKJP-H1rP`^wm87(0Znc9>+9P0b@+ zt42#s)3UJTxc5@e0oDBud$~2*bIoGt|3X!TUUlH@o647!kEdeyGz{llb4$Ik5d@=X zx~D}6VyAIP;N=|Tc1u=Pff{?0k<{$;3dcP}XfI>9n;YY`@qFd+(T!Uj`D4UZ9!E>_QF12 zNL0;JU%91FFZ39nRdcwTyrov7YLKv;7T^p~{*0%j;-6t6HEKk-&J2T848zLjhu1fI)HvwetrDyF}&Y= zSyK&rDFYzQ2^2^nqZr1D>Ul-y9Q9_PH?XO~JLD4B z%5%Ahq8}!-@`hZq!iEI6#;htz(g6@h?%FMI z1@xFq>KqtYu7$g4QMhWhCMSyoUS()Ai|JUMM_{IyafSiDLYNSza2P^k!R zcv`b{*!%4j23S?zEVZk!$@N7#dSRC;xYaniIEHA)n?V& z<4mIE$vrGKoHUb5xhBk2P9ull(cEHYRM-Dn^!^&NlOEo%I9z(ImG0iKkL7B8+U5_| zZM84BY1kNyTx&Xz0Kb{E#xH4dX7wO=gNv za_!TH^z5(nE`1dTmcDf+*n+2c3lfEpidnAH>lDXX+)L#STm22k3oniC)J0G9#m4I- z2C?U*SA6Lu?iWVC3A)xe;7XQK)2w}9fQN;&vQH<6MvtYfcq6icu?Pq1JdOq z)?>d-<22q;QuA~gCNyqQ@2#8!kMwi8>yo*g+D4(Mb711Tr)k-IZL&~Z6BAmTTRzP) zA#Qj&%TGz{h=*b*9*K3aAAf)O;_O$)tvmaXUPyNK>aq~jmanXNgG#xxs!m@?6WkeM zb!SbCXG@hKOO+vYWe%-FdY_%FAp!9@q85)4`O@Rb?KsMFphHRKQ)9~n z&e#EF6)8-a$IHRw!-m5ZuQ}wc^nxr<2al~n3&Ybmw7fFb6U8q$%C{D`1XUf`i+g-7 zQ8iC}a0{Vc>@hwGGq@YSrBD5*M&Xt!H6XJCoH%6}m=oi(u$KM~r`^}dX z)wr880MeX5ffO=Iaipl81v=xXHv_$fbrtVfUKq;=;}viMKN280jeU&T6iK2Uk^!lF zD(6Y``gMlF%A{mEKsHY4@N39r{O4Tf^Px2R>UY=VFAW11HL5;0 zxC$l%f9OhzG5aH6svQb-ucjN4C{xh3wEKCJ(*lierVUlDO9<`rP{BpMj`huJx4;$9 zV+yIKz`$ZH+|7%^g~^JXEHikOq0KDjdv%_GnR3Dz2KW*o2+lp6JSZS_PIyVBA~@uE z&DLS>wWkUB{K2ZN z_60W$8>28G?}HS#3!@YYiyUw>HeR;;4@mxf`WfiQPZi7&eq1>8yK&epjvMUlj$OBG ZTk1jumLW3B-P&S#x3y~^pX)F={15wE{5}8x literal 0 HcmV?d00001 diff --git a/docs/build/.doctrees/double_negation_elimination.doctree b/docs/build/.doctrees/double_negation_elimination.doctree new file mode 100644 index 0000000000000000000000000000000000000000..9a502242ea6e0e8d37eb9a6655a9cdadaed8bfe5 GIT binary patch literal 2528 zcmai0OK%%D5Kin!viy+kJcX zw1)sSz+2d#*8kIwyQ{UVLu$bAayXpFH{Zzao1Hs>iL*5rVZmR#SLbP zP;%|l$MpQK^gewZhnBu`CfI_fcncbZkcwHZ)7unBS=~$J#_juot2@8)d5-4O${$h_Y`>xi%_p%Rhos9z ztjB(v!fCvtq~_@~OlaJs-di~d9;xS4*Clf~twEuva}eUYr)k-IZLm;XA11Uow|ts) zLL7KH%U4P4iicubJQC~TAijC^^6WRqtvmaPUPyNK`mzwzmanb(9Vof8DrkVEqzUc} zvAVM+Mto;f$O09zgv!`DB=^P18p0P}B4+UzF@6$9D!u~zPyS!+8PuL58}W_UL>B8! z7UIRKyM;Z`KIpI&FXDY~sdlQaAgQdGS?(Had)|1e(#fs3xzOPZ$B_Nqj-w*jTshL! zX?r1Q>J>K}_g?B5Si0ZQZfcG8T(cDWZ>S0=RL9%C3BC$Gor>MlIGl0KE%nAG92iB# zJuNF7wi<^7Ue0mcY>&YzoOZk^NUn6gh2tI~w3jK~of_k{@qFp>%uVHB@?j(4iq{hIPI^HWe1pgKK}*2XxNUi5tS5?JaKN_~Hw9JQu^0FG zTmm&ueQ*nErMRQ0o&`GNz?NQXyzn1)2flFRL!XREPufXhEJZW zs7$uTQ1C5G^X>?O?&t0TZ}bc_%+uGWpZA`{QN=3)P&j(Br~%u~k_koZxi#YF!u!g- zJUW8djjKy9j2;_1J4*3E)~o}7Ch@#Pc|6Lo0r}yRZ@&kgBReft%xB59`KJr>XjPgC zd(Q1xazCwop#6`8FBO~(J)NM3m>20}BOZW}CFz>8OMtj4Gvq4nxl8TooCrA+3cq0Q z9c41{w_QomW`6{9wF6N1>T`1>$`rJP_8`x2TA=Vvw*loELcBf?6g92LTgqKt*g7uxp zY#sJ~yMRGfHEo94Rb1!#B5%C7(F_xGFQ_OrlV}c4Jhd~9;e-{jkDx#;kEIUUu)N>i zW8B@4HaievSetf-er_SGPsj&Z*nEp)apdAK3;bn;2;V1heC5Pr{5=xeF77NBtA4#x zNR&Lghs8#cdvc-Igt;tf^bkCXTTYDX>R+qgUlDfN!y6Wd3$OK~yEp7(xLTj5`GZwk z?G1JsCPraGo(Cyz6-FrliyW{s2CrKAM5tvi6`v)uFUe$iv}C~$LMCC}WGQXYAOQ(WlMWpLg)|ZqJbw0lV|)DUhnHE3 zkb)3urn;00j6f=__}2abT|^OTg^DUwmG~d{UUgBcR_&Mm&h@i>pXWWlNmHa&BGOF8 zcRBa$=bm%V^`W=^G}kBo@x4LQwA{^k%`jZgU_s1B4Ns36%njo=<5MrkFU7Nb%-1#o zFY+VQ0 z?*xaBB2J@|Trf5pt^Ba+)RfA9q8L6J) z)s?_&FeTV>Lk-|{u|}!;UL%<>h%lL z*wkc(Emx>}YPiswm6mQyx6490+vrZiEZ-v#;DbSEz)D!RD05}1NR9jNk3Vx14A+%P{BCV8#!trxy4{8%|$iAf)KXVR?c?#g;U+LiU1FSZ%$C%ZRR z^W~oO$R;}pMgCP8O0+mN9a{WBuf^|U(a&?iBNm#!Oj*wF=_N?tS~Yh{@{a{cCf~Uv zlkW<@qq`&pU`dpJzjaamwTu;+BW@R^-QVBWcT>{rNs}zjDKP)fWoXIbq{V;ewYXHA z#}jeFDs6G;^4y+QY2OJ3w2Lzz$|RZ(RrrxI@VP|oQv_IC5j$PMc4?pXJ%CcilWubT z(#^`XoGe+W)8=9Ocn`E>xzhSOcCo%xw0D<_wxgZe-^8f}*=9qzY_p*XKiW;U1#`8Z zBgnTb+^apf(oMJw`)C*bAcCo%xy2ldf8dlKBaEp=Deii2x z|%YX zEL%?4@S>W-RF|!a6km44E8~T$5x=V?|B^k)mhARqe*ip%4&(yQhARAU$?=lVe@#Gc zS?C}3U|Bbz{|@_ZO6a9j$%3DOAm8tSl`ME#|Fd1J-zoS!XDQyg`EYW%j(PuSQDyjP zE90SSo4AV0cXob)ZrW9^Ud?loYKIIVPlm(>Dj4J&l#Uxp@+8UvO7f)Pry`H4Mncaj zJpIh_J^NqaS$F*@X3OL%|B>wwX~@A=8sd2Rn)(8rCgmAd-^Jp)9@BJ_$P7)^MxR1O zBh*un!UakcD5kg3skqXmq%yBO?)iX+(hKS|a{{^){C1wC%zk>~$Cpnj0nWjxRMFXB zijJC3R?cbLPjX48YF=n6*(^#wA@du-1L9E0Gw(b!pi_U+I<@nmZTsazJ(P)BY|GZ9 zN6+6iUR4(Ao)@CHz!sVdD^1S_QtJ7$XYW@{%{6MCw?>Jv!;DqbvQTddP@fX6Y-LVq z&MRN3ezoYvuKwV2dHpZTOV}}Lg;$@4oIbt&?&p^E8Cce**MA7xl49)Mfp#B>V(fmh zJQvPRr5c~86iaT8pLy>1O_<{~HTBQ^=cHr5SU5JXA<+ZCxi||XX_biY(W20c7yJ1T zu(DA1yf1YS)dZa?d53Bb?|^bC%9qJA!HbBo_HBg7VVl^%N8v_1XPp^12A;pdM^j%S zVP0fd_YfQkk_6=8^Rhq1p9j)+w?+mhBLc^>z_i#}IWw6quPWDOgh8qep>M4|hz8H!DZ0 zF=xjVq}HZrwd~wZd42&?dxcgXwyza7nOT{Te|*u8bf!Eh0@9pv#nB8rl=;dNRz1K2 zT=?xdJhT|f;_LIRRU@m_MgnXaoq8hSpFXP%e5w=;6?Fs3kK) zoQ+E8oI+NTzssDtNpd7Z@QO^T@PUusD_^jGCo{@7^vk|#$BB6@`|jPaG}Y?eEzY(5 zl>()?vnt-I$>i~*WD};sgY?hulD^iafZWc>T}r+LwEZ^W3=ftnN6A_&8<;EQGoAx> zs#ZC~+q!99&eozhdwJ5tE@f9}p9Ym#sQ3>ff|iCD`#3?%0*!qyu}}nw=jgA)_Er2R zJ8%kB=W{ol!XZC?g?1!<{0MfY-cLrJPu66Qo0Cx-FY)PcqdC{w9`TY#`yA-b2mOq0 zQd)YV8caO8@XvVW?ylw8L%uo34~Fn`fs<4bnm*zO3zCQYq0kF8CtmF1FTGJ+5wM$`=}G}W}Z0VlRL zw7MOZ_$2ZfL>JXz>xgfQ1AN@noa}Rm&#+AkTtl`K1?i$8K4h?3w2I@V=^2(DsR5U1 z4UCL|{W>GO@j8naS@1|jYL~3qGB|&2bpko9E7d`8*J4pDFC-`-liATVR4m4v32Rl%u(; zk+#afas%H3=zrk{e5QN8p&E={>~W3-Jz3(zxNg)zCs<+`Dw4*!wHceke44J7YCgmV z=zck6M2)7J=^!{O22jLcK3)_F;9fBzw43Cg4>bc88J@b?Af4KWcXBUas=QOEi5{x! zRzPZOL(mM! zd;*O^*(Y>#h71g<ACZszj`L-hiIih04r5I$U;1*mhe%GS5KV15B!|=>v{n^jpX3(Nx{QfHPYEN z=FeL!tcx??0nV6V!@*%=p;m(#8KD_3j`E{W%7&WW74s9+ph+6C&G(6Rl}**eYauR8 zCKPy&l}m^8<7s^$h#TR|HY5u+D0b@;V;wk%SU;My*jlMx(|I*zgumFd2F&w)r6) ztJYM8mJCNlXBc@}i2eqjY4vtNS)F>~*S7f}bJwZEin5v{K_XSO@FEW52-T!RLnzJ+ zkb-K3aIjDtv^J3c=KI@5lb$OK16n=(uzvw-z82e*%xQtBqf+zMORg3 zPq5hjJ${*Qn6KM^L#}WCg??S6@rURaK@||}-_l>d!LNvq5e#ZT5y3@3**4$U767)z z=54X@hS;yL(I356DX}pPN18ise1_}Ok!(P}V?LpKXu1%+V~BqvkF>_$B(aVT_Vq0e1h2+V z!<^B72FHNDyZ{PJ2UAuy9c&>5X{5thaL#+>vQ(;-=T-Ra&rtWFf@FvJWLBt?dQ`~t z!}Riu8a(-uCIT{iY4O1%<9Z%x;jP2M?vu$zGOq!%|Qm=DRpmHT>dePuwdJ|Nqli8iOo*B>1Ec0f3 zP*rM$Dq``}O6^os&`SLV5<)`Ia#x^2i;$4`#PtCoMXLA$LKR5BH-7&&JIBuM&f0`Z zAT^R5&pZG3_5M%wzxc~jJLEsHmp2U4S)bE%-EnosLouYg)u7HCKYSrP@pSlPI3tEV zZH>EuS7o8tffZH5v~`a;;l)sl({kUm`CN1VAZJzIbe&|o(QgbGgBQaYV_5Y2rf;*% zl$bOf-*fdq?kRf#W@$0j?tYl96A+!2JQGHc4Ky^s;fKbg7*-R&jXp8Zgm+QwwoQkH zi$O&bBbx7fW+m`}C*jp+>YQ*GtlApq7{uTGj#iKU8q$MC`ccuUD;}%Snm`Qt+A>Xr z#$IFE7&Q(Uea1m?-<|VIk8tMkrMt9MQ(wA&qiSeg{eI82KoY*x2pnK(n{L3D04raL zU|h;lKqU&yc^oL+u&^tr7<(cfq(q#E2gJx-tY$i`j^XDxeog={<7SCZIa+Sa0)&2mFf4{aW^LKi8b+3N&z^IXlUd*;`%Wq* zS2RbN2a5BTOsB@cp(>MzT~d5Q^A*ju-8HWGuA(!~TxE);)LgF~*jkzUn$Jl36t|{u zx6Ty4;rJTpR+Vd%n&;M|37xQKO2cDy6U>{Fax-I;L?7S^Q|xcgVh?17SiNCr+~iqY z_H{rc62wx0{DHQg$evzI+k3J6cF?mV2AeeM3gr$l+F*`uI?L)hq%I5T{*Hu=m1e+n zq`b$v3%R+}l#TILUS#gpyW=n;c1r+6ANO@=3VxTt*pTG~rvl_2FOn`X07PhOD?O!L zgfKBQS=US_G+Z%=FMp!}bJHhx?7=r%Z`fwl^utX#y{36icv{y}FeKZ54RKB2+ZV)3<&?7b1Vx7&6W;A#Nm^Lj^qQM15SMM;0PbtN^PF2p6P zrlSzv9~Xf`i(_@6#Xsz|`1@G&os`*dfW{AEQj0?o^T0Yw`exTDX5C+Ntc$)=)Ri@k;!sy40L|C2%aqGXz^cqEiUBT(TH=p z$vbjRwc$YWnr9sb>a841hY}{HLnU#r@cfjS)(JXUMuDAztSu^{brVi0qDnWGesH@i z?SWU8uj9tFb)*MeS=Q3}Lt9v1$lYT-xa*nAMmu{S!nHZ}CPOKElcAEhp(}gk1sVQ6 zMn_*Ye=qc)OE>;9?Aw;g_ChSnU}P}XBRv4iGMLssu!Z%7435>;4JtNM9k#5I=WI2; zBRR(@jx?pBXj8N&ajw=TAeAza3P3Vc5(o5xvoh>|mQJ~9_J6Sl)w;3&CG6W4`-{=a zGJgWh{6Y_~vdpLTpWnjzcIKx6Z9XIu15xA^ik&BA4*FU%947xR|ICg-Qy@wh`ZRCE$wTu60Vi zyCmFm$~~@!^N^S$i=UOJXQG?-o0OR=m%n=cgu-zTZl!#GjVV=B1d?RGWk2yHo~pRM zp(L{?4EW5e^V{U58C%_cDW_Y%*1Wazr7iojm%1n-G|85%iLai!aipxw*Id^}=E>$8 z^OqW~2cXomr%&Ii8k(b5Tz7@CCY$NYsC1wj!BM@C=Iqj}(wI{|T>ePjl3n=9`~3P} z=9koCRFW<{4nAFZ>gD$}>pjq{D^I-w-O4!GKO`0}ilI@eniK0{Tqis3m2|9HU1@tuLOoq~!GZ`w0iTsfn zj-E+CyqYv}4yP1xw_BWf8}@B0&TL181T8MPPD5&L?g2_xFlqhqEv!duX&uG7D4rr- zwib0t5$9Tq!I$zrSQORKQ(mfc5wSPrWinK1t2n3PsV4wl4JWl8~6!XAHg75Z;<7Jki|Iy2~DinEv9LRGgg*HB+Ue9EHW%w zY|QDbe8rqBLxFi3y~C{F5l=pcZNw(3bug8KS3rpE1^!=7c1SaI2*BV04neVx#}Vdb z{9k0W=tV1blWmjo&DGW_%x;^4Q)%&o-%alAB(b>^#d@7qPg~#0Z8DNFw|MIgFQ_u* zei<*%Dv#Ql4pZtW_n9@02W09QYX|{6Sp|rIGm-{X*J%e`;rpvogir?!bs#;X4;Po$FA_2#R^3#QtMQM_Si zHk4|+F@1+Qx)qYfQoXgsskHwthiMv1<&%EWJG_Tl1SupOvN*Rz{F<9MZ92Y1&KDeQ z{h44!fE5cz!CEZaHCsq$JY}_uR`H3~c9Xo6ta)~JHeTt;dwnx%{*7`c_h{DXn*cn^DEbwBqlC`)g z8u{^pkP~J!rCRF?bkuZ`p4y=!CBZy)7kz2)L0uXtrg=F}8c~c{ag7gK$L%PXY zj7NpqD_>I617mdA(Vi@L;c^WKkhz}T2hGI{>fsZ}Wg?JNn zR`5B}{0uxBUt_*oRjDn8W^r*pAoMoEOwyK4B3T-vz91*4tLxP3LFv;tM>kGGt-5t; z_~1BlIvRl!kR$4v=^JX?oP!&i8=BoZi((W77x)*v_N>CgE$k8_hGr+9{bG`>o1hxX zF#(Sk^^1O;Rf1()H%?6i)MJ5jnO4WhFvwqJ1UGsM5EOw%Dtw1aofv3R2>e?4)-pHo z_kq?)m3f})$%>E-Ck?g(woYF5(3B|$OOzsHlQ+){H#-npn7zV11GiN_^ z767!)Rb5Y4bw&**xW|N?EQ$dH z95vtxl9;-Rs#eWh4~+paPPwm|4vAfq0FUWGy`d&D2+GONJYc) zvF0+hW}*;EO~7(~Zeh9puh=!c)2I4;H; ztdZ6v2pRP2G@uQDowP$-XZU`D&!0MlVLsQ`@D10QbG_wLq1aC=B>-5dqMZQjK{;0p zVZ40o^ev$0xL2#@j;E3I_?zP6p{*Lp>*O?6z804LqB#F)$x0FGvC3ZG80otNEEBPG(UTiVVDyH;-*uz1D%}T TG6gW`2}RV_3~-32L1pgWv4U8P literal 0 HcmV?d00001 diff --git a/docs/build/_sources/biconditional_elimination_left.rst.txt b/docs/build/_sources/biconditional_elimination_left.rst.txt new file mode 100644 index 000000000..a2e62cb79 --- /dev/null +++ b/docs/build/_sources/biconditional_elimination_left.rst.txt @@ -0,0 +1,2 @@ +biconditional-elimination-left +=============================== \ No newline at end of file diff --git a/docs/build/_sources/biconditional_elimination_right.rst.txt b/docs/build/_sources/biconditional_elimination_right.rst.txt new file mode 100644 index 000000000..50c67e6f1 --- /dev/null +++ b/docs/build/_sources/biconditional_elimination_right.rst.txt @@ -0,0 +1,2 @@ +biconditional-elimination-right +=============================== \ No newline at end of file diff --git a/docs/build/_sources/biconditional_introduction.rst.txt b/docs/build/_sources/biconditional_introduction.rst.txt new file mode 100644 index 000000000..1a14ce718 --- /dev/null +++ b/docs/build/_sources/biconditional_introduction.rst.txt @@ -0,0 +1,2 @@ +biconditional-introduction +=============================== \ No newline at end of file diff --git a/docs/build/_sources/conjunction_elimination_left.rst.txt b/docs/build/_sources/conjunction_elimination_left.rst.txt new file mode 100644 index 000000000..9f5ee24c5 --- /dev/null +++ b/docs/build/_sources/conjunction_elimination_left.rst.txt @@ -0,0 +1,2 @@ +conjunction-elimination-left +=============================== \ No newline at end of file diff --git a/docs/build/_sources/conjunction_elimination_right.rst.txt b/docs/build/_sources/conjunction_elimination_right.rst.txt new file mode 100644 index 000000000..3a59b13ca --- /dev/null +++ b/docs/build/_sources/conjunction_elimination_right.rst.txt @@ -0,0 +1,2 @@ +conjunction-elimination-right +=============================== \ No newline at end of file diff --git a/docs/build/_sources/double_negation_elimination.rst.txt b/docs/build/_sources/double_negation_elimination.rst.txt new file mode 100644 index 000000000..cd55ee472 --- /dev/null +++ b/docs/build/_sources/double_negation_elimination.rst.txt @@ -0,0 +1,2 @@ +double-negation-elimination +=============================== \ No newline at end of file diff --git a/docs/build/_sources/elimination_rule.rst.txt b/docs/build/_sources/elimination_rule.rst.txt new file mode 100644 index 000000000..1ee0901f5 --- /dev/null +++ b/docs/build/_sources/elimination_rule.rst.txt @@ -0,0 +1,28 @@ +elimination-rule +================== + +Definition +---------- + +An *introduction-rule* is an :doc:`inference_rule` that allows to derive a formula-statement of some syntactic form from some define premises. + +List of well-known *introduction-rules* +-------------------------------------- + +* :doc:`biconditional_elimination_left` +* :doc:`biconditional_elimination_right` +* :doc:`conjunction_elimination_left` +* :doc:`conjunction_elimination_right` +* :doc:`disjunction_elimination` +* :doc:`double_negation_elimination` + +Quotes +------- + + "Each of the introduction rules tells us how to derive a formula of some syntactic form. For instance, the conjunction introduction rule (∧I) shows that we can derive a conjunction if we derive both conjunctive terms; the disjunction introduction rules (∨I) show that we can derive a disjunction if we derive one of the disjunctive terms." + - :footcite:p:`porter_2008_handbookknowledgerepresentation`, p. 6-7 + +Bibliography +------------ + +.. footbibliography:: diff --git a/docs/build/_sources/introduction_rule.rst.txt b/docs/build/_sources/introduction_rule.rst.txt new file mode 100644 index 000000000..8266c3a0f --- /dev/null +++ b/docs/build/_sources/introduction_rule.rst.txt @@ -0,0 +1,33 @@ +introduction-rule +================== + +Definition +---------- + +An *introduction-rule* is an :doc:`inference_rule` that allows to derive a formula-statement of some syntactic form from some define premises. + +List of well-known *introduction-rules* +-------------------------------------- + +* :doc:`biconditional_introduction` +* :doc:`conjunction_introduction` +* :doc:`disjunction_introduction_left` +* :doc:`disjunction_introduction_right` +* :doc:`double_negation_introduction` + +Quotes +------- + + "Each of the introduction rules tells us how to derive a formula of some syntactic form. For instance, the conjunction introduction rule (∧I) shows that we can derive a conjunction if we derive both conjunctive terms; the disjunction introduction rules (∨I) show that we can derive a disjunction if we derive one of the disjunctive terms." + - :footcite:p:`porter_2008_handbookknowledgerepresentation`, p. 6-7 + +See also +--------- + +* :doc:`elimination_rule` +* :doc:`inference_rule` + +Bibliography +------------ + +.. footbibliography:: diff --git a/docs/build/biconditional_elimination_left.html b/docs/build/biconditional_elimination_left.html new file mode 100644 index 000000000..6d60a033f --- /dev/null +++ b/docs/build/biconditional_elimination_left.html @@ -0,0 +1,231 @@ + + + + + + + + +biconditional-elimination-left | punctilious 1.0.0 documentation + + + + + + + +

+Skip to content +
+
+ +
+
+
+ +
+
+
+

biconditional-elimination-left

+
+
+
+ +
+ + + + + + \ No newline at end of file diff --git a/docs/build/biconditional_elimination_right.html b/docs/build/biconditional_elimination_right.html new file mode 100644 index 000000000..24857aa85 --- /dev/null +++ b/docs/build/biconditional_elimination_right.html @@ -0,0 +1,231 @@ + + + + + + + + +biconditional-elimination-right | punctilious 1.0.0 documentation + + + + + + + +
+Skip to content +
+
+ +
+
+
+ +
+
+
+

biconditional-elimination-right

+
+
+
+ +
+ + + + + + \ No newline at end of file diff --git a/docs/build/biconditional_introduction.html b/docs/build/biconditional_introduction.html new file mode 100644 index 000000000..352ed4c8e --- /dev/null +++ b/docs/build/biconditional_introduction.html @@ -0,0 +1,231 @@ + + + + + + + + +biconditional-introduction | punctilious 1.0.0 documentation + + + + + + + +
+Skip to content +
+
+ +
+
+
+ +
+
+
+

biconditional-introduction

+
+
+
+ +
+ + + + + + \ No newline at end of file diff --git a/docs/build/conjunction_elimination_left.html b/docs/build/conjunction_elimination_left.html new file mode 100644 index 000000000..2776d0a17 --- /dev/null +++ b/docs/build/conjunction_elimination_left.html @@ -0,0 +1,233 @@ + + + + + + + + +conjunction-elimination-left | punctilious 1.0.0 documentation + + + + + + + + + +
+Skip to content +
+
+ +
+
+
+ +
+
+
+

conjunction-elimination-left

+
+
+
+ +
+ + + + + + \ No newline at end of file diff --git a/docs/build/conjunction_elimination_right.html b/docs/build/conjunction_elimination_right.html new file mode 100644 index 000000000..7f151326d --- /dev/null +++ b/docs/build/conjunction_elimination_right.html @@ -0,0 +1,233 @@ + + + + + + + + +conjunction-elimination-right | punctilious 1.0.0 documentation + + + + + + + + + +
+Skip to content +
+
+ +
+
+
+ +
+
+
+

conjunction-elimination-right

+
+
+
+ +
+ + + + + + \ No newline at end of file diff --git a/docs/build/double_negation_elimination.html b/docs/build/double_negation_elimination.html new file mode 100644 index 000000000..155fc65ef --- /dev/null +++ b/docs/build/double_negation_elimination.html @@ -0,0 +1,233 @@ + + + + + + + + +double-negation-elimination | punctilious 1.0.0 documentation + + + + + + + + + +
+Skip to content +
+
+ +
+
+
+ +
+
+
+

double-negation-elimination

+
+
+
+ +
+ + + + + + \ No newline at end of file diff --git a/docs/build/elimination_rule.html b/docs/build/elimination_rule.html new file mode 100644 index 000000000..29e8e820d --- /dev/null +++ b/docs/build/elimination_rule.html @@ -0,0 +1,266 @@ + + + + + + + + +elimination-rule | punctilious 1.0.0 documentation + + + + + + + + + +
+Skip to content +
+
+ +
+
+
+ +
+
+
+

elimination-rule

+
+

Definition

+

An introduction-rule is an inference-rule that allows to derive a formula-statement of some syntactic form from some define premises.

+
+
+

List of well-known introduction-rules

+ +
+
+

Quotes

+
+

“Each of the introduction rules tells us how to derive a formula of some syntactic form. For instance, the conjunction introduction rule (∧I) shows that we can derive a conjunction if we derive both conjunctive terms; the disjunction introduction rules (∨I) show that we can derive a disjunction if we derive one of the disjunctive terms.” +- [1], p. 6-7

+
+
+
+

Bibliography

+
+ +
+
+
+
+
+ +
+ + + + + + \ No newline at end of file diff --git a/docs/build/introduction_rule.html b/docs/build/introduction_rule.html new file mode 100644 index 000000000..67be83c1a --- /dev/null +++ b/docs/build/introduction_rule.html @@ -0,0 +1,272 @@ + + + + + + + + +introduction-rule | punctilious 1.0.0 documentation + + + + + + + + + +
+Skip to content +
+
+ +
+
+
+ +
+
+
+

introduction-rule

+
+

Definition

+

An introduction-rule is an inference-rule that allows to derive a formula-statement of some syntactic form from some define premises.

+
+
+

List of well-known introduction-rules

+ +
+
+

Quotes

+
+

“Each of the introduction rules tells us how to derive a formula of some syntactic form. For instance, the conjunction introduction rule (∧I) shows that we can derive a conjunction if we derive both conjunctive terms; the disjunction introduction rules (∨I) show that we can derive a disjunction if we derive one of the disjunctive terms.” +- [1], p. 6-7

+
+
+
+

See also

+ +
+
+

Bibliography

+
+ +
+
+
+
+
+ +
+ + + + + + \ No newline at end of file