为什么TPTP(Thousand Problems...)公式的解析树中有二元公式(thf_binary_formula)?

Why there is binary formula (thf_binary_formula) in the parse tree of TPTP (Thousand Problems...) formula?

我正在尝试创建库,该库根据 TPTP(定理证明者的千问题)语言 http://tptp.org/. There is nice ANTRL4 grammar https://github.com/TobiasGleissner/TPTP-ANTLR4-Grammar 的公式创建抽象语法树,我正在使用它来生成解析器。我有公式(TPTP 表达式)(![A:animal]:?[H:human]:H=owner_of(A)) 并且它有美化的(漂亮的打印)解析树,它是由根据引用语法创建的标准 ANTLR4 解析器生成的:

thf_formula
  thf_logic_formula
    thf_unitary_formula (
      thf_logic_formula
        thf_binary_formula
          thf_binary_pair
            thf_unitary_formula
              thf_quantified_formula
                thf_quantification
                  thf_quantifier
                    fof_quantifier !
                  [
                  thf_variable_list
                    thf_variable
                      thf_typed_variable
                        variable A
                        :
                        thf_top_level_type
                          thf_unitary_type
                            thf_unitary_formula
                              thf_atom
                                thf_function
                                  atom
                                    untyped_atom
                                      constant
                                        functor
                                          atomic_word animal
                  ]:
                thf_unitary_formula
                  thf_quantified_formula
                    thf_quantification
                      thf_quantifier
                        fof_quantifier ?
                      [
                      thf_variable_list
                        thf_variable
                          thf_typed_variable
                            variable H
                            :
                            thf_top_level_type
                              thf_unitary_type
                                thf_unitary_formula
                                  thf_atom
                                    thf_function
                                      atom
                                        untyped_atom
                                          constant
                                            functor
                                              atomic_word human
                      ]:
                    thf_unitary_formula
                      thf_atom
                        variable H
            thf_pair_connective =
            thf_unitary_formula
              thf_atom
                thf_function
                  functor
                    atomic_word owner_of
                  (
                  thf_arguments
                    thf_formula_list
                      thf_logic_formula
                        thf_unitary_formula
                          thf_atom
                            variable A
                  )
      )

通常 - 原始解析树非常复杂,但我理解它的每一部分,除了 - 这就是我的问题 - 为什么在解析树中有 thf_binary_formulathf_binary_pair?据我所知,TPTP 二元公式适用于二元连接词(合取、析取、蕴涵),但我的公式有 none 个,我的公式只有相等函数 = 和两个量词,它们都构成嵌套一元公式.

那么 - TPTP 二进制公式的含义是什么?为什么它会出现在我的解析树中,因为这个没有二进制连接词的简单公式?

这里没有真正的答案,除了:因为语法的作者就是这样定义规则的:)

让我们看下面这个非常简单的语法:

grammar Expr;

parse
 : expr EOF
 ;

expr
 : add_expr
 ;

add_expr
 : mult_expr ( ('+' | '-') mult_expr)*
 ;

mult_expr
 : atom ( ('*' | '/') atom)*
 ;

atom
 : '(' expr ')'
 | NUMBER
 ;

NUMBER
 : ( [0-9]* '.' )? [0-9]+
 ;

SPACES
 : [ \t\r\n]+ -> skip
 ;

因为 add_expr 放在 mult_expr 之前,输入像 1+2*3 将导致 * 运算符的优先级高于 + 运算符。这导致以下解析树:

但是,因为语法是这样写的,解析树在解析时也会有(空的)add_exprmult_expr节点用于简单数字1 :

这就是为什么您会在您的解析树中看到您可能意想不到的空节点。