An Improved Proof-Theoretic Compilation of Logic Programs
在以前的工作中，我们表明，逻辑编程编译可以给出一个通用的抽象逻辑程序设计语言的证明理论的理由，并证明了这种技术的情况下，遗传Harrop公式及其线性变体。编译后的子句本身就是逻辑公式，除了在与它们的头相匹配的原子目标上存在二阶抽象。在本文中，我们重新审视我们以前的结果，以更详细和更充分的逻辑理由，消除这种虚假的抽象。然后，我们改进所得到的技术，以有效地支持模式良好的程序。
2012-10-05 cs.LO cs.PL
Description Logics with Abstraction and Refinement
Leipzig University（莱比锡大学）；Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI)（可扩展数据分析与人工智能中心（ScaDS.AI））
本文提出一种支持多级抽象的描述逻辑扩展，引入概念和角色的抽象与精化显式算子，证明了推理可判定性并精确确定了逻辑复杂度。
2023-10-20 cs.AI cs.LO
Logic is Algebra
本文指出逻辑本质上是代数，并强调只有在正确使用抽象代数与抽象逻辑的前提下，两者才能等同。
2023-04-01 cs.LO
Polyvariant Program Specialisation with Property-based Abstraction
在本文中，我们表明，基于属性的抽象，一个既定的技术起源于软件模型检验，是一个灵活的方法，在标准的在线专业化算法控制程序专业化的多变量。专业化是一种程序转换，它根据限制其行为的给定约束来转换程序。多变量专业化是指生成同一程序代码的两个或多个专业化版本。在计算过程中，同一个程序点可以不止一次地达到，每种情况下都有不同的约束条件，而多变量专业化允许实现不同的专业化。基于属性的抽象使用属性的有限集合来定义谓词的抽象版本的有限集合，确保仅生成有限数量的专用版本。属性的特定选择对于多元性至关重要;太少的版本可能导致专业化不足，而太多的版本可能导致代码大小的增加，而没有相应的效率增益。使用实例，我们展示了基于属性的抽象专业化的灵活性，并讨论了其在控制流细化，验证，终止分析和基于维度的专业化。
2019-08-20 cs.LO cs.PL
Logical Characterizations of Heap Abstractions
形状分析关注的问题，确定“形状不变量”的程序，执行破坏性更新动态分配的存储。在最近的工作中，我们已经展示了如何使用基于3值一阶逻辑的抽象解释进行形状分析。在这项工作中，具体的存储是有限的2值逻辑结构，并且在执行期间可能出现的存储集合使用有限的3值逻辑结构的某个族来表示（保守地）。在本文中，我们展示了如何在形状分析中出现的3值结构可以使用具有传递闭包的一阶逻辑中的公式来表征。我们还定义了一个非标准的（“超赋值”）语义的3值一阶逻辑，比传统的3值语义更精确，并证明了超赋值语义可以有效地实现使用现有的定理证明。
2005-03-16 cs.LO
Automatic Probabilistic Program Verification through Random Variable Abstraction
最弱预期望演算已被证明是分析概率和不确定性规划定量性质的成熟理论。我们提出了一个自动的方法证明定量线性性质的任何可数状态空间使用迭代向后不动点计算的一般框架中的抽象解释。为了完成这一任务，我们提出了随机变量抽象（RVA）的技术，我们还假设了一个充分条件，实现精确的不动点计算的抽象域。我们的方法的可行性示出了两个例子，一个获得的概率程序的预期运行时间，和其他的赌博策略的预期收益。我们的方法适用于一般的保护概率和不确定性的过渡系统，而不是普通的pGCL程序，使我们能够很容易地模拟广泛的系统，包括分布式的和非结构化的程序。我们提出了该程序的操作和最弱前提语义，并证明了它的等价性。
2010-06-26 cs.LO cs.PL
Temporal logic with predicate abstraction
考虑了一个没有量词但具有谓词抽象机制和等式的谓词线性时态逻辑LTL_{λ,=}。LTL_{λ,=}的模型可以很自然地看作是在某些（可能是无限的）域的元素上移动的卵石（柔性常数）系统。这允许使用LTL_{λ,=}的规范的动态系统使用一些资源，如使用内存位置，移动代理占用一些网站等的进程。另一方面，我们表明，LTL_{λ,=}是不是递归axiomatizable，因此，LTL_{λ,=}规范的全自动验证是不，一般来说，可能的。
2004-10-27 cs.CL cs.LO
From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions
允许-名义逻辑（Permissive-Nominal Logic，PNL）是一阶谓词逻辑的扩展，它包含了可以在其参数中绑定名称的项形成器。它在（许可的）名义集合中采用语义。在PNL中，形式量词或形式结合符只是满足公理的项形成符，它们的表示是名义原子抽象上的函数。然后我们有高阶逻辑（HOL）和它在普通集合（即Zermelo-Fraenkel）中的模型; forall或lambda的表示是全函数空间或部分函数空间上的函数。这就提出了以下问题：这两种绑定模型是如何连接的？在PNL和HOL之间，以及在名义集合和函数之间，什么样的转换是可能的？我们展示了翻译的PNL到HOL，并从模型的PNL到某些模型的HOL。这是自然的，但也是部分的：我们将一个受限制的子系统完整的PNL HOL。不平移的额外部分是名义集合关于置换的对称性。使用一点名义上的行话：我们可以翻译名称和绑定，但不能翻译它们的名义等变性。这似乎是合理的，因为HOL和普通集合不是等变的。因此，通过这种翻译，PNL和HOL和他们的模型做不同的事情，但他们享受非平凡和丰富的子系统是同构的。
2011-11-20 cs.LO
On Feller Continuity and Full Abstraction (Long Version)
我们研究了应用双相似性的性质在$λ$ -演算赋予运营商从连续分布的采样。一方面，我们表明，双相似性，逻辑等价，测试等价都符合上下文等价时，实数只能通过连续函数进行操作。实现这一结果的关键因素是一个新的概念，标记马尔可夫过程，我们相信独立的利益，是一个广泛的一类LMP的共归纳和逻辑启发的等价物相吻合的费勒连续性。另一方面，我们表明，如果没有限制的方式实数被操纵，表征上下文等价原来是困难的，大多数上述概念的等价甚至是不健全的。
2022-07-21 cs.LO cs.PL
Nominal Abstraction
递归关系规范通常用于描述形式系统的计算结构。最近的研究证明理论已经确定了两个功能，促进直接的，基于逻辑的推理这样的描述：通过递归定义的原子判断的解释和编码的约束结构通过通用的判断。然而，包含这两个特征的逻辑目前不允许定义体现与绑定相关的动态方面的关系，这是许多推理任务所需的能力。我们提出了一个新的术语之间的关系称为名义抽象作为克服这一缺陷的一种手段。我们将名义抽象到一个丰富的逻辑，也包括定义，通用量化，归纳，并共同归纳，然后我们证明是一致的。我们提出的例子表明，这种逻辑可以提供优雅的治疗绑定的情况下，出现在许多证明，如那些建立属性的类型演算和任意级联替代，在reductionalarguments中发挥作用。
2010-09-23 cs.LO
Automatic Modular Abstractions for Linear Constraints
提出了一种通过抽象解释自动生成用于静态分析的抽象Transformers的方法。该方法的重点是对程序的线性约束，操作合理的，真正的或浮点变量，并包含线性分配和测试。除了无循环代码，同样的方法也适用于获得最小不动点作为前提条件的函数，这允许分析循环和递归函数。我们的算法是基于新的量词消去和符号操作技术。给定一个抽象域的规范和一个程序块，我们的方法自动输出相应的抽象Transformer的实现。因此，它是程序转换的一种形式。我们工作的动机是数据流同步程序设计语言，用于构建控制命令嵌入式系统，但它也适用于命令式和函数式编程。
2008-11-02 cs.LO cs.PL
Automatic modular abstractions for template numerical constraints
提出了一种通过抽象解释自动生成用于静态分析的抽象Transformers的方法。该方法的重点是对程序的线性约束，操作合理的，真正的或浮点变量，并包含线性分配和测试。除了无循环代码，同样的方法也适用于获得最小不动点作为前提条件的函数，这允许分析循环和递归函数。我们的算法是基于新的量词消去和符号操作技术。给定一个抽象域的规范和一个程序块，我们的方法自动输出相应的抽象Transformer的实现。因此，它是程序转换的一种形式。我们工作的动机是数据流同步程序设计语言，用于构建控制命令嵌入式系统，但它也适用于命令式和函数式编程。
2010-05-31 cs.LO cs.PL
A Survey of the Proof-Theoretic Foundations of Logic Programming
一些形式系统，如归结和最小模型语义，为逻辑编程提供了一个框架。在本文中，我们将调查使用结构证明理论作为替代基础。在过去的35年里，研究人员一直在使用这个基础来将逻辑编程从一阶经典逻辑的根源提升到直觉和线性逻辑的高阶版本。这些更具表现力的逻辑程序设计语言允许捕获有状态计算和丰富形式的抽象，包括高阶编程、模块化和抽象数据类型。术语级绑定是另一种抽象，在证明理论和这些扩展逻辑程序设计语言中，它们都得到了优雅而直接的处理。逻辑编程也激发了证明理论的新成果，例如涉及极性和聚焦证明的成果。这些最新的研究结果提供了一个高层次的手段，呈现前向链和后向链风格推理之间的差异。在证明论中验证逻辑编程也有助于识别它与函数式编程、演绎数据库和模型检验的联系和区别。
2021-10-30 cs.LO cs.PL
Bridge and Bound: A Logic-Based Framework for Abstracting (Extended Report)
University of Warsaw（华沙大学）
本文提出了一种基于逻辑的抽象框架，通过引入充分条件和分层抽象，实现复杂系统的分层简化。
2026-01-03 cs.LO
A Relational Program Logic with Data Abstraction and Dynamic Framing
饰Tony Hoare霍尔在1972年发表的一篇论文中阐述了隐藏不变量和模拟的基本概念。隐藏：封装数据表示的不变量不需要在包含模块API的规范中提及。模拟：可以通过使用封装状态上定义的耦合关系证明旧实现和新实现之间的模拟来确定新数据表示和实现的正确性。这些结果在语义上被形式化，并且是针对一个简单的状态模型，尽管该论文声称这可以扩展到包含动态分配的对象。近年来，已经取得了进展，正式的索赔，模拟，虽然主要是在语义的发展。在这篇文章中，隐藏和模拟结合了Hoare 1969年论文中的思想：程序逻辑。对于一个基于对象的语言与动态分配，我们引入了一个关系霍尔逻辑与状态框架条件，形式化封装，隐藏的不变量，和耦合，涉及两个实现。关系和其他断言用一阶逻辑表示。规范可以表达广泛的关系属性，如条件等价和不干扰解密。证明规则通过方便的对齐来促进关系推理，并且相对于传统的操作语义被示出为合理的。导出的链接程序等价性证明规则直接体现了表示独立性。具有代表性的例子的适用性证明使用基于SMT的实现。
2022-07-19 cs.LO cs.PL
On Quasi-Interpretations, Blind Abstractions and Implicit Complexity
准解释是一种保证一阶函数程序复杂性界限的技术：通过终止排序，它们给出了一个程序在多项式时间内可执行的充分条件，这里称为P-准则。为了更好地理解程序的内涵表达能力，我们研究了满足P-准则的程序的性质。给定一个二进制列表上的程序，它的盲抽象是通过将列表替换为它们的长度（自然数）而获得的不确定性程序。如果一个程序的盲抽象在多项式时间内终止，则该程序是盲多项式的。我们表明，所有的程序满足的P-准则的变种，实际上是盲目的多项式。然后，我们给出了两个扩展的P-准则：一个通过放松的终止序条件，和其他一个（有界值属性）给出了一个必要和充分条件的程序是多项式时间可执行的，与memoisation。
2006-08-06 cs.CC cs.LO cs.PL
Go with the Flow: Compositional Abstractions for Concurrent Data Structures (Extended Version)
并发分离逻辑有助于显着简化并发数据结构的正确性证明。然而，这种证明中反复出现的问题是，由于复杂的共享和覆盖，在顺序设置中工作良好的数据结构抽象在并发设置中更难推理。为了解决这个问题，我们提出了一种新的方法来抽象区域的堆编码的数据结构不变到一个局部条件的每个节点。该条件可以取决于与在整个堆图上被计算为固定点的节点相关联的量。我们把这个量称为流量。流可以编码堆的结构属性（例如从根形成树的可达节点）以及数据不变量（例如排序）。然后，我们引入了流接口的概念，它表示依赖和保证堆区域施加在其上下文上，以保持局部流相对于全局堆不变。我们的主要技术成果是，这个概念导致了一个新的语义模型的分离逻辑。在这个模型中，流接口提供了一个通用的抽象机制来描述复杂的数据结构。这种抽象机制允许在各种各样的数据结构上推广的证明规则。为了证明我们的方法的多功能性，我们展示了如何扩展逻辑RGSep流接口。我们已经使用这种新的逻辑来证明非平凡并发数据结构的线性化和内存安全性。特别是，我们获得参数线性化证明并发字典算法，抽象的底层数据结构表示的细节。使用现有的分离逻辑提供的抽象机制，这些证明不能容易地表达。
2017-11-09 cs.DS cs.LO cs.PL
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
研究正确性与错误性变换程序逻辑，扩展以处理终止与非终止，证明其为自然关系语义的抽象解释，提供计算化方法设计可靠完备证明系统，并扩展 Hoare 逻辑及设计新前置条件逻辑。
2023-11-23 cs.LO
A proof-theoretic approach to abstract interpretation
Google Inc.（谷歌公司）；Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；University of Johannesburg（约翰内斯堡大学）；University of Luxembourg（卢森堡大学）；INRIA（法国国家信息与自动化研究所）
本文通过将逻辑系统与有限抽象系统关联，提出了一种生成与抽象格同构的Lindenbaum-Tarski代数的逻辑的通用程序，并建立了相应的可靠性和完备性结果。
2026-05-26 cs.LO math.LO
Automatic Modular Abstractions for Template Numerical Constraints
提出了一种通过抽象解释自动生成用于静态分析的抽象Transformers的方法。该方法的重点是对程序的线性约束，操作合理的，真正的或浮点变量，并包含线性分配和测试。给定一个抽象域的规范和一个程序块，我们的方法自动输出相应的抽象Transformer的实现。因此，它是程序转换的一种形式。除了无循环代码，同样的方法也适用于获得最小不动点作为前提条件的函数，这允许分析循环和递归函数。我们工作的动机是数据流同步程序设计语言，用于构建控制命令嵌入式系统，但它也适用于命令式和函数式编程。我们的算法是基于线性算术公式上的量词消去和符号操作技术。我们也给出了非线性约束和非线性程序结构的一般结果。
2010-05-26 cs.LO cs.PL
An expectation transformer approach to predicate abstraction and data independence for probabilistic programs
在本文中，我们重新审视了著名的谓词抽象技术，将概率系统模型的性能属性。我们重铸的理论，使用期望Transformers，并确定Transformer属性对应的抽象，但产生精确的约束无限状态概率系统的性能。此外，我们扩展开发的技术的特殊情况下，“数据独立”的程序，将概率。最后，我们证明了微妙的扩展技术，通过使用PRISM模型检验工具来分析一个无限状态协议，获得其性能的精确界限。
2010-06-26 cs.LO
Proceedings 29th and 30th Workshops on (Constraint) Logic Programming and 24th International Workshop on Functional and (Constraint) Logic Programming
（约束）逻辑编程研讨会（WLP）是德国逻辑编程学会（Gesellschaft für Logische Programmierung e.V.，GLP），并汇集了对逻辑编程、约束编程、答案集编程以及数据库和人工智能等相关领域感兴趣的研究人员（不仅来自德国）。函数和（约束）逻辑编程国际研讨会（WFLP）旨在汇集对函数编程，逻辑编程及其集成感兴趣的研究人员，学生和从业者。讲习班有一个共同地点的传统，以促进对高级声明性程序设计语言和相关领域的基础、应用和组合感兴趣的社区之间的跨部门思想和经验交流。
2016-12-31 cs.LO cs.PL
Reasoning About TSO Programs Using Reduction and Abstraction
我们提出了一种方法，用于证明在总存储排序（TSO）内存模型下运行的程序是鲁棒的，即，它的所有TSO计算等价于在顺序一致性（SC）语义下的计算。该方法受Lipton的约简理论的启发，证明了并发程序的原子性。对于程序是不强大的，我们引入了一个抽象机制，允许构建强大的程序过近似他们的TSO语义。这使得使用的证明方法设计的SC语义在证明不变量举行的TSO语义的非鲁棒程序。这些技术已经评估了一个大型的基准测试，使用CIVL，一个通用的工具，推理下的SC语义并发程序提供的基础设施。
2018-04-14 cs.LO
Omission-based Abstraction for Answer Set Programs
抽象是一种众所周知的简化复杂问题的方法，通过故意丢失信息来过度近似它。到目前为止，在回答集编程（ASP）中还没有考虑到它，这是一个解决问题的方便工具。我们介绍了一种自动抽象ASP程序的方法，该方法通过减少词汇表同时确保过度近似（即，每个原始答案集映射到某个抽象答案集）。这允许生成可以帮助近似推理的部分答案集候选。由于搜索空间较小，计算抽象答案集直观上更容易，但代价是遇到虚假答案集。忠实（非虚假）的抽象可以用来表示投影的答案集，并在答案集构造中指导求解器。为了处理虚假的答案集，我们采用了ASP调试方法来帮助抽象细化，它确定原子被严重忽略，并将它们添加回抽象中。作为一个展示的情况下，我们应用抽象来解释ASP程序的阻塞集，这是一组原子，使抽象到他们保留不可满足性方面的不可满足性。实验结果证明了它们的实用性。
2020-04-03 cs.LO
Exact Separation Logic (Extended Version)
本文提出精确分离逻辑（ESL），一种既能验证所有终止行为又能确保结果可达的逻辑，首次实现 UX 逻辑的函数组合性，并探讨了抽象在 UX 推理中的作用。
2023-08-30 cs.LO cs.PL
Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Systems
我们调查程序等价的线性高阶（顺序）语言赋予计算效果的原语。更具体地说，我们研究了基于操作的概念的程序等价的线性$λ$ -演算明确复制和代数效果\emph{à la} Plotkin和电源。这样的演算明确了复制和线性之间的相互作用，这是计算的内涵方面，而效果是\emph{extensional}。我们回顾了一些文献中提出的线性结石等价的概念，并显示其局限性时，适用于有效的结石复制是一等公民。然后，我们引入资源转换系统，即转换系统的状态是建立在元组的程序表示可用的资源，作为一个操作语义会计程序的内涵和外延的交互行为。我们的主要结果是一个健全的和完整的表征上下文等价的跟踪等价定义的资源转移系统。
2021-06-24 cs.LO cs.PL
Abstraction and Acceleration in SMT-based Model-Checking for Array Programs
抽象（以其各种形式）是模型检验中一种强大的既定技术;然而，当涉及无界数据结构时，它并不总是以令人满意的方式处理发散现象。加速是一种广泛应用的避免发散的方法，但它主要应用于整数规划。本文讨论了无界数组的加速转换关系问题，最终目标是避免抽象程序可达性分析过程中的发散。为此，我们首先设计了一种格式来计算在这个域中的加速度，然后我们展示了如何适应所谓的“单调抽象”技术，以有效地处理复杂的公式与嵌套的量词所产生的加速预处理。值得注意的是，我们的技术可以很容易地插入到抽象/细化循环，并大大有助于避免发散：与MCMT模型检查器进行的实验证明了我们的方法对具有无界数组的程序的有效性，如果单独应用加速和抽象/细化技术，则会失败。
2013-10-03 cs.LO
A Foundational Theory of Quantitative Abstraction: Adjunctions, Duality, and Logic for Probabilistic Systems
本文提出概率系统定量抽象的理论框架，结合范畴论、余代数和最优传输，通过伴随关系和定量逻辑实现抽象与实现的对偶性，为概率领域中的状态抽象和表示学习提供严格基础。
2026-03-12 cs.AI cs.LG cs.LO
Abstraction-driven Concolic Testing
Concolic测试是一种很有前途的生成大型程序测试集的方法。然而，它受到路径爆炸问题的困扰，并且经常无法找到覆盖程序中难以到达的部分的测试。相比之下，基于反例引导的抽象细化的模型检查器详尽地探索程序，而无法精确地扩展大型程序。在本文中，我们提出了一种新的方法，迭代地结合concolic测试和模型检验，找到一个测试套件的给定的覆盖标准。如果concolic测试不能覆盖某些测试目标，那么模型检查器将改进其程序抽象以证明更多路径不可行，从而减少concolic测试的搜索空间。我们已经实现了我们的方法上的concolic-testing工具CREST和模型检查器Cpaetron。我们评估了我们的工具上收集的程序和一类SvComp基准。在我们的实验中，我们观察到与CREST相比，分支覆盖率在最佳情况下从48%提高到63%，平均从66%提高到71%。
2015-12-29 cs.LO
Refining Trace Abstraction using Abstract Interpretation
众所周知，当抽象精化过程没有导出循环不变量时，软件模型检验中的CEGAR循环就会发散。基于SMT求解器的抽象细化过程被应用于迹线，即，程序的一种限制形式（没有循环）。在本文中，我们提出了一个新的抽象细化过程，旨在尽可能地规避这种限制。我们将抽象解释应用于我们从给定的跟踪中导出的程序。如果程序包含一个循环，我们保证得到一个循环不变量。我们只在抽象解释返回不确定答案的情况下调用SMT求解器。也就是说，这个想法是使用抽象解释和SMT求解器串联。在痕迹提取设置的实验评估表明，这一想法的实际潜力。
2017-02-08 cs.LO
AbPress: Flexing Partial-Order Reduction and Abstraction
偏序约简（POR）和带插值的惰性抽象是两种互补的技术，它们被成功地应用于并行程序的模型检验工具。在这项工作中，我们提出了AbPress -基于抽象的偏序约简与源集-一种算法，融合了最近提出的和强大的动态POR技术的基础上的源集和懒惰的抽象，以获得一个有效的软件模型检查多线程程序。它通过考虑抽象和源集来修剪交织空间。我们放大了AbPress的有效性与一个新的解决方案，总结了访问共享变量的交织的集合。我们已经在一个工具中实现了AbPress，该工具使用惰性抽象来分析并发程序，即，因帕拉我们对所提出的方法的有效性的评价是令人鼓舞的。AbPress与景观中现有的最先进的工具相比毫不逊色。
2014-10-22 cs.LO
Predicate Abstraction via Symbolic Decision Procedures
我们提出了一种新的方法进行谓词抽象的基础上的符号决策过程。直觉上，一个理论的符号决策过程需要理论中的一组谓词，并在谓词集合上的所有子集上符号地执行决策过程。符号决策过程的结果是一个共享表达式（由有向无环图表示），它隐式地表示谓词抽象查询的答案。我们提出了象征性的决定程序的逻辑等式和未解释的功能（EUF）和差异逻辑（DIFF），并表明这些程序运行在伪多项式（而不是指数）的时间。然后，我们提供了一种方法来构造简单的混合理论（包括上述两个理论）的符号决策程序使用扩展的纳尔逊-奥本组合方法。我们提出了初步评估我们的程序谓词抽象基准从设备驱动程序验证SLAM。
2007-04-24 cs.LO cs.PL cs.SC
A General Framework for Sound and Complete Floyd-Hoare Logics
本文将霍尔逻辑抽象为可追踪的对称monoidal范畴，这是系统理论的一个非常一般的框架。我们的抽象是基于一个跟踪monoidal函子从任意跟踪monoidal范畴到范畴的前序和单调关系。我们给出了几个例子，我们的理论如何概括通常的霍尔逻辑（部分正确的，而程序，部分正确的指针程序），并提供了一些案例研究，它可以用来开发新的霍尔逻辑（运行时分析，而程序和流电路）。
2008-07-07 cs.LO cs.OH
Interpretable and Explainable Logical Policies via Neurally Guided Symbolic Abstraction
Technical University of Darmstadt（达姆施塔特工业大学）；National Research Center for Applied Cybersecurity（国家应用网络安全研究中心）；Eindhoven University of Technology（埃因霍温理工大学）；Hessian Center for AI (hessian.AI)（黑森人工智能中心）；German Research Center for AI (DFKI)（德国人工智能研究中心）
本文提出NUDGE框架，通过神经引导的可微逻辑规则搜索，构建兼具可解释性与可说明性的策略，其性能优于纯神经网络且适应不同环境规模。
2023-10-25 cs.AI cs.CL cs.LG
Semantics of templates in a compositional framework for building logics
对逻辑规约语言（如FO（.）和ASP.实现这些抽象的一种技术是模板（有时称为宏）。虽然模板的语义几乎总是通过一个语法重写方案来描述，我们提出了另一种看法模板作为二阶定义。为了扩展FO（.）的现有定义构造，二阶，我们介绍了一个强大的组合框架定义逻辑模块集成的逻辑结构指定为一个语法和语义归纳规则对。我们使用的框架来建立一个逻辑嵌套的二阶定义适合表达模板。我们表明，在适当的限制下，作为宏的模板的视图是语义上正确的，并且添加它们不会扩展基本逻辑的描述复杂性，这与现有方法的结果是一致的。
2015-07-24 cs.LO
Proving linearisability via coarse-grained abstraction
线性化已经成为并发数据结构的标准安全标准，确保具体操作的效果发生在执行某些原子语句之后（通常称为线性化点）。线性化点的识别是一项重要的任务，甚至可以通过执行其他并发操作来线性化操作。本文提出了一种不需要在具体规范中确定线性化点的线性化验证方法。相反，我们表明，具体的程序是一些粗粒度的抽象细化。抽象中的线性化点很容易识别，线性化证明本身也很简单，因为它的原子语句粒度很粗。具体的细粒度程序是粗粒度程序的细化，因此也是可线性化的，因为具体程序的每个行为都是其抽象的可能行为。
2012-12-20 cs.LO cs.SE
Answer-Set-Programming-based Abstractions for Reinforcement Learning
Siemens AG Österreich（西门子奥地利公司）；TU Wien (Vienna University of Technology)（维也纳技术大学）；Jönköping University（约翰·科平大学）
本文提出使用回答集编程（ASP）实现CARCASS框架中的抽象，以解决强化学习中状态空间巨大带来的挑战，并通过积木世界和Minigrid两个领域的案例验证了该方法的有效性。
2026-05-29 cs.AI cs.LO
Full abstraction for probabilistic PCF
我们提出了一个概率版本的PCF，一个著名的简单类型的通用函数语言。类型层次结构基于自然数的单一基类型。即使语言是全局按名称调用的，我们也允许对基础类型参数进行按值调用评估，以便为语言提供合适的算法表达能力。我们描述了一个指称语义的基础上的概率一致性空间，经典的线性逻辑模型在以前的作品。我们证明了一个充分性和一个方程的充分抽象定理，表明在模型中的平等符合自然的概念，观测等价。
2015-11-04 cs.LO
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction
本文研究了实时的【形】系统的安全性验证与综合问题。我们介绍实时的【形】程序，这些程序由可以执行离散和实值变量赋值的指令组成。它们足够通用，可以捕获有趣的时间系统类，如时间自动机，秒表自动机，时间（d）Petri网和混合自动机。我们提出了一种使用轨迹抽象细化的半算法来解决实时的【形】程序的可达性验证问题和参数综合问题。所有提出的算法已经实施，我们已经进行了一系列的实验，比较我们的新方法的性能，以国家的最先进的工具，在经典的可达性，鲁棒性分析和参数合成定时系统。我们表明，我们的新方法提供了解决方案，这些问题是无法解决的，目前最先进的工具。
2020-07-21 cs.FL cs.LO cs.SY
Clausal Abstraction for DQBF (full version)
依赖量化布尔公式（DQBF）是一种允许布尔函数存在量化的逻辑，它允许我们优雅地陈述验证中的综合问题，例如搜索不变量，程序或游戏的获胜区域。本文将量化布尔公式的子句抽象算法（QBF）提升为DQBF。QBF的子句抽象是一种抽象细化算法，它对表示不同量词级别的抽象序列进行操作。对于DQBF，我们需要将这个原则推广到抽象的偏序。需要克服的两个挑战是：（1）子句可能包含具有不可比较依赖关系的文字，我们通过最近提出的称为Fork Extension的证明规则来解决这一问题，以及（2）存在变量可能具有虚假依赖关系，我们通过跟踪执行期间的一致性要求来防止。我们的实现dCAQE解决了显着更多的公式比现有的DQBF算法。
2019-05-07 cs.LO
Model Checking as Program Verification by Abstract Interpretation (Extended Version)
本文提出将模型检验视为程序验证，引入MOKA语言把时序逻辑公式编码为程序，并结合抽象解释与局部完全抽象动态精化分析精度，从而复用更一般的抽象并避免误报。
2025-06-05 cs.LO
The Logic of Logic Programming
本文主张逻辑编程的本质是归纳定义逻辑而非经典逻辑的 Horn 子句子逻辑，并以此解释 Prolog 程序与数学归纳定义的根本相似性，为相关语义问题提供自然解答。
2023-04-26 cs.LO
Towards Abstraction in ASP with an Application on Reasoning about Agent Policies
TU Wien（维也纳工业大学）
ASP程序是解决问题的方便工具，而对于大型问题实例，状态空间的大小可能会令人望而却步。我们认为抽象作为一种手段的过度近似，并介绍了一种方法来自动抽象（可能是非地面）ASP程序，保留其结构，同时减少问题的大小。一个特定的应用程序的情况下，定义声明性的政策反应式代理和推理的问题，我们举例说明。
2018-09-18 cs.AI cs.LO
Logical Characterization of Coherent Uninterpreted Programs
一个未解释的程序（UP）是一个程序，其语义定义在理论上的未解释的功能。这是等价性检查、编译器优化和程序验证中常用的抽象。虽然简单，但该模型足够强大，可以对计数器自动机进行编码，因此不可判定。最近，一类UP程序，称为相干，已被提出并证明是可判定的。我们提供了一个替代的，合乎逻辑的表征，这一结果。具体来说，我们证明了每一个相干程序是一个有限状态系统的双相似。此外，一个连贯程序的归纳不变量可以用一个公式表示，该公式的项的深度至多为1。我们还表明，原来的证明，通过自动机，只适用于一元未解释的功能的程序。虽然这项工作是纯理论的，它提出了一种新颖的抽象，是完整的连贯的程序，但可以合理地用于任意的未解释（和部分解释）的程序。
2021-07-26 cs.FL cs.LO
Abstraction for Zooming-In to Unsolvability Reasons of Grid-Cell Problems
TU Wien（维也纳工业大学）
人类在研究问题时能够抽象出不相关的细节。这对于网格单元的问题尤其明显，因为人类能够忽略网格的某些部分，而专注于对问题重要的关键元素。最近，抽象的概念已被引入到回答集编程（ASP），一个知识表示和推理范式广泛用于解决问题，有可能理解的关键元素的程序中发挥作用，找到一个解决方案。本文件进一步授权抽象处理结构方面，特别是层次抽象的域。我们专注于获得网格上的问题无法解决的原因，并显示了自动实现类似人类的抽象，区分只有网格的相关部分的可能性。对抽象解释的用户研究证实了机器与人类解释中焦点的相似性，并重申了利用抽象来获得机器解释的挑战。
2019-09-11 cs.AI cs.LO
