Skip to content

Commit 5dd93c8

Browse files
committed
readme: link FitchFX-formatted natural deduction proofs of C-N 1-bases
+ spelling
1 parent 097551e commit 5dd93c8

File tree

3 files changed

+29
-29
lines changed

3 files changed

+29
-29
lines changed

README.html

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -270,13 +270,13 @@ <h1 id="xamidipmgenerator">@xamidi/pmGenerator</h1>
270270
</li>
271271
<li><a href="#multi-node-computing">Multi-node Computing</a></li>
272272
<li><a href="#custom-proof-systems">Custom Proof Systems</a><ol>
273-
<li><a href="#merediths-axiom-1-basis-cccccpqcnrnsrtcctpcsp-top1000-cardinalities-sample-info">Meredith's Axiom; 1-basis <code>(CCCCCpqCNrNsrtCCtpCsp)</code></a></li>
274-
<li><a href="#walshs-1st-axiom-1-basis-ccpccnpqrcsccntcrtcpt-top1000-cardinalities-sample-info">Walsh's 1st Axiom; 1-basis <code>(CCpCCNpqrCsCCNtCrtCpt)</code></a></li>
275-
<li><a href="#walshs-2nd-axiom-1-basis-cpccqcprccnrccnstqcsr-top1000-cardinalities-sample-info">Walsh's 2nd Axiom; 1-basis <code>(CpCCqCprCCNrCCNstqCsr)</code></a></li>
276-
<li><a href="#walshs-3rd-axiom-1-basis-cpccnqccnrscptcctqcrq-top1000-cardinalities-sample-info">Walsh's 3rd Axiom; 1-basis <code>(CpCCNqCCNrsCptCCtqCrq)</code></a></li>
277-
<li><a href="#walshs-4th-axiom-1-basis-cpccnqccnrsctqccrtcrq-top1000-cardinalities-sample-info">Walsh's 4th Axiom; 1-basis <code>(CpCCNqCCNrsCtqCCrtCrq)</code></a></li>
278-
<li><a href="#walshs-5th-axiom-1-basis-ccpqcccrcstcqcnsnpcps-top1000-cardinalities-sample-info">Walsh's 5th Axiom; 1-basis <code>(CCpqCCCrCstCqCNsNpCps)</code></a></li>
279-
<li><a href="#walshs-6th-axiom-1-basis-cccpqcccnrnsrtcctpcsp-top1000-cardinalities-sample-info">Walsh's 6th Axiom; 1-basis <code>(CCCpqCCCNrNsrtCCtpCsp)</code></a></li>
273+
<li><a href="#merediths-axiom-1-basis-cccccpqcnrnsrtcctpcsp-top1000-cardinalities-nd-sample-info">Meredith's Axiom; 1-basis <code>(CCCCCpqCNrNsrtCCtpCsp)</code></a></li>
274+
<li><a href="#walshs-1st-axiom-1-basis-ccpccnpqrcsccntcrtcpt-top1000-cardinalities-nd-sample-info">Walsh's 1st Axiom; 1-basis <code>(CCpCCNpqrCsCCNtCrtCpt)</code></a></li>
275+
<li><a href="#walshs-2nd-axiom-1-basis-cpccqcprccnrccnstqcsr-top1000-cardinalities-nd-sample-info">Walsh's 2nd Axiom; 1-basis <code>(CpCCqCprCCNrCCNstqCsr)</code></a></li>
276+
<li><a href="#walshs-3rd-axiom-1-basis-cpccnqccnrscptcctqcrq-top1000-cardinalities-nd-sample-info">Walsh's 3rd Axiom; 1-basis <code>(CpCCNqCCNrsCptCCtqCrq)</code></a></li>
277+
<li><a href="#walshs-4th-axiom-1-basis-cpccnqccnrsctqccrtcrq-top1000-cardinalities-nd-sample-info">Walsh's 4th Axiom; 1-basis <code>(CpCCNqCCNrsCtqCCrtCrq)</code></a></li>
278+
<li><a href="#walshs-5th-axiom-1-basis-ccpqcccrcstcqcnsnpcps-top1000-cardinalities-nd-sample-info">Walsh's 5th Axiom; 1-basis <code>(CCpqCCCrCstCqCNsNpCps)</code></a></li>
279+
<li><a href="#walshs-6th-axiom-1-basis-cccpqcccnrnsrtcctpcsp-top1000-cardinalities-nd-sample-info">Walsh's 6th Axiom; 1-basis <code>(CCCpqCCCNrNsrtCCtpCsp)</code></a></li>
280280
<li><a href="#s5-cpcqpccpcqrccpqcprccnpnqcqpclppclcpqclplqcnlnplnlnp-top1000-cardinalities-db-sample-info">S5 <code>(CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp)</code></a></li>
281281
</ol>
282282
</li>
@@ -627,7 +627,7 @@ <h4 id="custom-proof-systems">Custom Proof Systems</h4>
627627
<p>There are illustrated seven proof systems in the following which according to <a href="http://fitelson.org/walsh.pdf">M. Walsh and B. Fitelson</a> are minimal 1-bases (i.e. generators consisting of shortest single axioms) for propositional logic.
628628
Their only remaining candidate CCCpqCCrNsCtNtCCtpCrp can be refuted since <code>pmGenerator -c -n -s CCCpqCCrNsCtNtCCtpCrp -g -1</code> produces only 9 more representatives (1.<code>D11:CCpCNpqCrCNpq</code>, 2.<code>D1D11:CCNppCqp</code>, 3.<code>D1D1D11:CCpNCpNpCqNCpNp</code>, 4.<code>DD11D11:CpCNCqCNqrCNqr</code>, 5.<code>DD11D1D11:CpCNCNqqq</code>, 6.<code>DDD11D111:CNCpCNpqCNpq</code>, 7.<code>DD11D1D1D11:CpCNCqNCqNqNCqNq</code>, 8.<code>DDD11D1D111:CNCNppp</code>, 9.<code>DDD11D1D1D111:CNCpNCpNpNCpNp</code>).<br>Therefore, these systems are implied to be the only minimal 1-bases for C-N propositional calculus.</p>
629629
<p>Target files are distinguished using a hexadecimal SHA-512/224 digest as a folder name for each proof system.<br>For user identification of hash folders, I recommend to use custom icons, such as illustrated below.<br>&nbsp;&nbsp;<sub><img src="png/customIconPreview.png" alt="Icon-Preview" title="Hash folders with icons under Windows 7"></sub><br>For this purpose, a favicon database (<code>ico.dll</code>) is included in the release files, as well as an archive (<code>ico.7z</code>) with all the <code>.ico</code> files for usability with non-Windows operating systems.</p>
630-
<h6 id="merediths-axiom-1-basis-cccccpqcnrnsrtcctpcsp-top1000-cardinalities-sample-info">Meredith's Axiom; 1-basis (<a href="svg/meredith.svg">CCCCCpqCNrNsrtCCtpCsp</a>) &nbsp;<small>[<a href="data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/top1000SmallestConclusions_1to83Steps.txt">top1000</a>] [<a href="data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/cardinalities.txt">cardinalities</a>] [<a href="data/m.txt">sample</a>] [<a href="data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/!.def">info</a>]</small></h6>
630+
<h6 id="merediths-axiom-1-basis-cccccpqcnrnsrtcctpcsp-top1000-cardinalities-nd-sample-info">Meredith's Axiom; 1-basis (<a href="svg/meredith.svg">CCCCCpqCNrNsrtCCtpCsp</a>) &nbsp;<small>[<a href="data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/top1000SmallestConclusions_1to83Steps.txt">top1000</a>] [<a href="data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/cardinalities.txt">cardinalities</a>] [<a href="data/m_ffx.txt">nd</a>] [<a href="data/m.txt">sample</a>] [<a href="data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/!.def">info</a>]</small></h6>
631631
<details open><summary>Behavioral Graph<sup></sup> <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture> &nbsp;<small>[<a href="svg/plot/m-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/m-plot_data_x200.txt">raw</a>]</small></summary>
632632
<a href="https://xamidi.github.io/pmGenerator/svg/plot/m-bgraph.svg"><img src="svg/plot/m-bgraph.svg" alt="m-bgraph.svg" width="700"></a></details>
633633
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture></summary>
@@ -721,7 +721,7 @@ <h6 id="merediths-axiom-1-basis-cccccpqcnrnsrtcctpcsp-top1000-cardinalities-samp
721721

