合一
在逻辑和计算机科学中，合一（unification），是方程求解表达式之间方程的算法过程。例如，使用 x, y, z 作为变量，单元素集合解的方程{cons(x, cons(x, nil)) = cons(2, y)}是一个语法一阶合一问题，具有替换{x ↦ 2, y ↦ cons(2, nil)}作为其唯一解。 合一算法首先由雅克·埃尔布朗 ( 发现，而第一个正式研究可归因于 ，他使用一阶句法合一作为基本构建块他对一阶逻辑的归结过程的…
标签：#重写系统
共 3 篇文章
重写逻辑
在数学、计算机科学和逻辑学中，重写逻辑是把目标逻辑的抽象语法替换为代数结构，通过用其他术语表示公式子项的各种实现方法。利用重写规则，目标逻辑的推理规则可以被描述出来。 重写逻辑中的结构化公理和语法都由用户自己定义，这使其变得极为简单且通用。在最基本的形式中，一种重写的规则可适用多个规则。因此，当与适当的算法结合时，重写系统被视为绝大多数编程语言和系统应用程序进行规范描述的计算机逻辑，许多定理证明和宣告式编程语言是基于重写的。 1992年…
马尔可夫算法
马尔可夫算法是使用类似形式文法的规则在符号串上操作的字符串重写系统。马尔可夫算法被证明是图灵完全的，这意味着它们适合作为一般的计算模型，并可以用它的简单概念表示任何数学表达式。 Refal是基于马尔可夫算法的编程语言。 算法 #自顶向下依次检查规则，看是否能在符号串中找到任何在箭头左边的字符串。 #如果没有找到，停止执行算法。 #如果找到一个或多个，把符号串中的最左匹配的文字替换为在第一个相应规则的箭头右边的字符串。 #返回步骤1并继续…