Polynomial Interpretations for Higher-Order Rewriting
弱单调代数的终止方法，在HRS形式主义中被定义为高阶重写，提供了很大的力量，但近年来很少使用。我们适应和扩展这种方法的替代形式主义的代数功能系统，其中简单类型的代数演算与代数约简相结合。使用这一理论，我们定义高阶多项式的解释，并显示如何实现这种技术的挑战可以解决。终止工具WANDA中提供了完整的实现。
2012-03-26 cs.LO
Generic Encodings of Constructor Rewriting Systems
Université de Lorraine（洛林大学）；LORIA（洛林计算机科学及其应用实验室）
重写是一种广泛应用于计算机科学和数理逻辑的形式主义。经典的形式主义已经扩展，在函数式语言的上下文中，与规则的顺序，并在基于重写的语言的上下文中，与模式的否定。本文提出了一种简洁明了的模式差异计算算法，该算法可用于将具有否定和顺序的构造函数项重写系统的通用编码定义为经典项重写系统。作为一个直接的后果，建立的方法用于长期重写系统可以应用到分析的扩展系统的属性。该方法也可以被看作是一个通用的编译器，其目标是提供基本模式匹配原语的任何语言。形式主义也提供了一个新的方法来决定一组模式是否包含一个给定的模式，从而检查无用模式的存在或模式的完整性。
2019-06-11 cs.CL cs.LO cs.PL
Rewriting Logic Semantics of a Plan Execution Language
计划执行交换语言（英语：Plan Execution Interchange Language，缩写：PLEXIL）是一种由NASA开发的同步语言，用于支持自主航天器操作。在本文中，我们提出了一个重写的逻辑语义PLEXIL在Maude，一个高性能的逻辑引擎。重写逻辑语义本身就是语言的形式解释器，可以用作PLEXIL执行程序实现的语义基准。在Maude中的实施还有一个额外的好处，即为PLEXIL设计人员和开发人员提供Maude提供的所有正式分析和验证工具。PLEXIL语义在重写逻辑中的形式化提出了一个有趣的挑战，由于语言的同步性和定义其语义的优先级规则。为了克服这个困难，我们提出了一个通用的程序，用于模拟同步集关系重写逻辑是健全的，确定性的关系，完成。我们还报告了两个问题，在设计层面上的原始PLEXIL语义确定的帮助下，在Maude的可执行规范。
2010-02-15 cs.LO cs.PL
Verification of recursive parallel systems
在本文中，我们考虑证明适合用递归和并行来描述（无限状态）系统的形式主义的无限行为的性质的问题。作为一个正式的设置，我们认为过程重写系统（PRS）的框架。对于一个有意义的片段的PRS，允许同时容纳下推自动机和Petri网，我们状态的可判定性结果的一类性质的无限衍生物（无限长期重写）。所得结果可用于PRS描述的无限状态系统的某些线性时间性质的自动验证。为了验证评估结果，我们引入了一个有意义的基于自动机的形式主义，它允许表达递归和多线程。
2003-12-11 cs.LO
A Minimal OO Calculus for Modelling Biological Systems
在本文中，我们提出了一个最小的面向对象的核心演算建模的生物概念的类型，产生于生物本体的形式主义的基础上长期重写。该演算实现了封装、方法调用、子类型和一种简单的重写继承形式，并且适用于以最流行的术语重写形式主义设计的模型。以形式实现的类可以在几个模型中使用，如编程库。
2011-09-07 cs.CE cs.LO
ZX-Calculus and Extended Hypergraph Rewriting Systems I: A Multiway Approach to Categorical Quantum Information Theory
范畴量子力学和Wolfram模型提供了不同但互补的方法来研究组合结构上的图形重写系统与物理学基础之间的关系;本文的目的是在Coecke和Duncan的ZX演算形式主义的背景下开始阐明这两种方法之间的形式对应关系，用于图解地推理量子比特之间的线性映射。在简要总结了相关的形式主义，并提出了一个明确的公式的Wolfram模型的粘合剂类别和双推出重写系统，我们说明了如何图形重写的ZX演算可以嵌入和实现在更广泛的背景下Wolfram模型多路系统，并举例说明我们专门为此目的开发的软件框架（ZXMultiwaySystem）的一些功能。最后，我们提出了一个证明（连同一个明确计算的例子）的方法的基础上的狄克逊和基辛格的多路演化图和分支图的Wolfram模型是自然赋予monoidal结构的基础上rulial组成，而且，兼容的monoidal产品的ZX图。
2020-10-05 cs.DM cs.LO
A Category of Surface-Embedded Graphs
引入曲面嵌入图重写的范畴形式化方法，通过明确记录边界的双推出重写新表述与旋转系统，将曲面拓扑纳入其中以表示非对称弦图。
2023-07-31 cs.LO
A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems
本文提出了一种基于算法的方法来证明命题系统的归纳性质，如可容许性，可逆性，割消和单位扩展。虽然一般来说是不可判定的，但这些结构属性在证明理论中是至关重要的，因为它们可以减少证明搜索工作，并进一步用作获得其他元结果（如一致性）的脚手架。算法-利用重写逻辑元逻辑框架，并使用重写和缩小为基础的推理-详细解释，并说明整个文件的例子。他们已经完全机械化的L-框架，从而提供了一个正式的规约语言和现成的机械化的证明搜索算法来证明定理和元定理的目标系统的半决策程序。本文通过实例分析说明，L-框架在单结论和多结论直觉逻辑、经典逻辑、经典线性逻辑及其二元系统、直觉线性逻辑和正规模态逻辑等命题推理系统上的应用，实现了很大程度的自动化。
2021-01-08 cs.LO math.LO
A Machine Learning guided Rewriting Approach for ASP Logic Programs
Department of Mathematics and Computer Science University of Calabria（卡利亚里大学数学与计算机科学系）
回答集编程（ASP）是一种声明式逻辑形式主义，允许通过逻辑程序编码计算问题。尽管声明性质的形式主义，一些先进的专业知识是必需的，在一般情况下，设计一个ASP编码，可以有效地评估一个实际的ASP系统。试图减少手动调整ASP程序的负担的常见方法包括根据合适的技术自动重写输入编码，以产生替代的但语义上等效的ASP程序。然而，重写并不总是在性能方面给予好处，因此，需要适当的手段来预测其效果与这方面。在本文中，我们描述了一种基于机器学习（ML）的方法来自动决定是否重写。特别是，给定一个ASP程序和一组输入事实，我们的方法选择是否以及如何重写输入规则的基础上测量其结构属性和域信息的一组功能。为此，一个多层感知器模型，然后训练，以指导ASP地面I-DLV重写输入规则。我们报告并讨论了一个原型实现的实验评估的结果。
2020-09-22 cs.AI cs.LG cs.LO
Combinatorial Conversion and Moment Bisimulation for Stochastic Rewriting Systems
本文提出组合转换与矩互模拟方法，用于分析随机重写系统动力学，并展示图形重写系统与离散重写系统间的矩互模拟关系，为应用化学反应系统分析技术铺路。
2020-07-09 cs.DM cs.LO math-ph
Dependency Stochastic Boolean Satisfiability: A Logical Formalism for NEXPTIME Decision Problems with Uncertainty
随机布尔可满足性（Stochastic Boolean Satisfiability，SSAT）是一种逻辑形式主义，用于建模具有不确定性的决策问题，例如用于概率系统验证的部分可观察马尔可夫决策过程（Partially Observable Markov Decision Process，POMDP）。然而，SSAT受限于其在PSPACE复杂性类中的描述能力。更复杂的问题，如NEXPTIME完全分散POMDP（Dec-POMDP），不能用SSAT简洁地编码。为了提供这样的问题的逻辑形式主义，我们扩展的依赖量化布尔公式（DQBF），在NEXPTIME-完全类的代表性问题，其随机变量，命名为依赖SSAT（DSSAT），并显示DSSAT也是NEXPTIME-完全的。我们展示了DSSAT的潜在应用的概率和近似设计的电路综合。此外，为了研究DSSAT的描述能力，我们建立了从Dec-POMDP到DSSAT的多项式时间约简。随着这项工作的理论基础，我们希望鼓励DSSAT解算器的发展，为潜在的广泛应用。
2021-02-25 cs.CC cs.LO
Abstract Certification of Global Non-Interference in Rewriting Logic
非干扰性是一种语义程序属性，它为数据对象分配保密级别，并防止非法信息流从高到低的安全级别发生。在本文中，我们提出了一种新的安全模型的全局不干扰，近似不干扰作为一个安全属性。我们还提出了一个认证技术的全球非干扰完整的Java类重写逻辑的基础上，一个非常一般的逻辑和语义框架，有效地实现了高层次的程序设计语言Maude。从现有的Java语义规范Maude写的，我们开发了一个扩展的，信息流的Java语义，使我们能够正确地观察全球的非干扰政策。为了实现有限状态转换系统，我们开发了一个抽象的Java语义，我们使用安全和有效的非干扰Java分析。分析产生的证书是可独立检查的，并且足够小，可以在实践中使用。
2010-06-22 cs.CR cs.LO cs.PL
Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory
有两种根本不同的方法来指定和验证系统的属性。逻辑方法利用规范给出的时间或模态逻辑的公式，并依赖于有效的模型检验算法;行为方法利用各种等价或细化检查方法，提供的规格是在相同的形式主义实现。在本文中，我们提供的最大不动点的Hennessy-Milner逻辑的逻辑形式主义和析取模态转换系统的行为形式主义之间的翻译。我们还介绍了一个新的操作商的上述等价的形式主义，这是伴随的结构组成，并允许合成缺失的规范从部分实现。这是一个实质性的推广商确定性模态过渡系统中定义的早期文件。
2013-06-04 cs.LO
GRUNGE: A Grand Unified ATP Challenge
本文描述了一个大的相关的定理证明的问题，从HOL 4标准库转换成多个逻辑形式。形式主义是高阶逻辑（有或没有类型变量）和一阶逻辑（可能有多个类型，也可能有类型变量）。由此产生的问题集允许我们在相应的问题上运行支持不同逻辑格式的自动定理证明器，并比较它们的性能。这也导致了一个新的“大统一”的大型理论基准，模拟ITP/ATP锤设置，其中系统和元系统可以以互补的方式使用多种ATP形式，并共同从积累的知识中学习。
2019-11-19 cs.LO
Computational Logic: Its Origins and Applications
计算逻辑是使用计算机以逻辑形式建立事实。起源于19世纪试图理解数学推理的本质，该主题现在包括各种各样的形式主义，技术和技术。其中一种工作遵循Robin Milner FRS开创的“LCF方法”，在这种方法中，可以交互地或在用户代码的帮助下（不损害正确性）构建证明。LCF的一个改进，称为Isabelle，保留了这些优点，同时在逻辑形式主义的选择和更强的自动化方面提供了灵活性。这些技术的主要应用是证明硬件和软件系统的正确性，但越来越多的研究人员将其应用于数学本身。
2018-02-14 cs.LO
Composing Programs in a Rewriting Logic for Declarative Programming
基于构造器的条件重写逻辑是一个集成一阶泛函和逻辑程序设计的通用框架，它为非确定性泛函-逻辑程序提供了一种代数语义。在这种形式主义的背景下，我们引入了一个简单的概念，程序模块作为一个开放的程序，可以扩展与几种机制结合起来。这些机制是基于一组减少的操作。然而，这些操作的高表达性使我们能够以简单的方式为程序模块化建模典型的构造，如隐藏，导出/导入，泛型/实例化和继承。我们还通过引入一个直接结果运算符来处理该建议的语义方面，并在逻辑编程的路线上研究基于该运算符的程序模块的几种替代语义：运算符本身，它的最小不动点（模块的最小模型），其前缀定点的集合（模块的术语模型）和一些其他变体，以便找到一个组合的和完全抽象的语义wrt的操作集和一个自然的可观察性概念。
2002-03-04 cs.LO cs.PL
Interactions between Causal Structures in Graph Rewriting Systems
图重写形式主义是一个强大的方法来建模复杂的分子系统。它们捕捉分子相互作用的内在并发性，从而实现机制的正式概念（部分有序的事件集），解释系统如何在给定一组重写规则的情况下实现特定结果。然后，验证从给定模型中出现的机制是否符合关于它们相互干扰的经验观察是有用的。在这项工作中，我们的目标是确定实现X的机制中的特定事件是否阻止或促进实现Y的机制中的特定事件的发生。这种检查也可用来假设使示范机制符合观察结果的规则。我们定义了一个严格的框架，用于定义由图形重写规则系统引起的机制之间的干扰（积极或消极）的概念，并用于确定是否可以实现两种机制作为输入的断言的影响。
2019-01-03 cs.CE cs.LO
Decidability of Graph Neural Networks via Logical Characterizations
本文利用Presburger量词等可判定逻辑刻画图神经网络的表达能力，建立了精确对应关系，并据此提出了GNN验证问题的判定过程，同时证明了相关静态分析与验证问题的不可判定性。
2025-01-29 cs.LO
Encoding of Predicate Subtyping with Proof Irrelevance in the $λ$$Π$-Calculus Modulo Theory
$λ$ $Π$ -演算模理论是一个逻辑框架，其中可以编码各种逻辑和类型系统，从而帮助基于这些逻辑和类型系统的证明系统的交叉验证和互操作性。在本文中，我们将展示如何编码谓词子类型和证明无关性，这是PVS证明助手的两个重要特性。我们证明，这种编码是正确的，编码的证明可以机械检查Dedukti，类型检查器的$λ$ $Π$ -微积分模理论，使用重写。
2021-10-26 cs.LO
A Visual Analytics Approach to Compare Propagation Models in Social Networks
描述社交网络中的社会影响的许多传播模型可以在文献中找到。这使得在特定情况下难以选择适当的模式。选择最相关的模型需要能够客观地比较它们。这种比较只能以描述基于共同形式主义但又独立于它们的模型为代价。我们建议使用图重写来正式描述传播机制作为根据策略应用的本地转换规则。当这种方法得到专用于图重写的可视化分析框架的支持时，它是有意义的。本文首先介绍了我们的方法来描述一些传播模型作为一个图重写问题。然后，我们说明了我们的可视化分析框架如何允许交互式地操纵模型，并强调它们的差异的基础上计算的模拟轨迹的措施。
2015-04-10 cs.LO cs.SI
Logic-Parametric Neuro-Symbolic NLI: Controlling Logical Formalisms for Verifiable LLM Reasoning
University of Luxemburg（卢森堡大学）；University of Sheffield（谢菲尔德大学）
本文提出逻辑参数化框架，通过可控逻辑形式提升神经符号推理的鲁棒性与适应性，实验表明内部逻辑策略在不同领域具有更优表现。
2026-01-09 cs.AI cs.CL cs.LO
A pilot study of the use of LogEx, lessons learned
LogEx是一个学习环境，支持学生重写命题逻辑公式，使用标准等价。我们组织了一项试点研究，准备对学习环境进行大规模评估。在本文中，我们描述了这项研究，连同结果，这给了我们宝贵的经验教训，为大规模的评估。
2015-07-14 cs.CY cs.LO
Behavioural Preorders on Stochastic Systems - Logical, Topological, and Computational Aspects
计算机系统随处可见：在太空中，在我们的家里，在我们的汽车里，在我们的口袋里，有时甚至在我们自己的身体里。出于安全、经济和方便的考虑，这种系统正确工作是重要的。然而，确保计算机上运行的软件正确运行是一项非常困难的任务。一种简化此任务的方法是模型检验，其中使用某种数学形式建立系统的模型。然后可以针对模型验证以形式语言表达的需求，以保证模型满足需求。对于许多计算机系统，时间是一个重要因素。因此，我们需要我们的形式主义和需求语言能够纳入实时的。因此，我们开发的形式主义和算法，使我们能够比较和表达实时系统的属性。我们首先介绍了一个逻辑形式主义的推理时间上的上限和下限，并研究这种形式主义的性质，包括axiomatisation和算法检查时，一个公式是满意的。然后我们考虑一个系统何时比另一个系统快的问题。我们表明，这是一个困难的问题，不能在一般情况下回答，但我们确定特殊情况下，这个问题可以回答。我们还表明，在这个概念的快于，局部速度的增加可能会导致全球速度下降，我们采取措施，以避免这种情况。最后，我们考虑如何比较系统的实时行为不仅定性，而且定量。因此，我们有兴趣知道一个系统比另一个系统快或慢多少。这是通过引入系统之间的距离来实现的。我们展示了如何计算这个距离，它的行为以及相对于某些属性。
2019-05-21 cs.FL cs.LO
Strong Equivalence and Program Structure in Arguing Essential Equivalence between Logic Programs
答案集编程是一个突出的声明式编程范式，用于制定组合搜索问题和实现不同的知识表示形式主义。对于一个给定的问题，通常会有几个相关但又有很大不同的答案集程序。有时这些编码可能会显示出显著不同的性能。揭示这些程序之间精确的形式联系通常很重要，但远非微不足道。本文提出了正式的结果仔细有关一些有趣的程序重写。为了提高效率，本文还对系统Projector自动重写程序的正确性进行了证明。逻辑程序设计理论与实践（TPLP）
2021-09-07 cs.AI cs.LO
On the Existence of Characterization Logics and Fundamental Properties of Argumentation Semantics
考虑到现有的各种各样的逻辑形式主义，选择最合适的一个用于特定目的是至关重要的，例如，用于表示与特定应用相关的知识或使用形式主义作为问题解决的建模工具。对逻辑形式主义的本质的认识，换句话说，对它的基本内在属性的认识，是必不可少的，并为明智的选择提供了基础。在这篇论文中，我们考虑了存在性特征逻辑以及抽象论证领域中的存在唯一性、可表达性、可替换性和可验证性等性质
2020-03-02 cs.AI cs.LO
Logics for Epistemic Actions: Completeness, Decidability, Expressivity
我们考虑动态版本的认知逻辑，如Baltag和Moss的“认知程序的逻辑”（2004）中所阐述的。这篇论文提出了一种动态认知逻辑的逻辑语言（实际上是由动作签名参数化的语言家族）。已有研究表明，该语言的有效性是Pi-1-1-完备的，因此不存在递归公理化的完备逻辑系统，而本文则证明了无动作迭代的片段的弱完备性结果，以及无动作迭代的片段和常识的强完备性结果。我们的工作涉及到术语重写理论的迂回。该论点使用模态过滤，因此我们得到有限的模型属性，因此可判定性。我们也给我们最大的语言翻译成PDL，从而获得第二个证明的可判定性。本文最后给出了一些关于表达能力的结果。这些主要涉及比较动作迭代自由语言与模态逻辑增强传递闭包运算符。我们回答了一个自然的问题，我们通过不同的动作签名获得的语言：我们证明了一个逻辑语言与运营商的私人公告更有表现力比一个公共公告。
2022-03-13 cs.LO math.LO
On the distributed evaluation of recursive queries over graphs
诸如一阶逻辑（FO）和定点逻辑（FP）之类的逻辑形式主义非常适合以声明的方式表达分布式系统中所需的基本图形功能。我们表明，这些逻辑构成良好的抽象编程分布式系统作为一个整体，因为它们可以在一个完全分布式的方式进行评估，合理的复杂性上限。我们首先证明FO和FP可以用对数大小的消息的多项式数进行评估。然后，我们表明，（全球）的逻辑公式可以被翻译成规则程序描述的分布式系统的节点的本地行为，计算等价的结果。最后，我们介绍了这些逻辑，尽可能多地保留其分布式计算的本地片段，同时提供了丰富的网络功能的表达能力。我们证明，他们承认更严格的上限有界的消息数量有界的大小。最后，我们表明，本地片段的语义和复杂性被保存在本地一致的网络以及匿名网络，从而显示出所提出的本地逻辑形式主义的鲁棒性。
2009-04-21 cs.DC cs.LO
Logic Tensor Networks: Deep Learning and Logical Reasoning from Data and Knowledge
Fondazione Bruno Kessler（布鲁诺·凯斯勒基金会）；City University London（伦敦城市大学）
我们提出了逻辑张量网络：一个统一的框架，集成自动学习和推理。一个逻辑形式主义称为真正的逻辑是定义在一阶语言，其中公式的真值在区间[0，1]和语义定义具体的实数域。逻辑常数被解释为实数的特征向量。Real Logic促进了基于知识库的演绎推理和高效的数据驱动关系机器学习的良好集成。我们展示了如何使用Google的tensorflow原语在深度张量神经网络中实现Real Logic。最后，本文将逻辑张量网络应用于一个简单但具有代表性的知识完成示例。
2016-07-07 cs.AI cs.LG cs.LO
A Unified Algebraic Framework for Non-Monotonicity
German University in Cairo（开罗德国大学）；Cairo University（开罗大学）
多年来，人们一直致力于深入研究非单调推理。随着非单调逻辑形式主义的丰富，一个统一的理论，使比较不同的方法是非常必要的。在本文中，我们提出了一种代数分级逻辑，称为LogAG，能够包含各种非单调形式主义。我们建立在林和Shoham的参数系统首先开发的形式化非单调常识推理。我们展示了如何编码的参数系统LogAG理论，并证明LogAG捕获的概念，相信空间的参数系统。由于参数系统捕获默认逻辑，自认知逻辑，作为失败的否定原则，和限制，我们的研究结果表明，LogAG捕获上述非单调逻辑形式主义以及。以往的结果表明，LogAG包含可能性逻辑和任何非单调推理关系满足梅金森的合理性假设。通过这种方式，LogAG为非单调性提供了一个强大的统一框架。
2019-07-22 cs.AI cs.LO cs.SC