722722
</details>
723723

724-
<h6 id="walshs-1st-axiom-1-basis-ccpccnpqrcsccntcrtcpt-top1000-cardinalities-sample-info">Walsh's 1st Axiom; 1-basis (<a href="svg/walsh1st.svg">CCpCCNpqrCsCCNtCrtCpt</a>) &nbsp;<small>[<a href="data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/top1000SmallestConclusions_1to161Steps.txt">top1000</a>] [<a href="data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/cardinalities.txt">cardinalities</a>] [<a href="data/w1.txt">sample</a>] [<a href="data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/!.def">info</a>]</small></h6>
724+
<h6 id="walshs-1st-axiom-1-basis-ccpccnpqrcsccntcrtcpt-top1000-cardinalities-nd-sample-info">Walsh's 1st Axiom; 1-basis (<a href="svg/walsh1st.svg">CCpCCNpqrCsCCNtCrtCpt</a>) &nbsp;<small>[<a href="data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/top1000SmallestConclusions_1to161Steps.txt">top1000</a>] [<a href="data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/cardinalities.txt">cardinalities</a>] [<a href="data/w1_ffx.txt">nd</a>] [<a href="data/w1.txt">sample</a>] [<a href="data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/!.def">info</a>]</small></h6>
725725
<details open><summary>Behavioral Graph<sup></sup> <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture> &nbsp;<small>[<a href="svg/plot/w1-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/w1-plot_data_x400.txt">raw</a>]</small></summary>
726726
<a href="https://xamidi.github.io/pmGenerator/svg/plot/w1-bgraph.svg"><img src="svg/plot/w1-bgraph.svg" alt="w1-bgraph.svg" width="700"></a></details>
727727
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture></summary>
@@ -847,7 +847,7 @@ <h6 id="walshs-1st-axiom-1-basis-ccpccnpqrcsccntcrtcpt-top1000-cardinalities-sam
847847

