The grammar at first hand is a bit odd. Especially the fact that we have a name token that in BoxProver can be almost any set of chars. That is some_name,1,2,3-5 is a valid name. I have restricted this a bit, but it is actually quite cool. We can for example treat sub- and superscripts and so on. Ex. some_1^2 is valid in BoxProver, so why not make it $some_{1}^{2}$. \ is allowed too, so \ can be use to map special chars. Anyway, the grammar, here for Grammar2Slr:
* I have made changes to the grammar. It occurred to me that a single _ can't be treated by the former grammar without naming it. So a line can now be followed by another line without naming and so on. Another thing to note is that the ending . is not necessary in my version of the grammar. This diverges even further from the BoxProver grammar, but the change has some neat impact. More on that later.
#grammar for boxprover prec "not" 7 prec "all" 6 prec "exi" 5 prec "eq" 4 prec "and" 3 prec "or" 2 prec "imp" 1 assoc "left" : "and","or","not","eq" assoc "right" : "imp" token "and","or","imp","not","eq" as "/\\\\","\\\\/","=>|->","~","==|=" token "prem","assump" as "premise;","assumption;" token "all_e","all_i","bot_e","con_e1","con_e2","con_i","dis_e", "dis_i1","dis_i2","eq_e","eq_i","exi_e","exi_i","imp_e","imp_i", "neg_e","neg_i","nne","nni","pbc","top_i","var","all","exi", "lem","mt","by","copy" as "all_e(?= )","all_i(?= )","bot_e(?= )","con_e1(?= )","con_e2(?= )","con_i(?= )","dis_e(?= )", "dis_i1(?= )","dis_i2(?= )","eq_e(?= )","eq_i(?= )","exi_e(?= )","exi_i(?= )","imp_e(?= )","imp_i(?= )", "neg_e(?= )","neg_i(?= )","nne(?= )","nni(?= )","pbc(?= )","top_i(?= )","var(?= )","all(?= )","exi(?= )", "lem(?= )","mt(?= )","by(?= )","copy(?= )" token "lpar","rpar","lbracket","rbracket" as "(",")","\\[","\\]" token "uscore","scolon","dot" as "_",";","." token -cap "name" as "[a-zA-Z0-9@#\\-_'\\^]+|q[^q]*q" !token "\n","\r","\t"," " prod Lines -> Line LinesOptEnd prod LinesOptEnd-> "scolon" Naming Lines | Naming Lines | Lines | "dot" | prod Line -> Formula Rule | "lpar" Box "rpar" | "uscore" prod Rule -> "prem" | "assump" | "by" RuleApply prod Box -> "var" Naming Lines | Lines prod RuleApply -> "top_i" | "con_i" "name" "name" | "con_e1" "name" | "con_e2" "name" | "dis_i1" "name" | "dis_i2" "name" | "dis_e" "name" "name" "name" | "imp_i" "name" | "imp_e" "name" "name" | "neg_i" "name" | "neg_e" "name" "name" | "bot_e" "name" | "nne" "name" | "nni" "name" | "lem" | "pbc" "name" | "mt" "name" "name" | "all_i" "name" | "all_e" "name" "name" | "exi_i" "name" "name" | "exi_e" "name" "name" | "eq_i" | "eq_e" Bind "name" "name" | "copy" "name" prod Naming -> "lbracket" "name" "rbracket" prod Formula -> Formula "and" Formula | Formula "or" Formula | Formula "imp" Formula | Formula "eq" Formula | "all" Bind | "exi" Bind | "not" Formula | Atom prod Bind -> "lpar" Naming Formula "rpar" prod Atom -> "lpar" Formula "rpar" | "name" OptArgs prod OptArgs -> "name" OptArgs | "lpar" Formula "rpar" OptArgs |The grammar for predicate logic does not allow a formula as argument for anything, only terms (that is atoms and functions) can be used as arguments. In this version formulas are allowed because: why not. I'm not sure BoxProver allows this.