|
3 | 3 | Update instructions: |
4 | 4 | 1. Manually replace <body>[...]</body> with that of the updated version |
5 | 5 | 2. RegEx replace-all: [FIND]class\=\"markdown-content\"[/FIND], [REPLACE]id\=\"readme\"[/REPLACE] (1 occurence) |
6 | | - 3. RegEx replace-all: [FIND] class\=\" *\b(?!\bmarkdown-container ltr\b)[^\"]*\b *\"[/FIND], [REPLACE][/REPLACE] (257 occurences) |
| 6 | + 3. RegEx replace-all: [FIND] class\=\" *\b(?!\bmarkdown-container ltr\b)[^\"]*\b *\"[/FIND], [REPLACE][/REPLACE] (211 occurences) |
7 | 7 | 4. RegEx replace-all: [FIND]<p><img src\=\"icon\/icon-readme\.png\" align\=\"left\"><\/p>[/FIND], [REPLACE]<img src\=\"icon\/icon-readme\.png\" align\=\"left\">[/REPLACE] (1 occurence) |
8 | 8 | 5. RegEx replace-all: [FIND]id\=\"-xamidi-pmgenerator\"[/FIND], [REPLACE]id\=\"xamidi-pmgenerator\"[/REPLACE] (1 occurence) |
9 | | - (NOTE: Use RegEx replacements to not invalidate these instructions. Further content may require more bugfixes as by steps 4 and 5.) |
| 9 | + 6. RegEx replace-all: [FIND]<(/|)span>[/FIND], [REPLACE][/REPLACE] (418 occurences) |
| 10 | + (NOTE: Use RegEx replacements to not invalidate these instructions. Further content may require more bugfixes as by steps 4, 5 and 6.) |
10 | 11 | --> |
11 | 12 | <html> |
12 | 13 | <head> |
|
213 | 214 | </head> |
214 | 215 | <body><div class="markdown-container ltr"><div id="readme"><img src="icon/icon-readme.png" align="left"> |
215 | 216 | <h1 id="xamidi-pmgenerator">@xamidi/pmGenerator</h1> |
216 | | -<p>Code extracted from <a href="https://github.com/deontic-logic/proof-tool">deontic-logic/proof-tool</a> (still private; <a href="https://deontic-logic.github.io/readme.html">readme</a>). Can be used to generate improved versions of <a href="https://us.metamath.org/mmsolitaire/pmproofs.txt" title="us.metamath.org/mmsolitaire/pmproofs.txt">pmproofs.txt</a> of the <a href="https://us.metamath.org/mmsolitaire/mms.html" title="us.metamath.org/mmsolitaire/mms.html">mmsolitaire</a> project.<br>Exemplary generated results are available at <a href="https://github.com/xamidi/mmsolitaire" title="GitHub repository">xamidi/mmsolitaire</a>. Eligible for high-performance computing. If you have access to a supercomputer, please consider to use this tool to further contribute to our knowledge regarding minimal proofs.</p> |
| 217 | +<p>Code extracted from <a href="https://github.com/deontic-logic/proof-tool">deontic-logic/proof-tool</a> (still private; <a href="https://deontic-logic.github.io/readme.html">readme</a>). Can be used to generate improved versions of <a href="https://us.metamath.org/mmsolitaire/pmproofs.txt" title="us.metamath.org/mmsolitaire/pmproofs.txt">pmproofs.txt</a> of the <a href="https://us.metamath.org/mmsolitaire/mms.html" title="us.metamath.org/mmsolitaire/mms.html">mmsolitaire</a> project.<br>Exemplary generated results are available at <a href="https://github.com/xamidi/mmsolitaire" title="GitHub repository">xamidi/mmsolitaire</a>. Eligible for shared memory high-performance computing. If you have access to a powerful computer, please consider to use this tool to further contribute to our knowledge regarding minimal proofs.<br>The following table exemplary shows progress that has already been made.</p> |
| 218 | +<table> |
| 219 | +<thead> |
| 220 | +<tr> |
| 221 | +<th>Load Files up to..</th> |
| 222 | +<th style="text-align:right">Size of Files (with conclusions) [B]</th> |
| 223 | +<th style="text-align:right">Required Memory (approx.) [GiB]</th> |
| 224 | +</tr> |
| 225 | +</thead> |
| 226 | +<tbody> |
| 227 | +<tr> |
| 228 | +<td><a href="https://github.com/xamidi/pmGenerator/tree/master/data/dProofs-withConclusions">dProofs29.txt</a></td> |
| 229 | +<td style="text-align:right">735 676 962</td> |
| 230 | +<td style="text-align:right">2.68</td> |
| 231 | +</tr> |
| 232 | +<tr> |
| 233 | +<td><a href="https://mega.nz/file/G18AWIpC#B04xOdtQj_2PJJP0yNQxbim7pOgd-hwv1i1EVU6ZsTM">dProofs31-unfiltered31+.txt</a></td> |
| 234 | +<td style="text-align:right">2 897 309 412</td> |
| 235 | +<td style="text-align:right">9.84</td> |
| 236 | +</tr> |
| 237 | +<tr> |
| 238 | +<td><a href="https://mega.nz/file/3gVQSIJL#Qfa9CoUwsHWYYNHXYaP1mg61QQSJ1NSl1CHudK4g7BA">dProofs33-unfiltered31+.txt</a></td> |
| 239 | +<td style="text-align:right">11 246 333 287</td> |
| 240 | +<td style="text-align:right">36.49</td> |
| 241 | +</tr> |
| 242 | +</tbody> |
| 243 | +</table> |
217 | 244 | <p>Some aspects of this tool were explicated in a <a href="https://groups.google.com/g/metamath/c/v0p86y5b-m0">proposal</a> at the Metamath mailing list.</p> |
218 | 245 | <h4 id="usage">Usage</h4> |
219 | | -<pre><code><span>pmGenerator</span> <span>(</span> <span>-g</span> <span><limit></span> <span>[-u]</span> <span>[-c]</span> <span>| -r <pmproofs file> <output file> [-i <prefix>] [-c] [-d] | -a <initials> <replacements file> <pmproofs file> <output file> [-s] [-l] [-w] [-d] | -f ( 0 | 1 ) [-i <prefix>] [-o <prefix>] [-d] | -p [-i <prefix>] [-s] [-t] [-x <limit>] [-y <limit>] [-o <output file>] [-d] )+ |
220 | | -</span><span>-g:</span> <span>Generate</span> <span>proof</span> <span>files</span> |
221 | | -<span> -u:</span> <span>unfiltered</span> <span>(significantly</span> <span>faster,</span> <span>but</span> <span>generates</span> <span>redundant</span> <span>proofs)</span> |
222 | | -<span> -c:</span> <span>proof</span> <span>files</span> <span>without</span> <span>conclusions,</span> <span>requires</span> <span>additional</span> <span>parsing</span> |
223 | | -<span>-r:</span> <span>Replacements</span> <span>file</span> <span>creation</span> <span>based</span> <span>on</span> <span>proof</span> <span>files</span> |
224 | | -<span> -i:</span> <span>customize</span> <span>input</span> <span>file</span> <span>path</span> <span>prefix</span> <span>;</span> <span>default:</span> <span>"data/dProofs-withConclusions/dProofs"</span> |
225 | | -<span> -c:</span> <span>proof</span> <span>files</span> <span>without</span> <span>conclusions,</span> <span>requires</span> <span>additional</span> <span>parsing</span> <span>;</span> <span>sets</span> <span>default</span> <span>input</span> <span>file</span> <span>path</span> <span>prefix</span> <span>to</span> <span>"data/dProofs-withoutConclusions/dProofs"</span> |
226 | | -<span> -d:</span> <span>print</span> <span>debug</span> <span>information</span> |
227 | | -<span>-a:</span> <span>Apply</span> <span>replacements</span> <span>file</span> |
228 | | -<span> -s:</span> <span>style</span> <span>all</span> <span>proofs</span> <span>(replace</span> <span>proofs</span> <span>with</span> <span>alphanumerically</span> <span>smaller</span> <span>variants)</span> |
229 | | -<span> -l:</span> <span>list</span> <span>all</span> <span>proofs</span> <span>(i.e.</span> <span>not</span> <span>only</span> <span>modified</span> <span>proofs)</span> |
230 | | -<span> -w:</span> <span>wrap</span> <span>results</span> |
231 | | -<span> -d:</span> <span>print</span> <span>debug</span> <span>information</span> |
232 | | -<span>-f:</span> <span>Create</span> <span>proof</span> <span>files</span> <span>with</span> <span>removed</span> <span>(-f</span> <span>0</span><span>)</span> <span>or</span> <span>added</span> <span>(-f</span> <span>1</span><span>)</span> <span>conclusions</span> <span>from</span> <span>proof</span> <span>files</span> <span>of</span> <span>the</span> <span>other</span> <span>variant</span> |
233 | | -<span> -i:</span> <span>customize</span> <span>input</span> <span>file</span> <span>path</span> <span>prefix</span> <span>;</span> <span>default:</span> <span>"data/dProofs-withConclusions/dProofs"</span> <span>or</span> <span>"data/dProofs-withoutConclusions/dProofs"</span> |
234 | | -<span> -o:</span> <span>customize</span> <span>output</span> <span>file</span> <span>path</span> <span>prefix</span> <span>;</span> <span>default:</span> <span>"data/dProofs-withoutConclusions/dProofs"</span> <span>or</span> <span>"data/dProofs-withConclusions/dProofs"</span> |
235 | | -<span> -d:</span> <span>print</span> <span>debug</span> <span>information</span> |
236 | | -<span>-p:</span> <span>Print</span> <span>conclusion</span> <span>length</span> <span>plot</span> <span>data</span> |
237 | | -<span> -i:</span> <span>customize</span> <span>input</span> <span>file</span> <span>path</span> <span>prefix</span> <span>;</span> <span>requires</span> <span>files</span> <span>with</span> <span>conclusions</span> <span>;</span> <span>default:</span> <span>"data/dProofs-withConclusions/dProofs"</span> |
238 | | -<span> -s:</span> <span>measure</span> <span>symbolic</span> <span>length</span> <span>(in</span> <span>contrast</span> <span>to</span> <span>conclusion</span> <span>representation</span> <span>length)</span> |
239 | | -<span> -t:</span> <span>table</span> <span>arrangement,</span> <span>one</span> <span>data</span> <span>point</span> <span>per</span> <span>row</span> |
240 | | -<span> -x:</span> <span>upper</span> <span>horizontal</span> <span>limit</span> |
241 | | -<span> -y:</span> <span>upper</span> <span>vertical</span> <span>limit</span> |
242 | | -<span> -o:</span> <span>print</span> <span>to</span> <span>given</span> <span>output</span> <span>file</span> |
243 | | -<span> -d:</span> <span>print</span> <span>debug</span> <span>information</span> |
| 246 | +<pre><code>pmGenerator ( -g <limit> [-u] [-c] | -r <pmproofs file> <output file> [-i <prefix>] [-c] [-d] | -a <initials> <replacements file> <pmproofs file> <output file> [-s] [-l] [-w] [-d] | -f ( 0 | 1 ) [-i <prefix>] [-o <prefix>] [-d] | -p [-i <prefix>] [-s] [-t] [-x <limit>] [-y <limit>] [-o <output file>] [-d] )+ |
| 247 | +-g: Generate proof files |
| 248 | + -u: unfiltered (significantly faster, but generates redundant proofs) |
| 249 | + -c: proof files without conclusions, requires additional parsing |
| 250 | +-r: Replacements file creation based on proof files |
| 251 | + -i: customize input file path prefix ; default: "data/dProofs-withConclusions/dProofs" |
| 252 | + -c: proof files without conclusions, requires additional parsing ; sets default input file path prefix to "data/dProofs-withoutConclusions/dProofs" |
| 253 | + -d: print debug information |
| 254 | +-a: Apply replacements file |
| 255 | + -s: style all proofs (replace proofs with alphanumerically smaller variants) |
| 256 | + -l: list all proofs (i.e. not only modified proofs) |
| 257 | + -w: wrap results |
| 258 | + -d: print debug information |
| 259 | +-f: Create proof files with removed (-f 0) or added (-f 1) conclusions from proof files of the other variant |
| 260 | + -i: customize input file path prefix ; default: "data/dProofs-withConclusions/dProofs" or "data/dProofs-withoutConclusions/dProofs" |
| 261 | + -o: customize output file path prefix ; default: "data/dProofs-withoutConclusions/dProofs" or "data/dProofs-withConclusions/dProofs" |
| 262 | + -d: print debug information |
| 263 | +-p: Print conclusion length plot data |
| 264 | + -i: customize input file path prefix ; requires files with conclusions ; default: "data/dProofs-withConclusions/dProofs" |
| 265 | + -s: measure symbolic length (in contrast to conclusion representation length) |
| 266 | + -t: table arrangement, one data point per row |
| 267 | + -x: upper horizontal limit |
| 268 | + -y: upper vertical limit |
| 269 | + -o: print to given output file |
| 270 | + -d: print debug information |
244 | 271 | </code></pre><h4 id="examples">Examples</h4> |
245 | | -<pre><code><span>pmGenerator</span> -g <span>-1</span> |
246 | | -pmGenerator -r <span>"data/pmproofs.txt"</span> <span>"data/pmproofs-reducer.txt"</span> -i <span>"data/dProofs"</span> -c -d |
| 272 | +<pre><code>pmGenerator -g -1 |
| 273 | +pmGenerator -r "data/pmproofs.txt" "data/pmproofs-reducer.txt" -i "data/dProofs" -c -d |
247 | 274 | pmGenerator -a SD data/pmproofs-reducer.txt data/pmproofs.txt data/pmproofs-result-styleAll-modifiedOnly.txt -s -w -d |
248 | | -pmGenerator -g <span>19</span> -g <span>21</span> -u -r data/pmproofs-old.txt data/pmproofs-reducer.txt -d -a SD data/pmproofs-reducer.txt data/pmproofs-old.txt data/pmproofs-result-styleAll-modifiedOnly.txt -s -w -d |
249 | | -pmGenerator -f <span>0</span> -o data/dProofs-withoutConclusions_ALL/dProofs -d |
250 | | -pmGenerator -p -s -d -p -s -t -x <span>50</span> -y <span>100</span> -o data/plot_data_x50_y100.txt |
| 275 | +pmGenerator -g 19 -g 21 -u -r data/pmproofs-old.txt data/pmproofs-reducer.txt -d -a SD data/pmproofs-reducer.txt data/pmproofs-old.txt data/pmproofs-result-styleAll-modifiedOnly.txt -s -w -d |
| 276 | +pmGenerator -f 0 -o data/dProofs-withoutConclusions_ALL/dProofs -d |
| 277 | +pmGenerator -p -s -d -p -s -t -x 50 -y 100 -o data/plot_data_x50_y100.txt |
251 | 278 | </code></pre><h4 id="navigation">Navigation</h4> |
252 | 279 | <ul> |
253 | 280 | <li><a href="https://github.com/xamidi/pmGenerator/tree/c++11">C++11 branch</a></li> |
|
0 commit comments