prolog - 是否可以用一阶逻辑表示上下文无关文法？

Question

简而言之，我有一个 EBNF 语法和一个解析树，但我不知道是否有一个程序可以在一阶逻辑中翻译它。

例如：

DR ::= E and P
P ::= B | (and P)* | (or P)*
B ::= L | P (and L P)
L ::= a

Answer 1

就在这里。翻译表格产生式的一般模式

A ::= BC ... D

is to parphrase 是陈述性地解释为说

一个终端序列s是一个A（或者： A生成序列s，如果你更喜欢那个公式）如果：

• s是s_1、s_2、 ... s_n和

• s_1是一个B / B生成序列s_1，并且

• s_2是一个C / C生成的序列s_2，并且

• ...

• s_n是一个D / D生成的序列s_n。

假设我们使用generate谓词以显而易见的方式编写这些，并且我们可以使用 || 编写连接。运算符，您的第一条规则变为（如果我猜对了 E 和 P 是非终结符并且“and”是终结符）类似于

generates(DR,s) ⊃ generates(E,s1) 
                  ∧ generates(and,s2)
                  ∧ generates(P,s3)
                  ∧ s = s1 || s2 || s3
         

要确定后件（即证明s是A），请证明前件。只要语法确实生成了一些句子，并且只要您有一些前提定义了终结符号的“生成”关系，证明就会很简单。

Prolog 定子句语法是这种模式的一个很好的实例。我们中的一些人需要一些时间来理解和欣赏 DCG 中差异列表的使用，但是它们处理将s划分为子序列以及子序列与右侧不同部分的关联比简单的翻译要优雅得多进入上面给出的逻辑。