余归纳谓词的表现性逻辑

时间超活性的共归纳证明

Coinductive Proofs for Temporal Hyperliveness

针对时序超性质演绎证明系统匮乏的问题，提出用共归纳关系近似∀*∃*ψ型超性质，构建Coq中的机械化框架HyCo并验证其可靠性与实用性。

直觉主义不动点逻辑

Intuitionistic Fixed Point Logic

本文研究直觉主义不动点逻辑IFP，定义其可实现性解释以从证明中提取计算内容，证明其语义可靠性并给出Haskell翻译方法，还应用该方法提取了实数表示转换程序。

Mendler式Iso-（Co）归纳谓词：一种强规范化方法

Mendler-style Iso-(Co)inductive predicates: a strongly normalizing approach

我们提出了一个扩展的二阶逻辑AF 2与ISO风格的归纳和共归纳的定义，专门设计用于提取程序的原始（共）递归原则的手段证明一个拉Krivine Parigot。我们的逻辑包括原始的最小和最大不动点的谓词Transformers器的建设者，但与常见的方法相反，我们不限制自己的积极运营商，以确保单调性，而是我们使用的Mendler风格，动机在这里的概念单调化的任意运营商在一个完整的格。我们证明了一个充分性定理的基础上饱和集和饱和值函数的可实现性语义，因此，我们得到了强规范化属性的证明长期减少，一个重要的功能，这是在以前的相关工作中没有。

带Between谓词的双变量逻辑

Two-variable Logic with a Between Predicate

我们研究FO^2[<]的一个扩展，即用有限字解释的一阶逻辑，其中公式被限制为只使用两个变量。我们在这种语言中加入了两个变量的原子公式，即“字母a出现在位置x和y之间”。从某种意义上说，这是最简单的属性，仅使用两个变量是无法表达的。我们提出了几个逻辑，一阶和时间，具有相同的表达能力，并找到匹配的下限和上限的复杂性满足这些配方。我们还给出了一个有效的必要条件，在一个正则语言的语法幺半群，在这个逻辑中的一个属性是可表达的。我们证明，这个条件对于两个字母表上的单词也是足够的。这种代数分析使我们能够证明，除其他外，我们的新逻辑的表达能力严格低于完整的一阶逻辑FO[<]。

关于线性序表达能力的一个注记

A note on the expressive power of linear orders

本文证明了存在两个特殊的线性序，使得具有这两个线性序的一阶逻辑与具有位谓词FO（Bit）的一阶逻辑具有相同的表达能力。作为推论，我们得到：也存在一个内置置换，使得一阶逻辑具有线性序，并且这个置换与FO（Bit）一样具有表达性。

从闭谓词表达描述逻辑到数据变量的多项式重写

Polynomial Rewritings from Expressive Description Logics with Closed Predicates to Variants of Datalog

在许多情况下，完整和不完整的信息并存。出于这个原因，知识表示和数据库社区长期以来一直对在推理逻辑理论时同时支持封闭世界和开放世界的观点感兴趣。在这里，我们考虑使用逻辑理论查询可能不完整的数据的设置，形式化的本体介导的查询（OMQ），对查询与理论，有时称为本体，表达背景知识的评价。这可以通过从理论中指定一组封闭谓词来进一步丰富，这些谓词将在封闭世界假设下解释，而其余的则用开放世界观点来解释。通过这种方式，我们可以利用数据的部分完整性来检索更精确的查询答案。本文的中心目标是理解OMQ语言的相对表达能力，其中本体是用表达性描述逻辑（DL）ALCHOI编写的，并且包括一组封闭谓词。我们考虑一类有限的合取查询。我们的主要结果是表明，这种非单调查询语言中的每一个查询都可以在多项式时间内被翻译成稳定模型语义下的带否定的数据库。为了克服挑战，数据库没有直接的手段来表达存在的量化ALCHOI，我们定义了一个两个玩家的游戏，其特征在于本体的满意度，并设计了一个数据库查询，可以决定存在的获胜策略的游戏。如果没有封闭的谓词，也就是在查询一个普通的ALCHOI知识库的情况下，我们的翻译产生一个多项式大小的正析取数据库程序。据我们所知，不像以前的翻译相关片段表达（非霍恩）DL，这些是第一个多项式时间翻译。

实数域上带未解释一元谓词的差分逻辑的可判定性

Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates

