论文标题
统一的DLE-Logics逆通
Unified inverse correspondence for DLE-Logics
论文作者
论文摘要
通过利用SAHLQVIST对应关系背后的代数和秩序理论机制，统一对应关系为跨不同语义和签名的对应性和规范提供了强大的工具，涵盖了所有代数语义的逻辑，其代数语义是由正常（分布式）晶格扩展（引用为（D）LES）。特别是，每个（d）le中的参数算法有效地计算了（d）le诱导公式的一阶通讯员。我们提出了一种利用Alba的规则和代数语言将其步骤倒在DLE环境中的算法；因此，从其一阶通讯员开始有效地计算归纳公式。
By exploiting the algebraic and order theoretic mechanisms behind Sahlqvist correspondence, the theory of unified correspondence provides powerful tools for correspondence and canonicity across different semantics and signatures, covering all the logics whose algebraic semantics are given by normal (distributive) lattice expansions (referred to as (D)LEs). In particular, the algorithm ALBA, parametric in each (D)LE, effectively computes the first order correspondents of (D)LE-inductive formulas. We present an algorithm that makes use of ALBA's rules and algebraic language to invert its steps in the DLE setting; therefore effectively computing an inductive formula starting from its first order correspondent.
