You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
<p>This tool can collect exhaustive sets of <ahref="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 <ahref="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 unification with <ahref="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 <ahref="https://en.wikipedia.org/wiki/Logical_consequence#Syntactic_consequence">syntactic consequences</a> within <ahref="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 <ahref="https://github.com/xamidi/pmGenerator/discussions">discussion forum</a> for questions, ideas, challenges, and related information.</p>
272
272
<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 <ahref="https://en.wikipedia.org/wiki/Proof_complexity">complexity of proof systems</a>. Progress that has already been made is exemplarily shown below.</p>
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>
571
571
<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> <sub><imgsrc="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>
<p>The above systems show remarkable differences in complexity, despite similarities. For example, the syntax trees of Walsh's 3rd and 4th axiom differ only in four leaf nodes.</p>
1191
1191
<p>Only systems with an odd-ary rule such as necessitation can have condensed detachment proofs of even lengths.<br>The system of modal logic illustrated below extends <ahref="#freges-calculus-simplified-by-łukasiewicz-cpcqpccpcqrccpqcprccnpnqcqp-top1000-cardinalities-db-customization-info">Frege's calculus simplified by Łukasiewicz</a>. It can be covered by enabling the N-rule without limiting the number of its consecutive applications via <code>-c -N -1</code>.</p>
0 commit comments