研究了带未解释一元谓词的差分逻辑的可判定性，证明实数上带单个未解释一元谓词的量化差分逻辑不可判定，而整数差分逻辑结合实数序与未解释一元谓词仍可判定。

路径谓词模态逻辑的基本模型理论

Basic Model Theory for Path Predicate Modal Logic

研究路径谓词模态逻辑（PPML）基本模型理论，通过探讨定义亨尼斯 - 米尔纳类的方式及范·本特姆刻画定理，刻画其表达能力，分析处理PPML新特性的挑战与和标准方法的相似性。

一种精确表达的格理论网络验证框架

A Precise and Expressive Lattice-theoretical Framework for Efficient Network Verification

网络验证承诺通过逻辑分析控制或数据平面来检测错误，例如黑洞和转发循环。为了有效地这样做，最先进的技术（例如，Veriflow）将具有相同转发行为的数据包报头划分为相同的数据包等价类（PEC）。最近，Yang和Lam展示了如何构造PEC的最小集合，称为原子谓词。它们的构造使用二元决策图（BDD）。然而，BDD已被证明会导致每个数据包报头位的显着开销，在分析大规模数据中心时表现不佳。原子谓词的开销促使ddNF设计了一种专用的三进制位向量（TBV）数据结构。然而，TBV的表达严格低于BDD。此外，与原子谓词不同，ddNF的PEC集不是最小的。我们表明，ddNF的非极小是由于空PEC。此外，显示空PEC会触发错误的分析结果。这揭示了在正式网络验证中精确度、表现力和性能之间的内在紧张关系。我们的论文通过一种新的格理论PEC构造算法#PEC解决了这种紧张局势，该算法如下所述地推进了该领域：（i）#PEC可以编码更多种类的转发规则（例如，ip-tables），（ii）#PEC验证更宽类别的错误（例如，阴影规则）比ddNF，以及（iii）在广泛的真实世界数据集上，#PEC比原子谓词快10倍。通过实现精度，表现力和性能，本文回答了一个长期的追求，跨越了三代正式的网络分析技术。

偏极逻辑的共诱导证明搜索及其在全直觉命题逻辑中的应用

Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic

本文提出共诱导证明搜索方法，扩展至偏极直觉逻辑LJP，并通过解释将该方法应用于其他直觉逻辑系统，实现了解的可判定性继承。

一阶模谓词逻辑中的一个量词替换

One Quantifier Alternation in First-Order Logic with Modular Predicates

添加模谓词产生了一阶逻辑FO在词上的推广。FO[<，MOD]与顺序比较$x<y$和$x \equiv i \mod n$的谓词的表达能力已经由Barrington，Compton，Straubing和Therien研究过。FO[<，MOD]-片段的研究由Chaubard，Pin和Straubing发起。最近，Dartois和Paperman证明了双变量片段FO 2 [<，MOD]中的可定义性是可判定的。在本文中，我们继续这一工作路线。我们给出了Sigma 2 [<，MOD]中词语言的一个有效的代数刻画.片段Sigma 2由前束范式中的一阶公式组成，具有以存在块开始的两个量词块。此外，我们还证明了Sigma 2 [<，MOD]的最大子类Delta 2 [<，MOD]在否定下是封闭的，它具有与二元逻辑FO 2 [<，MOD]相同的表达能力。这将Therien和Wilke的结果FO 2 [<] = Delta 2 [<]推广到模块化谓词。作为副产品，我们获得了FO 2 [<，MOD]的另一个可判定的特征。

度量时态逻辑何时表达完备？

When is Metric Temporal Logic Expressively Complete?

Kamp的一个开创性的结果是，在实数上，线性时态逻辑（LTL）具有与具有二元顺序关系<和一元谓词的一阶逻辑相同的表达能力。一个关键的问题是是否存在一个类似的度量时态逻辑（MTL）的坎普定理-一个推广的LTL中，直到和因为模态注释的区间表示度量约束。Hirshfeld和Rabinovich给出了否定的回答，证明了具有二元序关系<和一元函数+1的一阶逻辑严格地比具有整数常数的MTL更有表达性。然而，Hunter，Ouaknine和Worrell最近的一个结果表明，在合理的定时常数下，MTL具有与一阶逻辑相同的表达能力，给出了肯定的答案。在本文中，我们推广了这些结果，给出了一个精确的表征，MTL和一阶逻辑具有相同的表达能力的常数集。我们还表明，完整的一阶表达可以恢复与计数方式，强烈支持的断言Hirshfeld和Rabinovich的Q2 MLO是最具表达性的可判定的片段FO（<，+1）。

Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down

