Skip to content

Commit b1306a8

Browse files
committed
fix '-c -N' documentation for unlimited consecutive N-rule applications
1 parent 53d36dd commit b1306a8

File tree

3 files changed

+3
-3
lines changed

3 files changed

+3
-3
lines changed

README.html

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -420,7 +420,7 @@ <h4 id="usage">Usage</h4>
420420
-i: specify axioms by input file path (where a LF-separated string of axioms is stored), ignoring lines that are empty or starting with '%'
421421
-s: specify axioms by comma-separated string ; used only when '-i' unspecified ; default: "C0C1.0,CC0C1.2CC0.1C0.2,CCN0N1C1.0"
422422
-n: specify formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
423-
-N: enable necessitation rule "N" for the given system with unlimited (-N 0) or limited (-N &lt;positive amount&gt;) consecutive necessitation steps allowed
423+
-N: enable necessitation rule "N" for the given system with unlimited (-N -1) or limited (-N &lt;positive amount&gt;) consecutive necessitation steps allowed
424424
-l: disable lazy N-rule parsing ; parse proofs Nα:Lβ despite knowing α:β (requires more time but less memory)
425425
-e: specify extracted system with the given identifier
426426
-d: default system ; ignore all other arguments except '-e'

README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ Some more – and very special – proof systems are illustrated [further down b
4545
-i: specify axioms by input file path (where a LF-separated string of axioms is stored), ignoring lines that are empty or starting with '%'
4646
-s: specify axioms by comma-separated string ; used only when '-i' unspecified ; default: "C0C1.0,CC0C1.2CC0.1C0.2,CCN0N1C1.0"
4747
-n: specify formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
48-
-N: enable necessitation rule "N" for the given system with unlimited (-N 0) or limited (-N <positive amount>) consecutive necessitation steps allowed
48+
-N: enable necessitation rule "N" for the given system with unlimited (-N -1) or limited (-N <positive amount>) consecutive necessitation steps allowed
4949
-l: disable lazy N-rule parsing ; parse proofs Nα:Lβ despite knowing α:β (requires more time but less memory)
5050
-e: specify extracted system with the given identifier
5151
-d: default system ; ignore all other arguments except '-e'

main.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ static const map<Task, string>& cmdInfo() {
5959
" -i: specify axioms by input file path (where a LF-separated string of axioms is stored), ignoring lines that are empty or starting with '%'\n"
6060
" -s: specify axioms by comma-separated string ; used only when '-i' unspecified ; default: \"C0C1.0,CC0C1.2CC0.1C0.2,CCN0N1C1.0\"\n"
6161
" -n: specify formulas in normal Polish notation (e.g. \"CpCqp\"), not with numeric variables (e.g. \"C0C1.0\")\n"
62-
" -N: enable necessitation rule \"N\" for the given system with unlimited (-N 0) or limited (-N <positive amount>) consecutive necessitation steps allowed\n"
62+
" -N: enable necessitation rule \"N\" for the given system with unlimited (-N -1) or limited (-N <positive amount>) consecutive necessitation steps allowed\n"
6363
" -l: disable lazy N-rule parsing ; parse proofs Nα:Lβ despite knowing α:β (requires more time but less memory)\n"
6464
" -e: specify extracted system with the given identifier\n"
6565
" -d: default system ; ignore all other arguments except '-e'\n";

0 commit comments

Comments
 (0)