Ultraproducts in abstract categorical logic
本文在抽象范畴逻辑框架下推广经典模型论中的超积方法，并证明了与具体量化词选择尽可能无关的 Łoś 基本定理。
2024-07-04 cs.LO
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
研究正确性与错误性变换程序逻辑，扩展以处理终止与非终止，证明其为自然关系语义的抽象解释，提供计算化方法设计可靠完备证明系统，并扩展 Hoare 逻辑及设计新前置条件逻辑。
2023-11-23 cs.LO
Nominalistic Logic (Extended Abstract)
名物化逻辑（NL）是对保罗·吉尔摩的内涵类型论（ITT）的一种新的表述，它是一种逻辑演算和一个简洁的名物化公理（N），在某些情况下，它允许谓词的名称作为个体。该逻辑有一个灵活的理解公理，但没有外延性公理和无穷公理，尽管公理N是导出自然数的皮亚诺公设的关键。
2008-12-28 cs.LO
An Epistemic Strategy Logic (Extended Abstract)
本文提出了一个扩展的时间认知逻辑与运营商量化的策略。该语言还提供了一种自然的方式来表示代理人会知道什么，如果他们知道其他代理人正在使用的策略。一些例子来激励框架，并讨论了交替时间认知逻辑的几个变种的关系。并对模型检验逻辑的计算复杂性进行了表征。
2014-04-03 cs.LO
A Logic for Non-Deterministic Parallel Abstract State Machines
我们开发了一个逻辑，使推理的单步的非确定性并行抽象状态机（ASM）。我们的逻辑建立在统一的逻辑介绍了Nanchen和Stärk推理分层（并行）ASM。我们在这方面的主要贡献是在逻辑形式主义中处理非决定论（有界和无界）。此外，我们这样做，而不牺牲逻辑的完整性的语句的单步的非确定性并行ASM，如规则的不变量，规则的一致性条件，或一步一步的规则等价。
2017-05-30 cs.LO
Complete Heyting Algebra Semantics for an Intuitionistic Version of Matching Logic (Extended Abstract)
Research Center for Logic, Optimization and Security (LOS), University of Bucharest（布加勒斯特大学逻辑、优化与安全研究中心）；Institute for Logic and Data Science, Bucharest（布加勒斯特逻辑与数据科学研究所）
该研究推进直觉主义版本可应用匹配逻辑的构建，提出基于完备Heyting代数的语义框架，还设计了对应的证明系统并验证了其可靠性。
2026-09-28 cs.LO
Bridge and Bound: A Logic-Based Framework for Abstracting (Extended Report)
University of Warsaw（华沙大学）
本文提出了一种基于逻辑的抽象框架，通过引入充分条件和分层抽象，实现复杂系统的分层简化。
2026-01-03 cs.LO
Completeness for a First-order Abstract Separation Logic
分离逻辑（SL）断言语言的定理证明的现有工作要么集中在抽象语义上，这在大多数程序验证应用中是不容易获得的，要么集中在具体模型上，这是不可能的。具体SL中的一个重要元素是指向谓词，它表示单例堆。带有指向谓词的SL已被证明是不可递归的。在本文中，我们开发了一个一阶SL，称为FOASL，与抽象版本的指向谓词。我们证明了FOASL是健全的和完整的抽象语义，其中标准SL语义是一个实例。我们还表明，一些推理原则，涉及点到谓词可以近似为FOASL理论，从而使我们的逻辑用于推理具体的程序验证问题。我们给出了一些例子理论，是健全的分离逻辑从文献中的不同变体，包括那些与雷诺兹的语义不兼容。在实验中，我们展示了我们的FOASL为基础的定理证明，这是能够处理大量的分离逻辑与堆语义，以及非标准的语义片段。
2016-08-24 cs.LO
Paths-based criteria and application to linear logic subsystems characterizing polynomial time
线性逻辑的几种变体已经被提出来描述证明-程序对应中的复杂性类。轻线性逻辑（LLL）确保了约简时间的多项式界限，并且以这种方式表征多项式时间（Ptime）。本文研究了线性逻辑证明网的复杂性，提出了基于上下文语义的三个语义准则：分层、依赖控制和嵌套。分层本身需要一个基本的时间界限，这三个标准一起需要一个多项式时间界限。这些准则可以用来证明线性逻辑的几个现有变体的复杂性可靠性。我们定义了线性逻辑的一个可判定语法子系统：SDNLL。我们证明了SDNLL的证明网满足这三个标准，这意味着SDNLL是健全的Ptime。将线性逻辑中表征多项式时间的几个子系统（LLL，mL^4，MS的极大系统）嵌入SDNLL中，证明了SDNLL的Ptime完备性.
2017-01-05 cs.CC cs.LO
Dual Logic Concepts based on Mathematical Morphology in Stratified Institutions: Applications to Spatial Reasoning
在不同类型的逻辑中，几个逻辑运算符被定义为对偶对。这种对偶算子对也出现在其他代数理论中，如数学形态学。基于这一观察，本文提出了定义，在抽象层次的制度，一对抽象的对偶和逻辑运算符作为形态侵蚀和膨胀。标准的量词和模态，然后从这两个抽象的逻辑运算符。这些运营商都研究了一套状态和一套模型。为了应付缺乏明确的一套制度的国家，建议的抽象逻辑对偶算子定义在机构的扩展，分层机构，考虑到开放的句子，其中的满意度是参数化的状态集的概念。还提供了一个提示的空间推理的建议框架的潜在利益。
2017-10-16 cs.LO
Topological representation of intuitionistic and distributive abstract logics
我们继续我们早期论文的工作（Lewitzka和Brunner：Minimally generated abstract logics，Logica Universalis 3（2），2009），其中研究了抽象逻辑，特别是直觉抽象逻辑。抽象逻辑可以直接自然地拓扑化。这有利于拓扑研究类的具体逻辑时，他们给出了抽象的形式。此外，这种直接的拓扑方法避免了通常用于表示逻辑的复杂的代数和格论机器。基于这一观点，本文定义了以稳定逻辑映射为态射的直觉抽象逻辑范畴和以谱映射为态射的蕴涵谱空间范畴。我们证明了这些范畴的等价性，并得出结论，分配抽象逻辑和分配清醒空间的更大的范畴是等价的。
2015-08-18 cs.LO math.LO
Process Behaviour: Formulae vs. Tests (Extended Abstract)
流程行为通常根据它们所满足的测试或它们所享有的逻辑属性来定义。在这里，我们比较这两种方法，使用扩展测试的风格DeNicola，轩尼诗，和递归版本的属性逻辑HML。我们首先检查可以通过测试捕获的属性逻辑的子集。然后，我们表明，这些子集的属性逻辑捕捉准确的测试的力量。
2010-11-30 cs.LO
Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax
众所周知，在逻辑框架中结合高阶抽象语法和（共）归纳是有问题的。以前的工作描述了一个名为混合动力的工具，在伊莎贝尔HOL，其目的是解决许多这些困难的实施。它允许使用高阶抽象语法来表示对象逻辑，并使用策略性定理证明和（共）归纳原理进行推理。在本文中，我们描述了如何使用它在一个多层次的推理方式，类似的精神，其他元逻辑，如BLOMF。通过明确引用证明在一个中间层称为规范逻辑，我们解决了推理的问题（共）归纳存在的非分层假设的判断，这使得非常优雅和简洁的规范对象逻辑推理规则。
2010-05-26 cs.LO
Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
抽象解释、霍尔逻辑和不正确（或反向霍尔）逻辑是静态分析计算机程序的强大技术。所有这些都已成功地扩展到量子设置，但在很大程度上是并行开发的。在本文中，我们研究这些技术之间的关系，在验证量子while程序的背景下，其中的抽象域和一组断言的量子状态是结构良好的。特别地，我们证明了任何完全的量子抽象解释都可以导出一个量子霍尔逻辑和一个量子不正确逻辑，这两个逻辑都是合理的和相对完备的。与文献中提出的逻辑不同，诱导逻辑系统是以向前的方式，使它们在某些应用中更有用。相反，任何健全的和相对完整的量子霍尔逻辑或量子不正确逻辑都导出一个完整的量子抽象解释。作为应用，我们证明了当局部子空间元组作为断言时，不存在任何可靠的、相对完备的量子霍尔逻辑或不正确逻辑.
2022-06-28 cs.LO quant-ph
A Program Logic for Abstract (Hyper)Properties
Department of Mathematics, University of Padua（帕多瓦大学数学系）；Department of Computer Science, University of Pisa（比萨大学计算机系）
本文提出APPL逻辑，统一了Hoare逻辑、错误逻辑和超Hoare逻辑变体，提供抽象程序逻辑的理论基础，支持多种抽象域。
2026-04-21 cs.LO cs.PL
A Complete Logic for Database Abstract State Machines
在数据库理论中，术语$\textit{database transformation}$用于指可计算查询和更新的统一处理。最近，有研究表明，非确定性数据库转换可以被ASM的一种变体准确捕获，即所谓的数据库抽象状态机（DB-ASM）。在这篇文章中，我们提出了一个DB-ASM的逻辑，扩展了Nanchen和Stärk的逻辑。特别是，我们开发了一个严格的证明系统的逻辑DB-ASMs，这是被证明是健全和完整的。扩展处理的最困难的挑战是一个适当的形式化捕获数据库转换的非确定性及其所有相关功能，如一致性，更新集或与DB-ASM规则相关的多集。由于数据库转换的状态的数据库部分是有限结构，并且DB-ASM通过仅允许状态的数据库部分上的量词来限制，因此我们通过将更新集显式地带入逻辑中来解决这个问题，即通过使用额外的模态运算符$[X]$，其中$X$被解释为由DB-ASM规则生成的更新集$Δ$。DB-ASM逻辑提供了一个强大的验证工具来研究数据库转换的属性。
2017-05-30 cs.LO
Stratifying Reinforcement Learning with Signal Temporal Logic
University at Albany, State University of New York（纽约州立大学奥尔巴尼分校）；Lockheed Martin, Advanced Technology Labs（洛克希德·马丁公司先进技术实验室）
本文提出基于分层理论的信号时间逻辑语义，揭示分层理论与STL的对应关系，为深度强化学习嵌入空间结构分析提供新框架，并推动新型计算技术发展。
2026-04-06 cs.LG cs.LO cs.SY
The Attack as Strong Negation, Part I
在经典逻辑中加入强否定$N$，将论证中“$x$攻击$y$“的攻击关系解释为$(x\to Ny)$。我们写了一个相应的对象级别（仅使用$N$）的经典理论，为每个论证网络，并表明，该理论的经典模型完全对应于完整的扩展的论证网络。我们通过例子展示了这种方法如何简化抽象论证网络的研究。我们比较与其他翻译的抽象论证网络到逻辑，如经典谓词逻辑或模态逻辑，或逻辑编程，我们也比较与抽象辩证框架。
2015-06-10 cs.LO
String Diagrams for Regular Logic (Extended Abstract)
正则逻辑可以被看作是正则范畴的内部语言，但逻辑本身一般不被给予范畴化的处理。本文用集合T上的自由正则范畴FRG（T）来理解正则逻辑的语法和证明规则。从这个观点来看，正则理论是从一个合适的2-范畴的上下文--FRG（T）中的2-范畴的关系--到偏序集的2-范畴的某些monoidal 2-函子。这样的函子给每个上下文中的公式集赋值，并按蕴涵排序。我们把这样一个2-函子称为一个正则演算，因为它自然地产生了一个图形化的弦图演算的精神Joyal和街。我们将证明，每一个自然范畴都有一个相关联的正则演算，反过来，从每一个正则演算，我们可以构造一个正则范畴。
2020-09-15 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
An Abstract Algebraic Logic View on Judgment Aggregation
在本文中，我们提出了抽象代数逻辑（AAL）作为一般的逻辑框架的判断聚合。我们的主要贡献是一个广义的赫茨伯格的代数方法来表征的结果在判断聚合和命题态度聚合，表征某些Arrovian类聚合布尔代数和MV-代数同态，分别。本文的刻画结果适用于任意自延逻辑的公式议程。这个概念来自AAL，包含了大量的逻辑，其中经典逻辑、直觉逻辑、模态逻辑、多值逻辑和关联逻辑都是特例。AAL的一般理论将一类唯一的代数$\Alg\Sm$规范地关联到每个自扩张逻辑$\Sm$。我们表明，对于任何自扩展逻辑$\Sm$，使$\Alg\Sm$是封闭的直积下，任何代数$\Alg\Sm$可以采取的真值集上的聚合问题可以制定。通过这种方式，在经典，直觉，模态，多值和相关逻辑形式化的议程上的判断聚合可以被统一地捕获为特例。这为系统研究由复杂公式组成的广泛的“现实议程”铺平了道路，这些公式的命题连接词的解释方式偏离了它们的经典解释。正如迪特里希所观察到的，这一点特别有趣，因为逻辑连接词的非经典（虚拟）解释可以提供一种逃避不可能结果的策略。
2016-03-27 cs.LO
An Inductive Construction for Many-Valued Coalgebraic Modal Logic
在本文中，我们提出了一个抽象的框架，多值模态逻辑的原子命题和模态算子的解释为谓词提升余代数上的一个endofunctor的集合范畴。它将Pattinson的共形模态逻辑分层方法推广到多值情形。与规范模型构造和过滤的标准技术相比，该方法采用归纳原理来证明逻辑的可靠性、完备性和有限模型性质。因此，我们可以解除对先前方法的限制~ \cite{Lin2022}，该方法要求底层语言必须具有内在化元级真值赋值操作的表达能力。
2022-10-24 cs.LO
A Formalisation of Abstract Argumentation in Higher-Order Logic
University of Luxembourg（卢森堡大学）
我们提出了一种方法，表示抽象的论证框架的基础上编码成经典的高阶逻辑。这为使用交互式和自动推理工具对抽象论证框架进行计算机辅助评估提供了一个统一的框架。这使得元理论属性的形式化分析和验证，以及灵活生成的扩展和标记方面的知名的论证语义。
2021-10-18 cs.AI cs.LO
Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic (Extended Abstract)
我们调查的时间，知识和概率的模型检查逻辑的可判定性，相对于两个认知语义：时钟和同步完美召回部分观察离散时间马尔可夫链的语义。可判定性的结果是已知的某些限制逻辑关于这些语义，受到各种各样的限制，要么是无法解释的，或涉及一个长期未解决的数学问题。我们表明，温和的推广已知的可判定的情况下，足以使模型检验问题明确不可判定。特别地，对于同步完美召回，从有限到达的时态算子到无限到达的算子的推广使得模型检验不可判定。时钟语义的情况下是密切相关的时间和概率的一元二阶逻辑，已知是可判定的，除了一组测量零。我们表明，这种逻辑的两个不同的扩展，使模型检验不可判定。其中之一涉及概率项的多项式组合，另一个涉及到概率算子范围内的一元二阶量化。这些结果解释了以前工作中的一些限制。
2016-06-24 cs.LO
Abstract argumentation and answer set programming: two faces of Nelson's logic
University of Nebraska Omaha（内布拉斯加大学奥马哈分校）；IRIT（图卢兹计算机科学研究所）；Université de Toulouse（图卢兹大学）；CNRS（法国国家科学研究中心）
在这项工作中，我们表明，逻辑编程和抽象的论证框架可以解释纳尔逊的建设性逻辑N4。在这种逻辑中，我们通过形式化两个原则来做到这一点，我们称之为非矛盾推理和加强的封闭世界假设：第一个原则指出，任何信念都不能基于矛盾的证据，而后者则迫使未知和矛盾的证据都被视为错误。使用这些原则，逻辑程序设计和抽象论证框架都以模块化的方式并使用对象语言转换为构造性逻辑。逻辑程序蕴涵和抽象论证支持在翻译中遵循不矛盾推理原则成为新的蕴涵连接词。然后，攻击通过将这个新的蕴涵与强否定相结合来表示。逻辑程序设计理论与实践（TPLP）
2022-03-27 cs.AI cs.LO
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
TWAM: A Certifying Abstract Machine for Logic Programs
类型保持（或类型化）编译使用类型化派生来证明编译的正确性。我们为Prolog的简单类型方言设计并实现了一个类型保留编译器，我们称之为T-Prolog。我们的方法的关键是一个新的认证抽象机，我们称之为类型沃伦抽象机（TWAM）。TWAM有一个足够强的依赖类型系统来指定逻辑框架LF中的逻辑程序的语义。我们提出了一个合理性元定理，它构成了部分正确性保证：良好类型的程序实现的逻辑程序指定的类型。这个元定理证明了我们的设计和实现的证明编译器从T-Prolog到TWAM。
2018-01-01 cs.LO cs.PL
Deriving Abstract Semantics for Forward Analysis of Normal Logic Programs
虽然否定作为失败是通过内建谓词来处理的，但在文献中还没有正式地讨论{ \em normal}逻辑程序的前向抽象解释问题！在Prolog中实现的方式。本文提出了一个解决这个问题的方法，推导出两个通用的不动点抽象语义$F^b and $ F^ \diamond { \em正常}逻辑程序的前向抽象解释。$F^b$用于推断程序图中边的数据描述，其中边表示执行控制从其源程序点转移到其目的程序点的可能性。$F^\diamond$源自$F^b$，用于推断文本程序点的数据描述。
1998-11-06 cs.LO cs.PL
On some many-valued abstract logics and their Epsilon-T-style extensions
具有经典否定和命题或命题自指手段的逻辑系统在某种程度上涉及悖论陈述，如说谎者。然而，如果我们用一个适当的非经典否定（如次协调否定）来代替经典否定，悖论就消失了（如果说谎者既是真的又是假的，就不会出现悖论）。我们考虑一个非弗雷格逻辑，它是最初由（Straeter 1992）引入的Epsilon-T-Logic的修订和扩展版本（Lewitzka 2012），作为一个具有全真谓词和命题量词的逻辑。自指是通过公式之间的方程来实现的，这些公式在命题的模型论域上进行解释。paragrical语句，如说谎者，只能断言的不可满足的方程，并不与命题。本文将Epsilon-T-Logic推广到与Dunn/Belnap逻辑B_4有关的四值逻辑。我们还分别定义了与Kleene的逻辑K_3和Priest的Partial逻辑P_3有关的三值版本。在这个多值的环境中，模型可能包含说谎者和其他被更严格的经典语义学排除的“悖论”命题。我们引入这些多值非Fregean逻辑作为抽象参数逻辑的扩展，使参数逻辑和扩展是相同的逻辑类型。为此目的，我们定义并研究了B_4、K_3和P_3型抽象逻辑。本文用语义学方法证明了B_4型抽象逻辑的结果关系的紧性，给出了作为极小生成逻辑的表示，并与Font（1997）的方法建立了联系。最后，我们提出了一个完整的ε-T型扩展的经典抽象逻辑简化结构最初开发的（斯特拉特1992年，蔡茨2000年…
2012-09-24 cs.LO math.LO
On the Relative Expressiveness of Argumentation Frameworks, Normal Logic Programs and Abstract Dialectical Frameworks
Computer Science Institute Leipzig University（莱比锡大学计算机科学研究所）
分析了抽象论证框架、规范逻辑程序和抽象辩证框架的二值语义的表达性。通过表达性，我们指的是在给定的命题签名上仅使用来自该签名的原子来编码所需的二值解释集合的能力。虽然所有这些语言的二值模型存在问题的计算复杂性是（几乎）相同的，我们表明，语言形成一个整洁的层次结构，就其表现力。
2014-05-05 cs.AI cs.LO
An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic
University of Luxembourg, Department of Computer Science（卢森堡大学计算机科学系）；Universität Greifswald, Institut für Mathematik und Informatik（格赖夫斯瓦尔德大学数学与信息学研究所）
本文提出将抽象辩证框架及其语义编码到经典高阶逻辑的方法，利用Isabelle/HOL证明助手正式编码和证明重要属性及语义关系，实现计算机辅助分析。
2023-12-08 cs.AI cs.LO
An Abstract Look at Awareness Models and Their Dynamics
本文以觉知模态逻辑为基础，建立其与抽象论证、justification logics、knowing-what 认知逻辑和道义逻辑的联系，刻画觉知集合的若干性质并给出典范公式公理化，进而通过事件模型研究动态更新，证明闭包定理并借助归约公理公理化相应动态逻辑。
2023-07-11 cs.LO
Logic and Topology for Knowledge, Knowability, and Belief - Extended Abstract
在最近的工作中，Stalnaker提出了一个逻辑框架，在这个框架中，信仰被实现为知识的弱化形式。基于Stalnaker的核心见解，并使用Bjorndahl和Baltag等人开发的框架，我们采用拓扑工具，以完善，我们认为，改善这一分析。拓扑子集空间的结构允许什么是已知的和（粗略地说）什么是可知的自然区别，我们认为，Stalnaker的系统的基本公理依赖于直观的这两个概念。更确切地说，我们认为，Stalnaker提出的原则的可解释性相关的知识和信仰依赖于一个微妙的模棱两可之间的“证据在手”的知识概念和一个较弱的“证据在那里”的概念可以被称为。我们的分析导致三峰逻辑的知识，可知性，并解释在拓扑子集空间中的信念是可定义的知识和可知性的信念。我们提供了一个健全的和完整的公理化的逻辑，以及它的单峰信念片段。然后，我们考虑较弱的逻辑，保持适当的翻译Stalnaker的公设，但不允许任何减少的信念。我们提出了新的拓扑语义，这些不可约的信念的概念，推广我们以前的语义，并提供相应的逻辑健全和完整的公理化。
2017-07-27 cs.LO
Logic programs with monotone abstract constraint atoms
本文介绍并研究了子句由单调约束原子构成的逻辑程序。我们表明，一步证明算子的操作概念推广到单调约束原子的程序，但推广涉及非确定性。我们的主要结果表明，我们的形式化是一个共同的推广（1）正常的逻辑编程与其语义的模型，支持的模型和稳定的模型，（2）逻辑程序与重量原子（lparse程序）的语义的稳定模型，定义的Niemela，Simons和Soininen，（3）析取逻辑编程与可能的模型语义的Sakama和井上。
2006-08-25 cs.AI cs.LO
Temporal logic with predicate abstraction
考虑了一个没有量词但具有谓词抽象机制和等式的谓词线性时态逻辑LTL_{λ,=}。LTL_{λ,=}的模型可以很自然地看作是在某些（可能是无限的）域的元素上移动的卵石（柔性常数）系统。这允许使用LTL_{λ,=}的规范的动态系统使用一些资源，如使用内存位置，移动代理占用一些网站等的进程。另一方面，我们表明，LTL_{λ,=}是不是递归axiomatizable，因此，LTL_{λ,=}规范的全自动验证是不，一般来说，可能的。
2004-10-27 cs.CL cs.LO
Bialgebraic Semantics for Logic Programming
双代数提供了一个抽象框架，包含不同类型的计算模型的语义。在本文中，我们提出了一个双代数方法的语义逻辑程序设计。我们的方法是研究逻辑程序作为反应系统，并利用抽象技术开发的设置。首先，我们使用饱和度模型的操作语义的逻辑程序作为余代数上的预层。然后，利用预层上的双代数，明确了其代数结构。由此产生的语义原来是组合方面的连接和长期替代。此外，它还编码了一个并行计算模型，其可靠性由不同线程之间的内置同步概念保证。
2015-03-27 cs.LO
Computing Abstract Distances in Logic Programs
抽象解释是执行逻辑程序的静态分析的一种成熟的技术。然而，选择提供最佳精度-成本权衡的抽象域、加宽、固定点等仍然是一个悬而未决的问题。这在很大程度上是因为在测量和比较不同分析的精度方面存在挑战。我们提出了一种新的方法来测量这样的精度，定义在抽象域的距离，并将它们扩展到一个给定的程序的整个分析之间的距离，从而允许在不同的分析精度进行比较。我们调查和扩展现有的建议，在格或抽象域的距离和度量，我们提出了一些常见的域中使用的逻辑程序分析的度量，以及扩展这些度量的空间，整个程序分析。我们在CiaoPP框架内实现这些指标，并将它们应用于衡量基准和现实程序上不同分析的精度。
2019-07-30 cs.LO cs.PL
Linear Logic by Levels and Bounded Time Complexity
通过证明-程序对应，给出了线性逻辑中初等和确定性多项式时间计算的一个新的刻画。吉拉德的开创性成果，关于初等和轻型线性逻辑，实现了这一特点，强制执行分层原则的证明，使用的概念，深度的证明网。在这里，我们提出了一种更一般的分层形式，基于通过索引在证明网中诱导水平，这使我们能够扩展Girard的系统，同时保持相同的复杂性。特别是，事实证明，吉拉德的系统可以恢复，迫使深度和水平相一致。深度层次灵活性较高的一个后果是没有处理段落模式的框。我们利用这一事实，提出了一个变种，我们的polytime系统中的段落模态只允许原子，从而可以作为一个基础，为开发的pendida演算类型分配系统，更有效的打字算法比现有的。
2009-07-26 cs.CC cs.LO
Binary Non-Termination in Term Rewriting and Logic Programming
该研究提出一种新的句法准则，可在包含简化项重写与逻辑编程的抽象场景中实现非终止性的自动检测。
2023-07-21 cs.LO
Modular Labelled Sequent Calculi for Abstract Separation Logics
抽象分离逻辑是霍尔逻辑的一系列扩展，用于推理操纵诸如存储器位置之类的资源的程序。这些逻辑是“抽象的”，因为它们独立于任何特定的具体资源模型。他们的断言语言，称为命题抽象分离逻辑（PASL），以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。特别地，这些逻辑包含连接词$*$和$-\!*$，分别表示资源的组成和扩展。这种额外的表达能力是有代价的，因为所产生的逻辑都是不可判定的。鉴于其广泛的适用性，甚至半决策程序，这些逻辑是可取的。虽然在文献中讨论了几个PASL和它们与BBI的关系，但这些逻辑的证明理论和自动推理是本文的会议版本解决的开放问题，该版本使用无割标记演算为各种PASL开发了模块化证明理论。本文非平凡地改进了以前的工作，给出了一个一般框架的演算上的任何新的公理在逻辑满足一定的形式对应的推理规则在我们的框架，和完整性证明一般考虑这样的公理。我们的基础演算处理Calcagno等人。的原始逻辑的分离代数，增加了健全的规则，部分确定性和cancellativity，同时保持削减消除。然后，我们证明了分离逻辑中的许多重要性质，如不可分单元、不相交性、可分裂性和交叉分裂性，都可以用我们的一般公理形式表示。因此，我们的框架免费提供了这些属性的推理规则和完整性。最后，我们展示了我们的演算如何减少到具有全局标签替换的演算，从而实现更高效的实现。
2018-03-26 cs.LO cs.PL
Together We Know How to Achieve: An Epistemic Logic of Know-How (Extended Abstract)
Vassar College（瓦萨学院）；Lafayette College（拉斐特学院）
达成目标的联盟战略的存在并不一定意味着联盟有足够的信息来知道如何遵循该战略。这也不意味着联合政府知道这种战略的存在。本文研究了分布式知识、联盟策略和联盟“专有技术”策略之间的相互作用。主要的技术成果是一个健全和完整的三模态逻辑系统，描述了这种相互作用的性质。
2017-07-27 cs.AI cs.LO
Common Knowledge of Abstract Groups
认知逻辑通常讨论个体代理或明确列出的代理组的知识。然而，人们往往希望表达由某一特定属性所指定的代理人群体的知识，如“这是经济学家之间的常识”。我们介绍这样一个逻辑的共同知识，我们的术语抽象组认知逻辑（AGEL）。也就是说，AGEL的特点是一个共同的知识运营商组的代理商给出的概念，在一个单独的代理逻辑，我们保持通用，与一个可能的代理逻辑是ALC。我们发现，AGEL是EXPTIME-完全的，与标准的组认知逻辑的减少建立的下限，并通过一个满足性保持嵌入到完整的$μ$ -演算的上限。进一步的主要结果包括有限的模型属性（不享有充分的$μ$ -演算）和一个完整的公理化。
2022-11-29 cs.AI cs.LO
Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
本文首次探索子结构逻辑的证明论语义，提出直觉主义乘法线性逻辑（IMLL）的基础扩展语义，其中逻辑常量定义均采用消去规则形式，并证明了其可靠性与完备性。
2024-11-12 cs.LO math.LO
The Lindstrom's Characterizability of Abstract Logic Systems for Analytic Structures Based on Measures
1969年，Per Lindstrom证明了他著名的刻画一阶逻辑的定理，并为离散结构的形式理论的一阶可定义性建立了标准。K. J. Barwise，S. Shelah，J.Vaananen和其他人将Lindstrom的特征化程序扩展到无穷逻辑系统的类别，包括M。Dzamonja和J.Vaananen关于Karp的链逻辑的一个新的结果，它满足内插、良序不可定义性，并且在具有这些性质的逻辑系统类中是极大的。链式逻辑的新颖之处在于它对可满足性的新定义。在我们的论文中，我们给出了一个框架Lindstrom的类型特征化的谓词逻辑系统的语义解释模型与对象的基础上的措施（分析结构）。特别地，Hajek积分逻辑被重新定义为具有一种新的Hajek可满足性的抽象逻辑，并构成了描述具有勒贝格积分的分析结构并满足紧性、初等链条件和弱否定的逻辑系统类中的极大逻辑。
2023-02-26 cs.CL cs.LO math.LO
Invariant stream generators using automatic abstract transformers based on a decidable logic
在模型或源代码上使用形式化分析工具通常需要关于所研究系统的辅助不变量的可用性。抽象解释是目前发现有用的不变量，特别是数值不变量的最佳方法之一。然而，它的应用受到两个正交问题的限制：（i）开发抽象解释通常是不平凡的;系统的每个传递函数必须在抽象级别上表示，这取决于所使用的抽象域;（ii）对于精确但昂贵的抽象域，由抽象解释器计算的信息只能在到达后定点时使用;这对于非常大的系统分析可能需要很长时间，或者延迟加宽以提高精度。本文提出了一种新的，完全自动的，方法来建立抽象解释器。它的一个很好的特点是，它产生的解释器可以提供声音的不变量的分析系统到达后固定点计算结束之前，所以作为在飞行不变的发电机。
2012-05-16 cs.LO cs.SE
An abstract fixed-point theorem for Horn formula equations
针对计算机科学多应用中重要的Horn公式方程，本文在带最小不动点算子的一阶逻辑中证明了适用于抽象语义的抽象不动点定理，并阐述其在程序验证逻辑基础等计算逻辑领域的推论。
2025-11-11 cs.LO math.LO
Local Completeness Logic on Kleene Algebra with Tests
局部完备性逻辑（LCL）是一种用来证明程序规格说明正确性和不正确性的程序逻辑。LCL是一种抽象逻辑，由抽象域参数化，允许组合程序行为的过近似和欠近似。事实证明，实例化为简单的单例抽象的LCL归结为O 'Hearn不正确逻辑，它允许我们证明程序错误的存在。最近已经证明，适当的扩展Kleene代数与测试（KAT）允许表示O 'Hearn不正确性和Hoare正确性程序逻辑在同一个等式框架内。在这项工作中，我们推广了这一结果，展示了如何KAT扩展无论是与模态钻石运营商或顶部元素能够代表本地完整性逻辑LCL。这是通过研究这些扩展的KAT如何可以被赋予一个抽象的域，以定义正确性/不正确性LCL三元组的有效性，并表明LCL证明系统是逻辑上健全的，在一些假设下，完整的。
2022-08-25 cs.LO cs.PL
Reasoning with Higher-Order Abstract Syntax in a Logical Framework
基于具有更高类型量化的直觉或线性逻辑的逻辑框架已成功地用于对程序设计语言和推理系统领域中的许多重要判断给出高级、模块化和形式化的规范。给定这样的规范，考虑证明框架中指定系统的属性是很自然的：例如，给定函数式程序设计语言的求值规范，证明该语言是确定性的或求值保留类型。开发这种推理框架的一个挑战是高阶抽象语法（HOAS），一种优雅的和声明性的对象级抽象和替换处理，很难在涉及归纳的证明中处理。在本文中，我们提出了一个元逻辑，可用于推理使用HOAS编码的判断，这个元逻辑是一个简单的直觉主义逻辑，承认高阶量化简单类型的非线性项（HOAS的关键成分），以及归纳和定义的概念的扩展。我们通过考虑直觉和线性逻辑的编码，探讨了HOAS编码的形式元理论分析的困难，并正式推导出这些逻辑的重要子集的割的容许性。然后，我们提出了一种方法，以避免高阶抽象语法的好处和分析所产生的编码的能力之间的明显的权衡。我们通过涉及简单函数式和命令式程序设计语言PCF和PCF：=的示例来说明这种方法。我们正式推导出这样的属性，作为唯一性的类型，主题减少，确定性的评价，和等价的过渡语义和自然语义表示的评价。
2001-01-15 cs.LO cs.PL
Making Abstract Domains Condensing
在本文中，我们表明，可逆分析的逻辑语言的抽象解释可以进行不损失的精度，系统地细化抽象域。其思想是将语义结构包含到抽象域中，以这种方式，精炼的抽象域变得足够丰富，以允许近似的自底向上和自顶向下语义一致。这些域被称为压缩抽象域。实质上，如果目标驱动和目标独立分析一致，则抽象域是浓缩的，即在目标独立分析中近似查询不会引起精度损失。我们证明了凝聚是一个抽象的域属性，并使一个抽象域凝聚的问题归结为问题，使域完整的统一。在一般的抽象解释设置，我们表明，当具体的域和操作引起quantales，即模型的命题线性逻辑，对象在一个完整的精炼抽象域可以明确的特征在于线性逻辑为基础的配方。这是用于逻辑程序分析的抽象域的情况，近似计算的答案替换，其中统一在幂等替换的Quantale中扮演乘法合取的角色。因此，凝聚抽象域可以通过最小限度地扩展任何，通常非凝聚域，由一个简单的域细化算子系统地得出。
2002-04-09 cs.LO cs.PL
On the Semantics of Abstract Argumentation Frameworks: A Logic Programming Approach
University of Calabria（卡拉布里亚大学）
最近，人们对Dung的抽象论证框架（AF）的扩展框架越来越感兴趣。流行的扩展包括双极AF和具有递归攻击和必要支持的AF。虽然AF语义和部分稳定模型（PSM）的逻辑程序之间的关系已被深入研究，这是不是更一般的框架扩展AF的情况下。在本文中，我们探讨基于AF的框架和PSM之间的关系。我们表明，每一个AF为基础的框架$Δ$可以被翻译成一个逻辑程序$P_Δ$，使扩展规定的不同语义的$Δ$符合子集的PSM的$P_Δ$。我们提供了一个逻辑编程方法，其特点是，在一个优雅和统一的方式，几个AF为基础的框架的语义。这一结果还允许定义新的AF为基础的框架，如AF与递归攻击和递归演绎支持的语义。《逻辑程序设计理论与实践》（Theory and Practice of Logic Programming）
2020-08-06 cs.AI cs.LO
Multirole Logic (Extended Abstract)
我们确定多角色逻辑作为一种新形式的逻辑，其中合取/析取被解释为一个超滤的幂集的一些基本的设置（角色）和概念的否定是广义的自同态在这个基本的设置。我们形式化的多角色逻辑（MRL）和线性多角色逻辑（LMRL）的经典逻辑（CL）和经典线性逻辑（CLL）的自然推广，分别，也提出了一个过滤器为基础的解释直觉主义的多角色逻辑。在为MRL和LMRL建立的各种元性质中，我们得到了一个称为多方割消元的性质，它指出每个包含一个或多个序列的割（作为包含恰好两个序列的（二元）割的推广）都可以被消元，从而推广了Gentzen关于割消元的著名结果.
2017-03-19 cs.DC cs.LO cs.PL
Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
本文提出一种扩展一阶逻辑，以 Hoare 三元组风格对抽象状态进行推理，并通过可实现性解释将证明提取为混合函数式/命令式程序，同时给出基于状态单子的语义解释及 Heyting 算术单子扩展。
2024-01-25 cs.LO math.LO
Axiomatizations and Computability of Weighted Monadic Second-Order Logic
加权一元二阶逻辑是一元二阶逻辑的加权扩展，它精确地捕捉了加权自动机的行为。它的语义是相对于半环参数化的，加权公式输出的值在半环上进行评估。Gastin和Monmege（2018）给出了加权一元二阶逻辑的抽象语义，以给出逻辑与加权自动机的等价性的更一般和模块化的证明。我们专注于抽象的语义的逻辑，我们给一个完整的公理化的完整的逻辑和一个片段没有一般的总和，从而给一个更细粒度的理解的逻辑。我们讨论了如何常见的决策问题的逻辑语言可以适应加权设置，并表明，其中许多是可判定的，虽然他们继承了坏的复杂性从底层的第一和第二阶逻辑。然而，我们表明，加权适应的可满足性是不可判定的逻辑时，使用的抽象解释。
2021-04-29 cs.FL cs.LO
Abstract Reasoning via Logic-guided Generation
Korea Advanced Institute of Science and Technology (KAIST)（韩国科学技术院）；Mohamed bin Zayed University of Artificial Intelligence (MBZUAI)（穆罕默德·本·扎耶德人工智能大学）
抽象推理，即，从给定的观察中推断复杂的模式，是人工智能的核心组成部分。虽然人类通过消除错误的候选人或首先构建答案来找到答案，但基于深度神经网络（DNN）的方法专注于前一种判别方法。本文旨在为后一种方法设计一个框架，并弥合人工智能和人类智能之间的差距。为此，我们提出了逻辑引导生成（Logic-guided generation，LoGe），这是一种新的生成式DNN框架，可以将抽象推理减少为命题逻辑中的优化问题。LoGe由三个步骤组成：从图像中提取命题变量，用逻辑层推理答案变量，并从变量重构答案图像。我们证明，在RAVEN基准测试下，LoGe优于黑盒DNN框架的生成抽象推理，即，基于从观察捕获各种属性的正确规则来重构答案。
2021-08-11 cs.AI cs.CV cs.LG
