new feature '--ndconvert': convert natural deduction to D-proof summary

- natural deduction format based on https://github.com/mrieppel/FitchFX
- includes Earley parser (to parse FitchFX-formatted formulas)
  - easy to use when more context-free grammars must be parsed,
    in case parsing is not performance-critical
+ --parse -s: fix axiom names to 1,…,9,a,b,…; not all numeric

Author: xamidi

.gitignore

@@ -32,6 +32,7 @@ data/*
 !data/pmproofs.txt
 !data/pmproofs-old.txt
 !data/cardinalities.txt
+!data/*_ffx.txt
 !data/52436f9e87daeb2c361a73a9f389b061258328e641f750b1767addf7/
 data/52436f9e87daeb2c361a73a9f389b061258328e641f750b1767addf7/*
 !data/52436f9e87daeb2c361a73a9f389b061258328e641f750b1767addf7/\!.def

README.html

@@ -514,6 +514,16 @@ <h4 id="usage">Usage</h4>
        -f: proof summary is given by input file path ; ignores lines that are empty or starting with '%'
        -o: redirect the result's output to the specified file
        -d: print debug information
+  --ndconvert &lt;input file&gt; [-b &lt;base file&gt;] [-n] [-u] [-h] [-k] [-o &lt;output file&gt;] [-d]
+     Convert proof from Fitch-style natural deduction to condensed detachment in a user-definable Hilbert system and print its proof summary (usable via '--transform' and '--unfold') ; ignores configured system
+     Input file must contain propositional FitchFX proof without premises, as exportable from https://mrieppel.github.io/FitchFX/ ; supported rules: 'Assumption','IP','~I','~E','&gt;I','&gt;E','&I','&E','vI','vE','&lt;&gt;I','&lt;&gt;E','Reit'
+       -b: provide target system with translation-assisting proofs via input file path of a proof summary ; proofs of (A1),(A2) are minimally required ; details: https://github.com/xamidi/pmGenerator/blob/master/nd/NdConverter.h
+       -n: specify and print formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
+       -u: print formulas in infix notation with operators as Unicode characters ; does not affect input format (for which '-n' can still be specified)
+       -h: use heterogeneous language ; do not consider all formulas to use only connectives in {C,N} (aliased by Kpq:=NCpNq, Apq:=CNpq, Epq:=NCCpqNCqp, and O:=NCpp)
+       -k: keep proofs for all theorems (not only those which are used to derive the target theorem)
+       -o: redirect the result's output to the specified file
+       -d: print debug information
   --search &lt;string&gt; [-n] [-s] [-w] [-t] [-p] [-f] [-d]
      Search in proof files at ./data/[&lt;hash&gt;/]/dProofs-withConclusions/ via comma-separated string of full formulas or full proofs ; [Hint: Generate missing files with '--variate 1 -s'.]
        -n: specify formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
@@ -579,6 +589,7 @@ <h4 id="usage">Usage</h4>
 pmGenerator --unfold CpCqp=1,CCpCqrCCpqCpr=2,CCNpNqCqp=3,[0]CCpCNqNrCpCrq:D2D13,[1]Cpp:DD211,[2]NCCppNCqq:DD3DD2DD2D[0]D[0]11D1[1][1] -n -t CNNpp,NCCppNCqq
 pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -p -2 -d
 pmGenerator --transform "CCCpqrCCrpCsp=1,[0]=DDDD1D1D1D1DDDD1D1D11111111,[1]=D1DD[0]1[0],[2]=DDDD1DD[1][1]1111" -n -w -t _
+pmGenerator --ndconvert data/m_ffx.txt -n -b data/w1.txt -u
 pmGenerator -c -s CCCCC0.1CN2N3.2.4CC4.0C3.0 -g 35 --plot -s -t -x 50 -y 100 -o data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/plot_data_x50_y100.txt
 pmGenerator -c -n -s CCCCCpqCNrNsrtCCtpCsp --search CpCqp,CCpCqrCCpqCpr,CCNpNqCqp -n
 pmGenerator --variate 1 -s --extract -t 1000 -s -d

README.md

@@ -146,6 +146,16 @@ Some more – and very special – proof systems are illustrated [further down b
            -f: proof summary is given by input file path ; ignores lines that are empty or starting with '%'
            -o: redirect the result's output to the specified file
            -d: print debug information
+      --ndconvert <input file> [-b <base file>] [-n] [-u] [-h] [-k] [-o <output file>] [-d]
+         Convert proof from Fitch-style natural deduction to condensed detachment in a user-definable Hilbert system and print its proof summary (usable via '--transform' and '--unfold') ; ignores configured system
+         Input file must contain propositional FitchFX proof without premises, as exportable from https://mrieppel.github.io/FitchFX/ ; supported rules: 'Assumption','IP','~I','~E','>I','>E','&I','&E','vI','vE','<>I','<>E','Reit'
+           -b: provide target system with translation-assisting proofs via input file path of a proof summary ; proofs of (A1),(A2) are minimally required ; details: https://github.com/xamidi/pmGenerator/blob/master/nd/NdConverter.h
+           -n: specify and print formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
+           -u: print formulas in infix notation with operators as Unicode characters ; does not affect input format (for which '-n' can still be specified)
+           -h: use heterogeneous language ; do not consider all formulas to use only connectives in {C,N} (aliased by Kpq:=NCpNq, Apq:=CNpq, Epq:=NCCpqNCqp, and O:=NCpp)
+           -k: keep proofs for all theorems (not only those which are used to derive the target theorem)
+           -o: redirect the result's output to the specified file
+           -d: print debug information
       --search <string> [-n] [-s] [-w] [-t] [-p] [-f] [-d]
          Search in proof files at ./data/[<hash>/]/dProofs-withConclusions/ via comma-separated string of full formulas or full proofs ; [Hint: Generate missing files with '--variate 1 -s'.]
            -n: specify formulas in normal Polish notation (e.g. "CpCqp"), not with numeric variables (e.g. "C0C1.0")
@@ -212,6 +222,7 @@ Some more – and very special – proof systems are illustrated [further down b
     pmGenerator --unfold CpCqp=1,CCpCqrCCpqCpr=2,CCNpNqCqp=3,[0]CCpCNqNrCpCrq:D2D13,[1]Cpp:DD211,[2]NCCppNCqq:DD3DD2DD2D[0]D[0]11D1[1][1] -n -t CNNpp,NCCppNCqq
     pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -p -2 -d
     pmGenerator --transform "CCCpqrCCrpCsp=1,[0]=DDDD1D1D1D1DDDD1D1D11111111,[1]=D1DD[0]1[0],[2]=DDDD1DD[1][1]1111" -n -w -t _
+    pmGenerator --ndconvert data/m_ffx.txt -n -b data/w1.txt -u
     pmGenerator -c -s CCCCC0.1CN2N3.2.4CC4.0C3.0 -g 35 --plot -s -t -x 50 -y 100 -o data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/plot_data_x50_y100.txt
     pmGenerator -c -n -s CCCCCpqCNrNsrtCCtpCsp --search CpCqp,CCpCqrCCpqCpr,CCNpNqCqp -n
     pmGenerator --variate 1 -s --extract -t 1000 -s -d

__dependency_graph.dot

@@ -15,9 +15,14 @@ digraph {
 	CfgGrammar -> "(cstdint)" [color=red]
 	CfgGrammar -> "(unordered_map)" [color=red]
 	CfgGrammar -> "(vector)" [color=red]
+	CfgParser -> FctHelper [color=blue]
+	CfgParser -> CfgGrammar [color=blue]
+	CfgParser -> TreeNode [color=red]
 	subgraph "cluster_D:/Dropbox/eclipse/pmGenerator\grammar" {
 		CfgGrammar
 		CfgGrammar
+		CfgParser
+		CfgParser
 	}
 	FctHelper -> "(cmath)" [color=blue]
 	FctHelper -> "(iostream)" [color=blue]
@@ -147,6 +152,7 @@ digraph {
 	main -> FctHelper [color=blue]
 	main -> Version [color=blue]
 	main -> DRuleReducer [color=blue]
+	main -> NdConverter [color=blue]
 	main -> DlProofEnumerator [color=blue]
 	main -> "boost/algorithm/string" [color=blue]
 	main -> "(cstring)" [color=blue]
@@ -191,6 +197,33 @@ digraph {
 		DRuleReducer
 		DRuleReducer
 	}
+	NdConverter -> FctHelper [color=blue]
+	NdConverter -> TreeNode [color=blue]
+	NdConverter -> DlCore [color=blue]
+	NdConverter -> DlProofEnumerator [color=blue]
+	NdConverter -> NdParser [color=blue]
+	NdConverter -> "boost/algorithm/string" [color=blue]
+	NdConverter -> "(numeric)" [color=blue]
+	NdConverter -> "(string)" [color=red]
+	NdParser -> FctHelper [color=blue]
+	NdParser -> CfgGrammar [color=blue]
+	NdParser -> CfgParser [color=blue]
+	NdParser -> DlCore [color=blue]
+	NdParser -> "boost/algorithm/string" [color=blue]
+	NdParser -> "(iostream)" [color=blue]
+	NdParser -> "(array)" [color=red]
+	NdParser -> "(cstddef)" [color=red]
+	NdParser -> "(cstdint)" [color=red]
+	NdParser -> "(map)" [color=red]
+	NdParser -> "(memory)" [color=red]
+	NdParser -> "(string)" [color=red]
+	NdParser -> "(vector)" [color=red]
+	subgraph "cluster_D:/Dropbox/eclipse/pmGenerator\nd" {
+		NdConverter
+		NdConverter
+		NdParser
+		NdParser
+	}
 	TreeNode -> ICloneable [color=red]
 	TreeNode -> IPrintable [color=red]
 	TreeNode -> "(algorithm)" [color=red]

data/m_ffx.txt

@@ -0,0 +1,33 @@
+% Meredith's Axiom (CCCCCpqCNrNsrtCCtpCsp), i.e. ((((0→1)→(¬2→¬3))→2)→4)→((4→0)→(3→0))
+% Fitch-style natural deduction proof constructor: https://mrieppel.github.io/FitchFX/
+%
+% Related Hilbert system: https://xamidi.github.io/pmGenerator/data/m.txt
+% Conversion to Hilbert-style condensed detachment proof summary:
+% - [base:CpCqp,CCpCqrCCpqCpr,CCNpNqCqp]: pmGenerator --ndconvert data/m_ffx.txt -n
+% - [<proof summary of base system>.txt]: pmGenerator --ndconvert data/m_ffx.txt -n -b <proof summary of base system>.txt
+
+Problem:  |- (((((A > B) > (~C > ~D)) > C) > E) > ((E > A) > (D > A)))
+
+1   | |_  ((((A > B) > (~C > ~D)) > C) > E)                          Assumption
+2   | | |_  (E > A)                                                  Assumption
+3   | | | |_  D                                                      Assumption
+4   | | | | |_  ~A                                                   Assumption
+5   | | | | | |_  ((A > B) > (~C > ~D))                              Assumption
+6   | | | | | | |_  ~C                                               Assumption
+7   | | | | | | | |_  A                                              Assumption
+8   | | | | | | | | |_  ~B                                           Assumption
+9   | | | | | | | | |   #                                            ~E  4,7
+10  | | | | | | | |   B                                              IP  8-9
+11  | | | | | | |   (A > B)                                          >I  7-10
+12  | | | | | | |   (~C > ~D)                                        >E  5,11
+13  | | | | | | |   ~D                                               >E  6,12
+14  | | | | | | |   #                                                ~E  3,13
+15  | | | | | |   C                                                  IP  6-14
+16  | | | | |   (((A > B) > (~C > ~D)) > C)                          >I  5-15
+17  | | | | |   E                                                    >E  1,16
+18  | | | | |   A                                                    >E  2,17
+19  | | | | |   #                                                    ~E  4,18
+20  | | | |   A                                                      IP  4-19
+21  | | |   (D > A)                                                  >I  3-20
+22  | |   ((E > A) > (D > A))                                        >I  2-21
+23  |   (((((A > B) > (~C > ~D)) > C) > E) > ((E > A) > (D > A)))    >I  1-22

data/w1_ffx.txt

@@ -0,0 +1,30 @@
+% Walsh's 1st Axiom (CCpCCNpqrCsCCNtCrtCpt), i.e. (0→((¬0→1)→2))→(3→((¬4→(2→4))→(0→4)))
+% Fitch-style natural deduction proof constructor: https://mrieppel.github.io/FitchFX/
+%
+% Related Hilbert system: https://xamidi.github.io/pmGenerator/data/w1.txt
+% Conversion to Hilbert-style condensed detachment proof summary:
+% - [base:CpCqp,CCpCqrCCpqCpr,CCNpNqCqp]: pmGenerator --ndconvert data/w1_ffx.txt -n
+% - [<proof summary of base system>.txt]: pmGenerator --ndconvert data/w1_ffx.txt -n -b <proof summary of base system>.txt
+
+Problem:  |- ((A > ((~A > B) > C)) > (D > ((~E > (C > E)) > (A > E))))
+
+1   | |_  (A > ((~A > B) > C))                                       Assumption
+2   | | |_  D                                                        Assumption
+3   | | | |_  (~E > (C > E))                                         Assumption
+4   | | | | |_  A                                                    Assumption
+5   | | | | | |_  ~E                                                 Assumption
+6   | | | | | | |_  ~A                                               Assumption
+7   | | | | | | | |_  ~B                                             Assumption
+8   | | | | | | | |   #                                              ~E  4,6
+9   | | | | | | |   B                                                IP  7-8
+10  | | | | | |   (~A > B)                                           >I  6-9
+11  | | | | | |   ((~A > B) > C)                                     >E  1,4
+12  | | | | | |   C                                                  >E  10,11
+13  | | | | | |   (C > E)                                            >E  3,5
+14  | | | | | |   E                                                  >E  12,13
+15  | | | | | |   #                                                  ~E  5,14
+16  | | | | |   E                                                    IP  5-15
+17  | | | |   (A > E)                                                >I  4-16
+18  | | |   ((~E > (C > E)) > (A > E))                               >I  3-17
+19  | |   (D > ((~E > (C > E)) > (A > E)))                           >I  2-18
+20  |   ((A > ((~A > B) > C)) > (D > ((~E > (C > E)) > (A > E))))    >I  1-19

data/w2_ffx.txt

@@ -0,0 +1,30 @@
+% Walsh's 2nd Axiom (CpCCqCprCCNrCCNstqCsr), i.e. 0→((1→(0→2))→((¬2→((¬3→4)→1))→(3→2)))
+% Fitch-style natural deduction proof constructor: https://mrieppel.github.io/FitchFX/
+%
+% Related Hilbert system: https://xamidi.github.io/pmGenerator/data/w2.txt
+% Conversion to Hilbert-style condensed detachment proof summary:
+% - [base:CpCqp,CCpCqrCCpqCpr,CCNpNqCqp]: pmGenerator --ndconvert data/w2_ffx.txt -n
+% - [<proof summary of base system>.txt]: pmGenerator --ndconvert data/w2_ffx.txt -n -b <proof summary of base system>.txt
+
+Problem:  |- (A > ((B > (A > C)) > ((~C > ((~D > E) > B)) > (D > C))))
+
+1   | |_  A                                                          Assumption
+2   | | |_  (B > (A > C))                                            Assumption
+3   | | | |_  (~C > ((~D > E) > B))                                  Assumption
+4   | | | | |_  D                                                    Assumption
+5   | | | | | |_  ~C                                                 Assumption
+6   | | | | | | |_  ~D                                               Assumption
+7   | | | | | | | |_  ~E                                             Assumption
+8   | | | | | | | |   #                                              ~E  4,6
+9   | | | | | | |   E                                                IP  7-8
+10  | | | | | |   (~D > E)                                           >I  6-9
+11  | | | | | |   ((~D > E) > B)                                     >E  3,5
+12  | | | | | |   B                                                  >E  10,11
+13  | | | | | |   (A > C)                                            >E  2,12
+14  | | | | | |   C                                                  >E  1,13
+15  | | | | | |   #                                                  ~E  5,14
+16  | | | | |   C                                                    IP  5-15
+17  | | | |   (D > C)                                                >I  4-16
+18  | | |   ((~C > ((~D > E) > B)) > (D > C))                        >I  3-17
+19  | |   ((B > (A > C)) > ((~C > ((~D > E) > B)) > (D > C)))        >I  2-18
+20  |   (A > ((B > (A > C)) > ((~C > ((~D > E) > B)) > (D > C))))    >I  1-19

data/w3_ffx.txt

@@ -0,0 +1,30 @@
+% Walsh's 3rd Axiom (CpCCNqCCNrsCptCCtqCrq), i.e. 0→((¬1→((¬2→3)→(0→4)))→((4→1)→(2→1)))
+% Fitch-style natural deduction proof constructor: https://mrieppel.github.io/FitchFX/
+%
+% Related Hilbert system: https://xamidi.github.io/pmGenerator/data/w3.txt
+% Conversion to Hilbert-style condensed detachment proof summary:
+% - [base:CpCqp,CCpCqrCCpqCpr,CCNpNqCqp]: pmGenerator --ndconvert data/w3_ffx.txt -n
+% - [<proof summary of base system>.txt]: pmGenerator --ndconvert data/w3_ffx.txt -n -b <proof summary of base system>.txt
+
+Problem:  |- (A > ((~B > ((~C > D) > (A > E))) > ((E > B) > (C > B))))
+
+1   | |_  A                                                          Assumption
+2   | | |_  (~B > ((~C > D) > (A > E)))                              Assumption
+3   | | | |_  (E > B)                                                Assumption
+4   | | | | |_  C                                                    Assumption
+5   | | | | | |_  ~B                                                 Assumption
+6   | | | | | | |_  ~C                                               Assumption
+7   | | | | | | | |_  ~D                                             Assumption
+8   | | | | | | | |   #                                              ~E  4,6
+9   | | | | | | |   D                                                IP  7-8
+10  | | | | | |   (~C > D)                                           >I  6-9
+11  | | | | | |   ((~C > D) > (A > E))                               >E  2,5
+12  | | | | | |   (A > E)                                            >E  10,11
+13  | | | | | |   E                                                  >E  1,12
+14  | | | | | |   B                                                  >E  3,13
+15  | | | | | |   #                                                  ~E  5,14
+16  | | | | |   B                                                    IP  5-15
+17  | | | |   (C > B)                                                >I  4-16
+18  | | |   ((E > B) > (C > B))                                      >I  3-17
+19  | |   ((~B > ((~C > D) > (A > E))) > ((E > B) > (C > B)))        >I  2-18
+20  |   (A > ((~B > ((~C > D) > (A > E))) > ((E > B) > (C > B))))    >I  1-19

data/w4_ffx.txt

@@ -0,0 +1,30 @@
+% Walsh's 4th Axiom (CpCCNqCCNrsCtqCCrtCrq), i.e. 0→((¬1→((¬2→3)→(4→1)))→((2→4)→(2→1)))
+% Fitch-style natural deduction proof constructor: https://mrieppel.github.io/FitchFX/
+%
+% Related Hilbert system: https://xamidi.github.io/pmGenerator/data/w4.txt
+% Conversion to Hilbert-style condensed detachment proof summary:
+% - [base:CpCqp,CCpCqrCCpqCpr,CCNpNqCqp]: pmGenerator --ndconvert data/w4_ffx.txt -n
+% - [<proof summary of base system>.txt]: pmGenerator --ndconvert data/w4_ffx.txt -n -b <proof summary of base system>.txt
+
+Problem:  |- (A > ((~B > ((~C > D) > (E > B))) > ((C > E) > (C > B))))
+
+1   | |_  A                                                          Assumption
+2   | | |_  (~B > ((~C > D) > (E > B)))                              Assumption
+3   | | | |_  (C > E)                                                Assumption
+4   | | | | |_  C                                                    Assumption
+5   | | | | | |_  ~B                                                 Assumption
+6   | | | | | | |_  ~C                                               Assumption
+7   | | | | | | | |_  ~D                                             Assumption
+8   | | | | | | | |   #                                              ~E  4,6
+9   | | | | | | |   D                                                IP  7-8
+10  | | | | | |   (~C > D)                                           >I  6-9
+11  | | | | | |   ((~C > D) > (E > B))                               >E  2,5
+12  | | | | | |   (E > B)                                            >E  10,11
+13  | | | | | |   E                                                  >E  3,4
+14  | | | | | |   B                                                  >E  12,13
+15  | | | | | |   #                                                  ~E  5,14
+16  | | | | |   B                                                    IP  5-15
+17  | | | |   (C > B)                                                >I  4-16
+18  | | |   ((C > E) > (C > B))                                      >I  3-17
+19  | |   ((~B > ((~C > D) > (E > B))) > ((C > E) > (C > B)))        >I  2-18
+20  |   (A > ((~B > ((~C > D) > (E > B))) > ((C > E) > (C > B))))    >I  1-19