为什么在TPTP千问题...公式的解析树中有二进制公式thf_binary_formula？

问题描述

我正在尝试创建一个库，该库根据TPTP（定理证明的成千上万种问题）语言http://tptp.org/的公式创建抽象语法树。我正在使用TPTP的一个很好的ANTRL4语法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
                  )
      )

通常-原始解析树非常复杂，但是我理解它的每个部分，除了-这是我的问题-为何parese树中有thf_binary_formula和thf_binary_pair？据我了解，TPTP二进制公式适用于二进制连接词（合取，析取，蕴含），但是我的公式没有一个，我的公式只有等式函数=和两个量词，它们都构成嵌套的一元公式。>

所以- 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_expr和mult_expr个简单数字1的节点：

这就是为什么您在解析树中看到空节点的原因，这也许是您所不希望的。