带 MaxDiff 的数组理论的插值与原型嵌入（扩展版）
计算机科学中的逻辑
2021-01-21 v2
摘要
本文提出了 McCarthy 外延数组理论并辅以 maxdiff 操作（该操作返回两个给定数组不同的最大索引）的扩展。文献已知数组理论需要 diff 操作才能享受无量词层的 Craig 插值性质。然而，文献中引入的 diff 操作仅为此目的而设，仅有纯粹形式化意义（它来自外延性公理的 Skolem 化）。我们的 maxdiff 操作显著提升了表达力水平；然而，为所得理论获取插值结果成为一项出奇困难的任务。我们通过对该理论的模型及其原型嵌入性质进行深入的语义分析获得了此类结果。这些结果相对于索引理论是模块化的，并展示了如何通过分层方法将它们转化为具体的插值算法。
引用
@article{arxiv.2010.07082,
title = {Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version)},
author = {Silvio Ghilardi and Alessandro Gianola and Deepak Kapur},
journal= {arXiv preprint arXiv:2010.07082},
year = {2021}
}