848848
</details>
849849

850-
<h6 id="walshs-2nd-axiom-1-basis-cpccqcprccnrccnstqcsr-top1000-cardinalities-sample-info">Walsh's 2nd Axiom; 1-basis (<a href="svg/walsh2nd.svg">CpCCqCprCCNrCCNstqCsr</a>) &nbsp;<small>[<a href="data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/top1000SmallestConclusions_1to43Steps.txt">top1000</a>] [<a href="data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/cardinalities.txt">cardinalities</a>] [<a href="data/w2.txt">sample</a>] [<a href="data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/!.def">info</a>]</small></h6>
850+
<h6 id="walshs-2nd-axiom-1-basis-cpccqcprccnrccnstqcsr-top1000-cardinalities-nd-sample-info">Walsh's 2nd Axiom; 1-basis (<a href="svg/walsh2nd.svg">CpCCqCprCCNrCCNstqCsr</a>) &nbsp;<small>[<a href="data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/top1000SmallestConclusions_1to43Steps.txt">top1000</a>] [<a href="data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/cardinalities.txt">cardinalities</a>] [<a href="data/w2_ffx.txt">nd</a>] [<a href="data/w2.txt">sample</a>] [<a href="data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/!.def">info</a>]</small></h6>
851851
<details open><summary>Behavioral Graph<sup></sup> <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture> &nbsp;<small>[<a href="svg/plot/w2-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/w2-plot_data_x6000.txt">raw</a>]</small></summary>
852852
<a href="https://xamidi.github.io/pmGenerator/svg/plot/w2-bgraph.svg"><img src="svg/plot/w2-bgraph.svg" alt="w2-bgraph.svg" width="700"></a></details>
853853
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture></summary>
@@ -909,7 +909,7 @@ <h6 id="walshs-2nd-axiom-1-basis-cpccqcprccnrccnstqcsr-top1000-cardinalities-sam
909909

