如何解决为什么在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
的节点:
这就是为什么您在解析树中看到空节点的原因,这也许是您所不希望的。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。