Translating the Object Constraint Language into First-order Predicate Logic

Translating the Object Constraint Language into First-order Predicate Logic
复制标题

将对象约束语言转换为一阶谓词逻辑

DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
P. Schmitt
P. Schmitt
中科院分区：
--
文献类型：
--
作者：
Bernhard Beckert;U. Keller;P. Schmitt

文献摘要

被引文献

相似文献

在本文中，我们定义了一个翻译的UML类图与OCL约束到一阶谓词逻辑。目标是对UML模型进行逻辑推理，通过交互式定理证明器实现。我们把重点放在翻译产生的公式的可用性，我们已经开发了优化和算法，以提高定理证明过程的效率。翻译已经实现为KeY系统的一部分，但我们的实现也可以独立使用。
In this paper, we define a translation of UML class diagrams with OCL constraints into first-order predicate logic. The goal is logical reasoning about UML models, realized by an interactive theorem prover. We put an emphasis on usability of the formulas resulting from the translation, and we have developed optimisations and heuristics to enhance the efficiency of the theorem proving process. The translation has been implemented as part of the KeY system, but our implementation can also be used stand-alone.