The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, we identify a general fibrational condition for the IA-FC coincidence, namely in the fiber over an initial algebra in the base category. Identifying (co)algebras in a fiber as (co)inductive predicates, our fibrational IA-FC coincidence allows one to use coinductive witnesses (such as invariants) for verifying inductive properties (such as liveness). Our general fibrational theory features the technical condition of st…

鹤滩上的裂缝：次度谓词

A Crevice on the Crane Beach: Finite-Degree Predicates

本文证明了词上的一阶逻辑（FO）与配备有限数量谓词集的FO是等表达的，即顺序、二元谓词MSB $_0$和有限度谓词：FO[Arb] = FO[<，MSB $_0$，Fin]. Crane Beach Property（CBP）是在十多年前提出的，如果所有允许使用中性字母的可表达语言都是正则的，那么CBP就是一个逻辑。虽然已知FO[Arb]不具有CBP，但是这里示出了CBP的（强形式）对于FO[<，Fin]和FO[<，MSB $_0$ ]都成立。因此，FO[<，Fin]表现出局部性和CBP的形式，并且仍然可以表达各种各样的语言，而与FO[Arb]的表达能力相差一个简单的谓词。作为应用，研究了FO[<，Fin]的计数能力.

余代数谓词逻辑的模型论与证明论

Model Theory and Proof Theory of Coalgebraic Predicate Logic

本文提出一种基于Set-余代数的通用对应语言，推广一阶逻辑，研究其公理化、完备性、表达能力及模型论性质，并建立相继式系统的消割结果。

Two Results on Separation Logic With Theory Reasoning

