Relational analysis of algebraic datatypes
Relational analysis of algebraic datatypes
复制标题
代数数据类型的关系分析
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
D. Jackson
中科院分区：
文献类型：
--
作者：
Viktor Kunčak;D. Jackson
我们提出了一种技术，该技术可以使用有限模型查找，以检查预期模型是无限的某些公式的满意度。当使用集合和关系的语言来推理结构化值（例如代数数据类型）时，就会出现此类公式。我们技术的关键思想是在关系逻辑中确定一种自然的句法公式，以便将无限结构的推理降低为有限结构的推理。结果，当公式属于此类时，我们可以使用现有的有限模型查找工具来检查该公式是否在所需的无限模型中。
We present a technique that enables the use of finite model finding to check the satisfiability of certain formulas whose intended models are infinite. Such formulas arise when using the language of sets and relations to reason about structured values such as algebraic datatypes. The key idea of our technique is to identify a natural syntactic class of formulas in relational logic for which reasoning about infinite structures can be reduced to reasoning about finite structures. As a result, when a formula belongs to this class, we can use existing finite model finding tools to check whether the formula holds in the desired infinite model.