重写逻辑

重写逻辑是一种对绝大多数编程语言和系统进行规范描述的计算机逻辑。重写逻辑能把目标逻辑的抽象语法表示为代数结构。利用重写规则，目标逻辑的推理规则可以被描述出来。重写逻辑中的语法和结构化公理都由用户自己定义，这使其变得极为简单且通用。1992年，José Meseguer在《作为统一并发模型的条件重写逻辑》一文中首先提出重写逻辑这一概念。重写逻辑中的基本公理是形如 t→t'的重写规则。重写规则有计算性解读与逻辑性解读两种解读方式。这两种不同的解读方式对应重写逻辑的两种应用价值：语义框架和逻辑框架。