一句话：证明缺少有限模型性质的 Time Warp 代数仍具有可判定等式理论，并给出基于 Z3 的判定实现。
论文研究离散时间尺度 ω+ 上的保 join 映射，即 time warps。这类映射被提议作为 graded modalities，用于量化程序执行过程中信息的增长。time warps 的集合构成一个分配对合剩余格，称为 time warp algebra，并带有与应用相关的剩余运算。作者关注该代数的等式理论可判定性。他们证明，尽管该代数生成的 variety 不具有有限模型性质，其等式理论仍然是可判定的。为说明判定过程，作者还描述了用 OCaml 实现、并调用 Z3 定理证明器来判定该代数中方程的程序。该工作揭示了有限模型性质的缺失与等式可判定性可以分离，并为该代数的等式推理提供了可执行工具。
Join-preserving maps on the discrete time scale $\omega^+$, referred to as time warps, have been proposed as graded modalities that can be used to quantify the growth of information in the course of program execution. The set of time warps forms a simple distributive involutive residuated lattice -- called the time warp algebra -- that is equipped with residual operations relevant to potential applications. In this paper, we show that although the time warp algebra generates a variety that lacks the finite model property, it nevertheless has a decidable equational theory. We also describe an implementation of a procedure for deciding equations in this algebra, written in the OCaml programming language, that makes use of the Z3 theorem prover.
@article{paperbot2783,
title = {Deciding Equations in the Time Warp Algebra},
author = {Sam van Gool and Adrien Guatto and George Metcalfe and Simon Santschi},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 1},
year = {2024},
doi = {10.46298/lmcs-20(1:8)2024}
}