910910
</details>
911911

912-
<h6 id="walshs-3rd-axiom-1-basis-cpccnqccnrscptcctqcrq-top1000-cardinalities-sample-info">Walsh's 3rd Axiom; 1-basis (<a href="svg/walsh3rd.svg">CpCCNqCCNrsCptCCtqCrq</a>) &nbsp;<small>[<a href="data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/top1000SmallestConclusions_1to73Steps.txt">top1000</a>] [<a href="data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/cardinalities.txt">cardinalities</a>] [<a href="data/w3.txt">sample</a>] [<a href="data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/!.def">info</a>]</small></h6>
912+
<h6 id="walshs-3rd-axiom-1-basis-cpccnqccnrscptcctqcrq-top1000-cardinalities-nd-sample-info">Walsh's 3rd Axiom; 1-basis (<a href="svg/walsh3rd.svg">CpCCNqCCNrsCptCCtqCrq</a>) &nbsp;<small>[<a href="data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/top1000SmallestConclusions_1to73Steps.txt">top1000</a>] [<a href="data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/cardinalities.txt">cardinalities</a>] [<a href="data/w3_ffx.txt">nd</a>] [<a href="data/w3.txt">sample</a>] [<a href="data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/!.def">info</a>]</small></h6>
913913
<details open><summary>Behavioral Graph<sup></sup> <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture> &nbsp;<small>[<a href="svg/plot/w3-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/w3-plot_data_x1000.txt">raw</a>]</small></summary>
914914
<a href="https://xamidi.github.io/pmGenerator/svg/plot/w3-bgraph.svg"><img src="svg/plot/w3-bgraph.svg" alt="w3-bgraph.svg" width="700"></a></details>
915915
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture></summary>
@@ -987,7 +987,7 @@ <h6 id="walshs-3rd-axiom-1-basis-cpccnqccnrscptcctqcrq-top1000-cardinalities-sam
987987

988988
</details>
989989

990-
<h6 id="walshs-4th-axiom-1-basis-cpccnqccnrsctqccrtcrq-top1000-cardinalities-sample-info">Walsh's 4th Axiom; 1-basis (<a href="svg/walsh4th.svg">CpCCNqCCNrsCtqCCrtCrq</a>) &nbsp;<small>[<a href="data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/top1000SmallestConclusions_1to169Steps.txt">top1000</a>] [<a href="data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/cardinalities.txt">cardinalities</a>] [<a href="data/w4.txt">sample</a>] [<a href="data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/!.def">info</a>]</small></h6>
990+
<h6 id="walshs-4th-axiom-1-basis-cpccnqccnrsctqccrtcrq-top1000-cardinalities-nd-sample-info">Walsh's 4th Axiom; 1-basis (<a href="svg/walsh4th.svg">CpCCNqCCNrsCtqCCrtCrq</a>) &nbsp;<small>[<a href="data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/top1000SmallestConclusions_1to169Steps.txt">top1000</a>] [<a href="data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/cardinalities.txt">cardinalities</a>] [<a href="data/w4_ffx.txt">nd</a>] [<a href="data/w4.txt">sample</a>] [<a href="data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/!.def">info</a>]</small></h6>
991991
<details open><summary>Behavioral Graph<sup></sup> <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture> &nbsp;<small>[<a href="svg/plot/w4-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/w4-plot_data_x1250.txt">raw</a>]</small></summary>
992992
<a href="https://xamidi.github.io/pmGenerator/svg/plot/w4-bgraph.svg"><img src="svg/plot/w4-bgraph.svg" alt="w4-bgraph.svg" width="700"></a></details>
993993
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture></summary>
@@ -1097,7 +1097,7 @@ <h6 id="walshs-4th-axiom-1-basis-cpccnqccnrsctqccrtcrq-top1000-cardinalities-sam
10971097