Two results are presented concerning the entailment problem in Separation Logic with inductively defined predicate symbols and theory reasoning. First, we show that the entailment problem is undecidable for rules with bounded tree-width, if theory reasoning is considered. The result holds for a wide class of theories, even with a very low expressive power. For instance it applies to the natural numbers with the successor function, or with the usual order. Second, we show that every entailment problem can be reduced to an entailment problem containing no equality (neither in the formulas nor in…

Temporal Stream Logic modulo Theories (Full Version)

Temporal stream logic (TSL) extends LTL with updates and predicates over arbitrary function terms. This allows for specifying data-intensive systems for which LTL is not expressive enough. In the semantics of TSL, functions and predicates are left uninterpreted. In this paper, we extend TSL with first-order theories, enabling us to specify systems using interpreted functions and predicates such as incrementation or equality. We investigate the satisfiability problem of TSL modulo the standard underlying theory of uninterpreted functions as well as with respect to Presburger arithmetic and the …

An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic

An efficient entailment proof system is essential to compositional verification using separation logic. Unfortunately, existing decision procedures are either inexpressive or inefficient. For example, Smallfoot is an efficient procedure but only works with hardwired lists and trees. Other procedures that can support general inductive predicates run exponentially in time as their proof search requires back-tracking to deal with a disjunction in the consequent. This paper presents a decision procedure to derive cyclic entailment proofs for general inductive predicates in polynomial time. Our pro…

关于Bernays-Schönfinkel-Ramsey分离逻辑的表达完备性

On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic

本文研究了$\exists^*\forall^*$语言中带有量词前缀的前向公式的分离合取和蕴涵无限制嵌套的分离逻辑在可能位置论域为可数无限或有限的情况下的可满足性问题.与带有未解释谓词和等式的一阶逻辑类似，我们称这个片段为伯奈斯-舍恩芬克尔-拉姆齐分离逻辑[BSR（SLk）]。我们表明，不同于在一阶逻辑中，（在）有限可满足性问题是不可判定的BSR（SLk），我们定义了两个非平凡的子集，这是可判定的有限和无限的可满足性，分别通过控制的范围内的普遍量化变量的出现分离的影响，以及后者的出现的极性。可判定性结果是通过分离连接词的受控消除获得的，描述为（i）将前束形式分离逻辑公式有效地翻译成少量\emph{test formulae}的组合，仅使用一阶连接词，随后（ii）将后者翻译成可均衡满足的一阶公式。

名义转换系统的模态逻辑

Modal Logics for Nominal Transition Systems

本文为名义转换系统定义了通用模型及Hennessy-Milner逻辑，证明其充分且表达完备，并系统处理多种互模拟变体，已在Nominal Isabelle中形式化。

LPrL：一种异步线性时间超逻辑

LPrL: An Asynchronous Linear Time Hyper Logic

LPrL是一种异步线性时间超逻辑，通过扩展LTL并引入术语和等式谓词，实现了可满足性和模型检验问题的初等时间解法，与同步HyperLTL形成对比。

可分解结构的序不变性

Order Invariance on Decomposable Structures

顺序不变公式访问结构论域上的顺序，但模型关系与所使用的顺序无关。顺序不变性经常用于计算机科学中基于逻辑的方法。序不变公式捕捉复杂类的无序问题，并且它们对数据库查询的答案与数据库的低级方面的独立性进行建模。我们研究了顺序不变的一元二阶（MSO）和一阶（FO）逻辑的表达能力的限制类的结构，承认某些形式的树分解（不一定有界宽度）。虽然顺序不变的MSO是更有表现力的MSO，甚至，CMSO（MSO与模计数谓词），我们表明，顺序不变的MSO和CMSO是同样有界树宽度的图形和平面图上的表达。这扩展了早期的结果树由于Courcelle。此外，我们表明，所有的性质定义在顺序不变的FO也定义在MSO对这些类。这些结果是一个定理的应用，该定理展示了如何将顺序不变逻辑的可定义性结果从图的树分解的袋子提升到图本身。

域、信息框架及其逻辑

Domains, Information Frames, and Their Logic

本文研究连续信息框架、连续信息系统及其范畴关系，证明相关范畴等价，并引入连续分层合取逻辑以增强表达力。

一种用于递归程序的可表达迹逻辑

An Expressive Trace Logic for Recursive Programs

本文提出一种基于迹公式的可表达逻辑，为递归程序提供组合式指称语义和证明演算，并建立程序与公式间的 Galois 连接，揭示程序构造与逻辑连接词的对应关系。

低秩MSO

Low rank MSO

该研究引入低秩MSO这一图性质描述新逻辑，证明其在弱稀疏图类、有界VC维图类及所有图上分别与分隔符逻辑、翻转连通性逻辑、翻转可达性逻辑表达能力等价，并指出无向图中其可表达性质可多项式时间判定。

具有无穷量词的一元谓词逻辑的模型论

Model Theory of Monadic Predicate Logic with the Infinity Quantifier

本文建立了模型理论性质的$\mathrm{FOE}^{\infty}$，一元一阶逻辑的变化，具有广义量词$\exists^\infty$（“有无限多”）。我们提供了语法定义的片段$\mathrm{FOE}^{\infty}$表征四个不同的语义属性的$\mathrm{FOE}^{\infty}$ -句子：（1）是单调的和（2）（斯科特）连续在一个给定的一元谓词集;（3）有真理下保持采取子模型或（4）不变量下采取继承。在每一种情况下，我们产生一个有效定义的映射，将任意句子$φ$翻译成属于相应句法片段的句子$φ^{p}$，其属性是$φ$等同于$φ^{p}$，当它具有相关的语义属性时。我们的方法是首先提供这些结果在更简单的设置一元一阶逻辑（$\mathrm{FOE}$）和（$\mathrm{FO}$）的平等，然后移动到$\mathrm{FOE}^{\infty}$包括广义量词$\exists^\infty$到图片。作为我们的推论，我们得到了上述四个语义性质对于$\mathrm{FOE}^{\infty}$ -语句是可判定的。此外，我们的结果是直接相关的自动机和表达模bisimilirity的一元二阶逻辑的变种的特征。该应用程序是在一个配套文件中开发的。

Hennessy-Milner Theorems via Galois Connections

We introduce a general and compositional, yet simple, framework that allows us to derive soundness and expressiveness results for modal logics characterizing behavioural equivalences or metrics (also known as Hennessy-Milner theorems). It is based on Galois connections between sets of (real-valued) predicates on the one hand and equivalence relations/metrics on the other hand and covers a part of the linear-time-branching-time spectrum, both for the qualitative case (behavioural equivalences) and the quantitative case (behavioural metrics). We derive behaviour functions from a given logic and …

论角色逻辑

On Role Logic

我们提出的角色逻辑，一个符号的关系结构的形状分析，数据库和知识库中描述的属性。我们使用de Bruijn的λ演算符号的思想来构造角色逻辑，在λ演算中编码一阶逻辑，以及一元和二元谓词的隐式参数的简单规则。角色逻辑的无限制版本具有传递闭包的一阶逻辑的表达能力。通过对角色逻辑公式的句法限制，我们识别出角色逻辑的一个自然片段RL ^2。我们证明了RL^2片段与计数C^2的二元逻辑具有相同的表达能力，因此是可判定的。我们提出了一个翻译的命令式语言到可判定的片段RL ^[2]，它允许组合验证的程序，操纵关系结构。此外，我们展示了RL^2如何编码布尔形状分析约束和一个富有表现力的描述逻辑。

为HER做这件事：在强化学习中使用一阶时间逻辑奖励规范（扩展版）

Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version)

