一阶约束逻辑——一种范畴无关的方法
计算机科学中的逻辑
2021-01-07 v1 软件工程
摘要
基于我们在代数规范、抽象模型论、图变换以及模型驱动软件工程(MDSE)等领域的经验，我们提出了一种通用的、范畴无关的“一阶约束逻辑”(LFOC)方法。传统一阶逻辑、描述逻辑以及草图框架被作为示例加以讨论。我们以 institution 的概念[Diaconescu08,GoguenBurstall92]为指导来描述 LFOC。主要结果表明，我们所将描述的六个参数的任意选取，都会给出一个相应的“约束 institution”。约束 institution 的“表示”可被刻画为“一阶草图”。作为[Makkai97]中“草图 entailment”的对应变体，我们最终引入“草图规则”以赋予 LFOC 所需的表达能力。
引用
@article{arxiv.2101.01944,
title = {Logics of First-Order Constraints -- A Category Independent Approach},
author = {Uwe Wolter},
journal= {arXiv preprint arXiv:2101.01944},
year = {2021}
}
备注
23 pages, presented at the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019), London, UK, June 3-6, 2019