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

Question

我正在尝试创建库，该库根据 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_formula 和 thf_binary_pair？据我所知，TPTP 二元公式适用于二元连接词（合取、析取、蕴涵），但我的公式有 none 个，我的公式只有相等函数 = 和两个量词，它们都构成嵌套一元公式.

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

Answer 1

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

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

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 :

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

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

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

parsing

logic

artificial-intelligence

antlr4

first-order-logic