10981098
</details>
10991099

1100-
<h6 id="walshs-5th-axiom-1-basis-ccpqcccrcstcqcnsnpcps-top1000-cardinalities-sample-info">Walsh's 5th Axiom; 1-basis (<a href="svg/walsh5th.svg">CCpqCCCrCstCqCNsNpCps</a>) &nbsp;<small>[<a href="data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/top1000SmallestConclusions_1to55Steps.txt">top1000</a>] [<a href="data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/cardinalities.txt">cardinalities</a>] [<a href="data/w5.txt">sample</a>] [<a href="data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/!.def">info</a>]</small></h6>
1100+
<h6 id="walshs-5th-axiom-1-basis-ccpqcccrcstcqcnsnpcps-top1000-cardinalities-nd-sample-info">Walsh's 5th Axiom; 1-basis (<a href="svg/walsh5th.svg">CCpqCCCrCstCqCNsNpCps</a>) &nbsp;<small>[<a href="data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/top1000SmallestConclusions_1to55Steps.txt">top1000</a>] [<a href="data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/cardinalities.txt">cardinalities</a>] [<a href="data/w5_ffx.txt">nd</a>] [<a href="data/w5.txt">sample</a>] [<a href="data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/!.def">info</a>]</small></h6>
11011101
<details open><summary>Behavioral Graph<sup></sup> <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture> &nbsp;<small>[<a href="svg/plot/w5-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/w5-plot_data_x30000.txt">raw</a>]</small></summary>
11021102
<a href="https://xamidi.github.io/pmGenerator/svg/plot/w5-bgraph.svg"><img src="svg/plot/w5-bgraph.svg" alt="w5-bgraph.svg" width="700"></a></details>
11031103
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture></summary>
@@ -1151,7 +1151,7 @@ <h6 id="walshs-5th-axiom-1-basis-ccpqcccrcstcqcnsnpcps-top1000-cardinalities-sam
11511151

11521152
</details>
11531153

1154-
<h6 id="walshs-6th-axiom-1-basis-cccpqcccnrnsrtcctpcsp-top1000-cardinalities-sample-info">Walsh's 6th Axiom; 1-basis (<a href="svg/walsh6th.svg">CCCpqCCCNrNsrtCCtpCsp</a>) &nbsp;<small>[<a href="data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/top1000SmallestConclusions_1to95Steps.txt">top1000</a>] [<a href="data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/cardinalities.txt">cardinalities</a>] [<a href="data/w6.txt">sample</a>] [<a href="data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/!.def">info</a>]</small></h6>
1154+
<h6 id="walshs-6th-axiom-1-basis-cccpqcccnrnsrtcctpcsp-top1000-cardinalities-nd-sample-info">Walsh's 6th Axiom; 1-basis (<a href="svg/walsh6th.svg">CCCpqCCCNrNsrtCCtpCsp</a>) &nbsp;<small>[<a href="data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/top1000SmallestConclusions_1to95Steps.txt">top1000</a>] [<a href="data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/cardinalities.txt">cardinalities</a>] [<a href="data/w6_ffx.txt">nd</a>] [<a href="data/w6.txt">sample</a>] [<a href="data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/!.def">info</a>]</small></h6>
11551155
<details open><summary>Behavioral Graph<sup></sup> <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture> &nbsp;<small>[<a href="svg/plot/w6-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/w6-plot_data_x800.txt">raw</a>]</small></summary>
11561156
<a href="https://xamidi.github.io/pmGenerator/svg/plot/w6-bgraph.svg"><img src="svg/plot/w6-bgraph.svg" alt="w6-bgraph.svg" width="700"></a></details>
11571157
<details open><summary>Data <picture><img src="svg/click-cursor.svg" width="20" alt=""></picture></summary>

0 commit comments

Comments
 (0)