重写逻辑
用另一個術語替換公式中的子項 / 维基百科,自由的 encyclopedia
在数学、计算机科学和逻辑学中,重写逻辑是把目标逻辑的抽象语法替换为代数结构,通过用其他术语表示公式子项的各种实现方法。利用重写规则,目标逻辑的推理规则可以被描述出来。[1][2][3] 重写逻辑中的结构化公理和语法都由用户自己定义,这使其变得极为简单且通用。在最基本的形式中,一种重写的规则可适用多个规则。因此,当与适当的算法结合时,重写系统被视为绝大多数编程语言和系统应用程序进行规范描述的计算机逻辑,许多定理证明和宣告式编程语言是基于重写的。[4][5][6]
此条目需要精通或熟悉相关主题的编者参与及协助编辑。 |
1992年,José Meseguer在《作为统一并发模型的条件重写逻辑》一文中首先提出重写逻辑这一概念。[7]