readme: refer to exemplary proof parsing and minimal 1-base PMC

Author: xamidi

README.html

@@ -284,7 +284,7 @@ <h1 id="xamidipmgenerator">@xamidi/pmGenerator</h1>
 </ol>
 </details>
 <h4 id="introduction">Introduction</h4>
-<p>This tool can collect exhaustive sets of <a href="https://en.wikipedia.org/wiki/Condensed_detachment">condensed detachment</a> proofs in D-N-notation and has various functions to display, analyze and utilize them. It can, for example, be used to generate improved versions of Metamath's <a href="https://us.metamath.org/mmsolitaire/pmproofs.txt" title="us.metamath.org/mmsolitaire/pmproofs.txt">“Shortest known proofs of the propositional calculus theorems from Principia Mathematica”</a> collection.<br>The D-rule combines <a href="https://en.wikipedia.org/wiki/Unification_(computer_science)">unification</a> with <a href="https://en.wikipedia.org/wiki/Modus_ponens">modus ponens</a> (⊢p,⊢Cpq ⇒ ⊢q), and there is an option to enable the N-rule (rule of necessitation; ⊢p ⇒ ⊢Lp), thus <em>pmGenerator</em> covers all <a href="https://en.wikipedia.org/wiki/Logical_consequence#Syntactic_consequence">syntactic consequences</a> within <a href="https://en.wikipedia.org/wiki/Hilbert_system">Hilbert systems</a> based on modus ponens and necessitation, each with a minimal proof, limited only by computing power.<br>There is a <a href="https://github.com/xamidi/pmGenerator/discussions">discussion forum</a> for questions, ideas, challenges, and related information.</p>
+<p>This tool can collect exhaustive sets of <a href="https://en.wikipedia.org/wiki/Condensed_detachment">condensed detachment</a> proofs in D-N-notation and has various functions to display, analyze and utilize them. It can, for example, be used to generate improved versions of Metamath's <a href="https://us.metamath.org/mmsolitaire/pmproofs.txt" title="us.metamath.org/mmsolitaire/pmproofs.txt">“Shortest known proofs of the propositional calculus theorems from Principia Mathematica”</a> collection.<br>The D-rule combines <a href="https://en.wikipedia.org/wiki/Unification_(computer_science)">unification</a> with <a href="https://en.wikipedia.org/wiki/Modus_ponens">modus ponens</a> (⊢p,⊢Cpq ⇒ ⊢q), and there is an option to enable the N-rule (rule of necessitation; ⊢p ⇒ ⊢Lp), thus <em>pmGenerator</em> covers all <a href="https://en.wikipedia.org/wiki/Logical_consequence#Syntactic_consequence">syntactic consequences</a> within <a href="https://en.wikipedia.org/wiki/Hilbert_system">Hilbert systems</a> based on modus ponens and necessitation, each with a minimal proof, limited only by computing power.<br>There is a <a href="https://github.com/xamidi/pmGenerator/discussions">discussion forum</a> for questions, ideas, challenges, and related information. Numerous use cases of the tool are exemplified, for example <em>proof parsing</em> under the <a href="https://github.com/xamidi/pmGenerator/discussions/2#proof-notation">Proof Notation</a> section of the <a href="https://github.com/xamidi/pmGenerator/discussions/2">“Minimal 1-bases for C-N propositional calculus”</a> proof minimization challenge.</p>
 <p>Eligible for high-performance computing. If you have access to a powerful computer, you may use <em>pmGenerator</em> to further contribute to our knowledge regarding the <a href="https://en.wikipedia.org/wiki/Proof_complexity">complexity of proof systems</a>. Progress that has already been made is exemplarily shown below.</p>
 <h6 id="freges-calculus-simplified-by-łukasiewicz-cpcqpccpcqrccpqcprccnpnqcqp-top1000-cardinalities-db-customization-info">Frege's calculus simplified by Łukasiewicz (<a href="svg/frege-1.svg">CpCqp</a>,<a href="svg/frege-2.svg">CCpCqrCCpqCpr</a>,<a href="svg/lukasiewicz-3.svg">CCNpNqCqp</a>) &nbsp;<small>[<a href="data/top1000SmallestConclusions_1to39Steps.txt">top1000</a>] [<a href="data/cardinalities.txt">cardinalities</a>] [<a href="https://us.metamath.org/mmsolitaire/pmproofs.txt">db</a>] [<a href="data/52436f9e87daeb2c361a73a9f389b061258328e641f750b1767addf7/!.def">customization info</a>]</small></h6>
 <details open><summary>Behavioral Graph<sup>✻</sup> <picture><img src="svg/click-cursor.svg" width="20" alt="☜"></picture> &nbsp;<small>[<a href="svg/plot/default-bgraph_grayscale.svg">grayscale</a>] [<a href="data/plot/default-plot_data_x500.txt">raw</a>]</small></summary>

README.md

@@ -28,7 +28,7 @@
 #### Introduction
 This tool can collect exhaustive sets of [condensed detachment](https://en.wikipedia.org/wiki/Condensed_detachment) proofs in D-N-notation and has various functions to display, analyze and utilize them. It can, for example, be used to generate improved versions of Metamath's [“Shortest known proofs of the propositional calculus theorems from Principia Mathematica”](https://us.metamath.org/mmsolitaire/pmproofs.txt "us.metamath.org/mmsolitaire/pmproofs.txt") collection.  
 The D-rule combines [unification](https://en.wikipedia.org/wiki/Unification_(computer_science)) with [modus ponens](https://en.wikipedia.org/wiki/Modus_ponens) (⊢p,⊢Cpq ⇒ ⊢q), and there is an option to enable the N-rule (rule of necessitation; ⊢p ⇒ ⊢Lp), thus *pmGenerator* covers all [syntactic consequences](https://en.wikipedia.org/wiki/Logical_consequence#Syntactic_consequence) within [Hilbert systems](https://en.wikipedia.org/wiki/Hilbert_system) based on modus ponens and necessitation, each with a minimal proof, limited only by computing power.  
-There is a [discussion forum](https://github.com/xamidi/pmGenerator/discussions) for questions, ideas, challenges, and related information.
+There is a [discussion forum](https://github.com/xamidi/pmGenerator/discussions) for questions, ideas, challenges, and related information. Numerous use cases of the tool are exemplified, for example *proof parsing* under the [Proof Notation](https://github.com/xamidi/pmGenerator/discussions/2#proof-notation) section of the [“Minimal 1-bases for C-N propositional calculus”](https://github.com/xamidi/pmGenerator/discussions/2) proof minimization challenge.
 
 Eligible for high-performance computing. If you have access to a powerful computer, you may use *pmGenerator* to further contribute to our knowledge regarding the [complexity of proof systems](https://en.wikipedia.org/wiki/Proof_complexity). Progress that has already been made is exemplarily shown below.