add computing time project extension proposal for 4.2025 - 3.2026

+ rwth1392_extension_2024.pdf: fix spelling mistake

Author: xamidi

README.html

@@ -1298,5 +1298,5 @@ <h6 id="s5-cpcqpccpcqrccpqcprccnpnqcqpclppclcpqclplqcnlnplnlnp-top1000-cardinali
 
 </details>
 
-<p><sup>✻</sup><sub>A proof is <em>minimal</em> in context of a behavioral graph if it is the alphanumerically smallest sequence of all shortest possible proofs towards its theorem. Consequently, each proof counted in a behavioral graph uniquely represents its theorem. So these graphs illustrate how many theorems (including but not counting all their infinitely many instances) of a certain size can first be proven using a certain amount of proof steps. These alphanumeric minima may not actually occur in the proof files, but they clearly exist. In contrast, proof minimization usually aims towards finding a <em>shortest</em> proof (also “minimal”, but referring to length) — not “<em>the</em> minimal proof” as in this context.</sub><br><sup>❈</sup><sub>Generation and utilization were performed with computing resources granted by RWTH Aachen University under project <a href="pdf/rwth1392_extension_2024.pdf" title="View rwth1392_extension_2024.pdf">rwth1392</a>.</sub></p>
+<p><sup>✻</sup><sub>A proof is <em>minimal</em> in context of a behavioral graph if it is the alphanumerically smallest sequence of all shortest possible proofs towards its theorem. Consequently, each proof counted in a behavioral graph uniquely represents its theorem. So these graphs illustrate how many theorems (including but not counting all their infinitely many instances) of a certain size can first be proven using a certain amount of proof steps. These alphanumeric minima may not actually occur in the proof files, but they clearly exist. In contrast, proof minimization usually aims towards finding a <em>shortest</em> proof (also “minimal”, but referring to length) — not “<em>the</em> minimal proof” as in this context.</sub><br><sup>❈</sup><sub>Generation and utilization were performed with computing resources granted by RWTH Aachen University under project <a href="pdf/rwth1392_extension_2025.pdf" title="View rwth1392_extension_2025.pdf">rwth1392</a>.</sub></p>
 </article></div></div></body></html>

README.md

@@ -382,4 +382,4 @@ The system of modal logic illustrated below extends [Frege's calculus simplified
 </details>
 
 <sup>✻</sup><sub>A proof is *minimal* in context of a behavioral graph if it is the alphanumerically smallest sequence of all shortest possible proofs towards its theorem. Consequently, each proof counted in a behavioral graph uniquely represents its theorem. So these graphs illustrate how many theorems (including but not counting all their infinitely many instances) of a certain size can first be proven using a certain amount of proof steps. These alphanumeric minima may not actually occur in the proof files, but they clearly exist. In contrast, proof minimization usually aims towards finding a *shortest* proof (also “minimal”, but referring to length) — not “*the* minimal proof” as in this context.</sub>  
-<sup>❈</sup><sub>Generation and utilization were performed with computing resources granted by RWTH Aachen University under project [rwth1392](pdf/rwth1392_extension_2024.pdf "View rwth1392_extension_2024.pdf").</sub>
+<sup>❈</sup><sub>Generation and utilization were performed with computing resources granted by RWTH Aachen University under project [rwth1392](pdf/rwth1392_extension_2025.pdf "View rwth1392_extension_2025.pdf").</sub>