本文提出了一种基于LTLfMT的一阶时间逻辑奖励规范框架，结合奖励机和HER解决奖励稀疏性问题，适用于连续控制任务。

无限变迁系统的同步积的模型检验

Model Checking Synchronized Products of Infinite Transition Systems

使用模型检验范式的形式化验证必须处理两个方面：系统模型是结构化的，通常是组件的产品，规范逻辑必须具有足够的表达能力，以允许可达性属性的形式化。本文研究了在这些前提下，无限转移系统可以得到什么样的结果。作为模型，我们考虑产品的无限过渡系统具有不同的同步约束。我们引入了可达同步变迁系统，即只包含可达（参数化）同步变迁的产品系统，并证明了产品系统的可达谓词扩展的一阶逻辑FO（R）的可判定性可归结为组件的FO（R）的可判定性.这个结果在以下意义上是最优的：（1）如果我们允许半有限同步，即仅在一个分量中有无穷多个转移是同步的，则乘积系统的FO（R）-理论一般是不可判定的。(2)我们不能扩展所考虑的逻辑的表达能力。已经有一个弱扩展的一阶逻辑与传递闭包，我们限制传递闭包运算符arity 1和嵌套深度2，是不可判定的异步（因此同步）产品，即无限网格。

Expressivity of Planning with Horn Description Logic Ontologies (Technical Report)

State constraints in AI Planning globally restrict the legal environment states. Standard planning languages make closed-domain and closed-world assumptions. Here we address open-world state constraints formalized by planning over a description logic (DL) ontology. Previously, this combination of DL and planning has been investigated for the light-weight DL DL-Lite. Here we propose a novel compilation scheme into standard PDDL with derived predicates, which applies to more expressive DLs and is based on the rewritability of DL queries into Datalog with stratified negation. We also provide a ne…

迈向关联Ciao断言与LPTP定理

Towards Relating Ciao Assertions and LPTP Theorems

研究关联Ciao断言与LPTP定理，提出系统翻译方案，根据逻辑可编码性描述断言类，为不可译情况提策略与构造，分析权衡，实现Ciao断言检查与LPTP演绎验证紧密集成，发挥互补能力。

基于可计算性逻辑的应用理论

Towards applied theories based on computability logic

可计算性逻辑（Computability Logic，CL）（见http：//www.cis.upenn.edu/linggiorgi/cl.html）是一个最近启动的程序，用于将逻辑重新发展为可计算性的形式理论，而不是逻辑更传统的形式真值理论。其中的公式代表计算问题，“真理”意味着算法解决方案的存在，而证明则对这些解决方案进行编码。在致力于寻找公理化的CL更有表现力的片段的研究路线，本文介绍了一个新的演绎系统CL 12，并证明了其可靠性和完整性方面的语义CL。保守地扩展了经典谓词演算，并提供了相当多的额外的表达和演绎能力，CL 12提出了一个合理的，计算上有意义的，建设性的替代经典逻辑作为应用理论的基础。为了获得这种理论的模型实例，本文将传统的基于经典逻辑的Peano算法重建为基于可计算性逻辑的Peano算法。本贡献的目的之一是提供一个起点，作者希望，可能成为一个新的研究路线与潜在的有趣的发现-一个探索的可能是相当不寻常的元理论CL为基础的算术和其他CL为基础的应用系统。