为什么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_formula
和 thf_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_expr
和mult_expr
节点用于简单数字1
:
这就是为什么您会在您的解析树中看到您可能意想不到的空节点。
我正在尝试创建库,该库根据 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 二进制公式的含义是什么?为什么它会出现在我的解析树中,因为这个没有二进制连接词的简单公式?
这里没有真正的答案,除了:因为语法的作者就是这样定义规则的:)
让我们看下面这个非常简单的语法:
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
:
这就是为什么您会在您的解析树中看到您可能意想不到的空节点。