Formalizing cCSP Synchronous Semantics in PVS
补偿CSP（Compensating CSP，cCSP）是一种定义为在标准CSP进程代数框架内对长时间运行的业务事务进行建模的语言。在早期的工作中，我们已经定义了语言的跟踪和操作语义。我们通过定义两个语义模型之间的关系，证明了它们之间的一致性。同步在早期的语义定义中是缺失的，而同步是任何进程代数的重要特性。在本文中，我们通过扩展语法和语义来支持同步并定义语义模型之间的关系来解决这个问题。此外，我们通过使用定理证明器PVS机械地验证语义关系来提高我们的证明技术的可扩展性。我们展示了如何将进程代数术语和语义嵌入到PVS中，并使用这些嵌入来证明语义关系。
2010-01-20 cs.LO
Formal Semantics and Formally Verified Validation for Temporal Planning
Techniche Universität München（慕尼黑工业大学）；King’s College London（伦敦国王学院）
我们提出了一个简单而简洁的语义时间规划。我们的语义开发和形式化的逻辑的互动定理证明伊莎贝尔/HOL。我们从这些语义的验证算法的时间规划和显示，使用Isabelle/HOL的正式证明，该验证算法实现我们的语义。我们通过实验评估我们验证的验证算法，并表明它是实用的。
2022-03-25 cs.AI cs.LO
A Formalization of the Semantics of Functional-Logic Programming in Isabelle
现代函数逻辑程序设计语言（如Toy或Curry）具有非严格的非确定性函数，这些函数在调用时选择语义下运行。这种语义的标准公式是CRWL逻辑，它指定了一个证明演算来计算每个表达式的可能结果集。在本文中，我们提出了一个形式化的演算在伊莎贝尔/HOL证明助手。我们已经证明了CRWL的一些基本性质：C-替换下的封闭性，极性和组合性。我们还讨论了已经获得的一些见解，如事实上，左线性的程序规则是不需要任何这些结果举行。
2009-08-04 cs.LO
A Formal Semantic for UML 2.0 Activity Diagram based on Institution Theory
给UML活动图（UMLAD）一个正式的语义是一项艰巨的任务。这种困难的原因是这种半形式化的形式主义的模糊性和精确的形式语义的缺乏。各种各样的语义学存在于处理这种语言所涵盖的各个方面的文献中。我们可以给出指称语义、功能语义和组合语义的例子。为了应付最近的趋势，给了一个异构的语义UML图，我们的目标是定义一个代数表示的语义UML AD。在这项工作中，我们定义了一个正式的语义UML 2.0 AD的基础上机构理论。对于UML AD形式化，这是一种图形化的语言，没有精确的形式语义，我们使用机构理论来定义预期的语义。因此，UMLAD形式主义将被定义在它自己的自然语义中。
2016-06-07 cs.LO cs.SE
A Formalization of SQL with Nulls
SQL是世界上最流行的声明性语言，是数十亿美元数据库行业的基础。虽然SQL已经标准化，但完整的标准是基于模糊的自然语言，而不是正式的规范。商业SQL实现以不同的方式解释标准，因此，给定相同的输入数据，相同的查询可以根据它运行的SQL系统产生不同的结果。即使对于特定的系统，SQL的所有广泛使用的功能的机械检查形式化仍然是一个开放的问题。缺乏一个良好理解的形式化语义使得验证数据库实现的可靠性非常困难。尽管SQL片段的形式化语义在过去已经设计好了，但它们通常不支持集合和包操作、横向连接、嵌套子查询，以及至关重要的空值。空值使SQL的语义复杂化，其方式与其他程序设计语言中的空指针或副作用类似。由于某些SQL查询在没有空值的情况下是等价的，但当应用于包含不完整数据的表时会产生不同的结果，因此忽略空值的语义能够证明在现实数据库中不合理的查询等价性。支持所有上述功能的SQL的正式语义最近才被提出。在本文中，我们报告我们的机械化SQL语义涵盖集/袋操作，横向连接，嵌套的子查询，空值，写在Coq证明助手，并描述了关键元属性的验证。此外，我们能够使用相同的框架来形式化平面关系演算（具有空值）的语义，并显示其范式到SQL的认证翻译。
2022-06-20 cs.LO
Realisability semantics of abstract focussing, formalised
我们提出了一个抽象的焦点，配备了证明条款的微积分：在传统的Zeilberger的工作，逻辑连接词和它们的介绍规则是作为一个参数的系统，它崩溃的同步和异步阶段的焦点作为宏观规则。我们进一步离开作为一个参数的操作，扩展了一个新的假设的背景下，这使我们能够捕捉经典和直观的聚焦微积分。然后，我们定义的可实现性语义（的证明）的系统，蒙奇-Maccagnoni的正交模型的基础上，经典的集中式微积分，但现在在更高的抽象层次上操作上述。在这个层次上，我们证明了一个引理，即如果一个项是A型的，那么在模型中它的外延是在A的（集合论）解释中。这表明了这样一个事实：取集合的正交时所涉及的全称量化在语义中反映了Zeilberger在异步阶段宏观规则中的全称量化。系统及其语义都在Coq中形式化。
2015-11-13 cs.LO
Two Remarks about Game Semantics of Classical Logic
University of Gothenburg（哥德堡大学）
本文介绍了Stefano Berardi关于经典逻辑游戏语义的两个未发表注记，并对其进行了解释。
2026-03-04 cs.LO
An Operational Semantics for the Cognitive Architecture ACT-R and its Translation to Constraint Handling Rules
计算心理学的目标是通过认知过程的计算模型来解释人类的认知。认知架构ACT-R是流行的开发这样的模型。虽然ACT-R有一个定义良好的心理学理论，并已被用来解释许多认知过程，有两个问题，使它很难正式推理的认知模型：首先，ACT-R缺乏一个形式化的底层产生式规则系统，其次，有许多不同的实现和扩展的ACT-R的技术工件复杂的形式推理。本文描述了一个正式的操作语义-非常抽象的语义-抽象尽可能多的技术细节，保持开放的扩展和不同的实现的ACT-R理论。在第二步中，此语义被细化以定义其在ACT-R的许多实现中发现的一些抽象特征-抽象语义。它集中在ACT-R的程序核心，适合于分析过渡系统，因为它仍然抽象的细节，如时间，子符号层或冲突解决。此外，定义了ACT-R模型到程序设计语言约束处理规则（Constraint Handling Rules，简称CSTR）的翻译。这使得抽象语义成为ACT-R的可执行规范。它已成功地用于嵌入其他基于规则的形式主义，如图转换系统或函数式编程。有许多结果和工具，支持形式化推理和分析的可重构程序。将ACT-R模型转换为XML已被证明是可靠和完整的。ACT-R的抽象操作语义。这为通过CHR分析ACT-R模型铺平了道路。因此，据我们所知，我们的抽象语义是第一个适合分析和执行的ACT-R公式。
2017-02-06 cs.LO
T-BAT semantics and its logics
本文研究表达非形式可证明性的T-BAT非确定四值逻辑，通过真值转换证明其可定义逻辑的完备性，并利用Kripke语义考察公理，最终给出直观公理化。
2025-10-16 cs.LO
Formal semantics of language and the Richard-Berry paradox
Politecnico di Milano（米兰理工大学）
经典的逻辑二律背反被称为理查德-贝瑞悖论，它与关于图灵机形式化某些句子的规模（即逻辑复杂性）的合理假设相结合，以表明语言的形式化导致矛盾。
2008-07-24 cs.CC cs.CL cs.LO
Virtual Evidence: A Constructive Semantics for Classical Logics
本文提出了一个计算语义的经典逻辑使用建设性类型论。这样的语义似乎是不可能的，因为经典逻辑允许排中律（LEM），而在构造性逻辑中不被接受，因为它没有计算意义。然而，在逻辑推理模型中所表达的明显的神谕力量，即对于任何命题P，要么它是真的，要么它的否定是真的，而不是P，也可以用不涉及“真理的神谕”的构造性证据来解释。具有虚拟证据和否定证据的构造性不可能性的类型为经典真理提供了足够的语义基础，并且具有简单的计算意义。这个想法是使用精化类型形式化的，精化类型是自1984年以来使用的构造性类型论的概念，在这里解释。一个新的公理创建虚拟证据，充分保留了经典语境中的逻辑算子的建设性意义。关键词：经典逻辑，构造性逻辑，直觉主义逻辑，命题类型，构造性类型论，精化类型，双重否定翻译，计算内容，虚拟证据
2014-08-31 cs.LO
Dunn Semantics for Contra-Classical Logics
在本文中，我展示了丰富的和系统化的饮食的例子，许多反经典逻辑可以作为FDE的变体，通过修改某些连接的真或假条件中的至少一个来获得。然后，我认为，使用邓恩语义学提供了一个清晰的理解的反经典性的来源，即，连接词，要么有经典的真理或经典的虚假条件的另一个连接。这需要对可以对评估条件进行的各种修改进行细粒度的分析，我在这里也提供了这种分析。
2022-04-14 cs.LO
On the Formal Semantics of the Cognitive Middleware AWDRAT
本文的工作有两个目的：一方面，我们希望对自生成和自适应的认知中间件AWDRAT的关键组件的行为进行形式化描述，这样不仅有助于理解中间件的语义和技术细节，而且为扩展中间件以支持其他复杂的网络安全应用领域提供了机会;另一方面，形式化是我们证明关键组件行为正确性的前提，以确保中间件本身的安全性。然而，这里我们只关注中间件的核心和关键组件，即执行监视器，它是AWDRAT的“架构差异”模块的一部分。执行监视器的作用是识别目标系统的运行时观察和系统架构模型的预测之间的不一致。因此，为了实现这一目标，我们首先定义的正式（指称）的观察（运行时事件）和预测（可执行规范的系统架构模型）的语义，然后基于上述正式语义，我们正式的“执行监视器”的中间件的行为。
2014-12-14 cs.LO cs.PL
Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS
我们以前已经出版了Isabelle/HOL形式化的一般理论的语法绑定。在这篇配套文件中，我们实例化的一般理论，以语法的λ演算和形式化的发展，导致几个基本的结构和结果：健全的语义解释，教会罗瑟和标准化定理，高阶抽象语法（HOAS）编码。对于Church-Rosser和标准化，我们的工作涵盖了微积分的按名称调用和按值调用版本，遵循Takahashi和Plotkin的经典论文。在形式化过程中，我们能够专注于开发的高级思想-感谢我们的一般理论提供的武器库：关于替换，交换和新鲜度操作符的丰富基本事实，以及递归定义和推理原则，包括语法语义解释的专业化。
2021-07-24 cs.LO cs.PL
Semantic Incompleteness of Hilbert System for a Combination of Classical and Intuitionistic Propositional Logic
本文证明del Cerro和Herzig提出的希尔伯特系统(C+J)−因缺少经典肯定前件规则而在语义上不完备，并利用Priest的悖论逻辑给出论证。
2023-12-26 cs.LO
Industrial Experiences with a Formal DSL Semantics to Check Correctness of DSL Transformations
领域特定语言（DSL）从实现细节中抽象出来，并与领域专家对软件组件的推理方式保持一致。DSL的开发通常围绕生成实现代码或分析模型的语法和转换。语言的语义通常是隐式定义的，并根据实现代码的转换来定义。在存在来自DSL的多个转换的情况下，生成的工件相对于DSL的语义的一致性是一个相关的问题。我们表明，一个正式的语义是必不可少的检查生成的工件之间的一致性。我们利用工业项目中的形式化语义，并使用形式化技术的基础上，等价性检查和基于模型的测试的一致性检查。我们报告我们的经验，这种方法在一个工业发展项目。
2015-11-25 cs.LO cs.PL cs.SE
Industrial Experiences with a Formal DSL Semantics to Check the Correctness of DSL Artifacts
领域特定语言（DSL）从实现细节中抽象出来，并与领域专家对软件组件的推理方式保持一致。DSL的开发通常围绕生成实现代码或分析模型的语法和转换。语言的语义通常是隐式定义的，并根据实现代码的转换来定义。在存在来自DSL的多个转换的情况下，生成的工件相对于DSL的语义的正确性是一个相关的问题。我们表明，一个正式的语义是必不可少的检查生成的工件的正确性。我们利用工业项目中的形式语义，并使用基于等价性检查和基于模型的测试验证生成的工件的正确性的形式化技术。我们报告我们的经验，这种方法在一个工业发展项目。
2016-03-29 cs.LO cs.PL cs.SE
First-order swap structures semantics for some Logics of Formal Inconsistency
形式不一致逻辑（LFI）是次协调逻辑（即包含矛盾但非平凡理论的逻辑），具有一致性连接符，允许以受控的方式恢复ex falso quodlibet原则。本文的目的是考虑一种新的语义方法，一阶线性模糊集的基础上塔斯基结构定义在交换结构，一类特殊的多代数。拟议的语义框架概括了以前的aproaches量化的LFI在文献中提出的。QmbC的情况下，更简单的量化LFI扩展经典逻辑，将进行详细分析。本文还研究了QmbC的一个公理化扩展QLFI10，它等价于da Costa和D'Ottaviano三值逻辑J3的量化形式.这种逻辑的语义结构是基于扭曲结构的塔肯结构。还考虑了QmbC和QLFI1o使用标准相等谓词的扩展。
2019-12-21 cs.LO math.LO
Implementation of Formal Semantics and the Potential of Non-Classical Logic Systems for the Enhancement of Access Control Models: A Literature Review
该文献综述梳理了经典逻辑在现有访问控制模型中的应用及模型局限，探究了用非经典逻辑系统增强访问控制模型的潜力，并明确了经典逻辑对RBAC、ABAC模型正确性的描述与证明作用。
2023-08-24 cs.CR cs.LO
A New Semantic Theory of Natural Language
形式语义学和分布语义学是自然语言处理中两个重要的语义框架。认知语义学属于认知语言学运动，它建立在当代认知科学的基础之上。每个框架都能处理一些意义现象，但没有一个能满足应用程序提出的所有要求。建立一个统一的语义理论来描述所有重要的语言现象具有重要的理论意义和实践意义，然而，尽管近年来人们进行了许多尝试，但迄今为止还没有一个理论能够实现这一目标。本文介绍了一种新的语义理论，它有可能描述自然语言的大多数重要意义现象，并满足哲学分析和自然语言处理应用的大多数必要要求。该理论以信息的统一表示为基础，构建了一种称为认知模型的数学模型，以组合的方式解释自然语言表达式。它接受了认知语义学的经验假设，克服了形式语义学和分布语义学的大部分缺点。然而，该理论不是现有理论的简单组合，而是对经典逻辑和形式语义学的广泛概括。它继承了形式语义学几乎所有的优点，并为对象和事件提供尽可能细的描述内容，描述内容代表了人类认知的结果。
2017-09-10 cs.CL cs.LO
A Formal Semantics of the GraalVM Intermediate Representation
本文在Isabelle/HOL中为GraalVM的图式SSA中间表示构建大步数据节点语义与小步控制流语义，并据此证明规范化和条件消除优化的正确性。
2021-07-05 cs.LO cs.PL
Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq
集束蕴涵逻辑（BI）是构成分离逻辑主干的子结构逻辑，分离逻辑是研究堆操作程序推理的逻辑。虽然BI的证明理论和元理论在数学上都有涉及，但重要的元理论结果的形式化仍然刚刚起步。在本文中，我们提出了一个自包含的形式化，在Coq的证明助手，证明了中央元理论性质的BI：削减消除其微积分。提出的证明是 * 语义 *，在这个意义上说，是通过解释在一个特定的“通用”模型的序列。这导致了一个比标准的Gentzen风格的切割消除参数更模块化和优雅的证明，这在BI的手动证明中可能是微妙和容易出错的。特别是，我们的语义方法避免了不必要的反演证明推导，或使用削减减少和多削减规则。除了模块化，我们的方法也是强大的：我们演示了我们的方法规模，与微小的修改，（i）BI的扩展与任意一组的\emph{simple structural rules}，和（ii）扩展与S4一样的$\Box$模态。
2021-12-10 cs.LO math.LO
FSLI: An Interpretable Formal Semantic System for One-Dimensional Ordering Inference
University of Massachusetts Amherst（马萨诸塞大学阿默斯特分校）
FSLI将自然语言排序推理转化为一阶逻辑，通过基于组合语义的解析算法和约束逻辑编程实现可解释的符号演绎，在BIG-bench上达100%准确率并优于LLM基线。
2025-09-19 cs.CL cs.LO
Semantically Reflected Programs
IT University of Copenhagen（哥本哈根信息技术大学）；University of Oslo（奥斯陆大学）
本文通过语义提升程序解决结构化与行为化知识形式化之间的矛盾，提出面向对象编程语言的语义反射层，通过地质建模案例展示其应用。
2026-04-07 cs.LO cs.PL
Formal Languages and Algorithms for Similarity based Retrieval from Sequence Databases
本文考虑了基于自动机，时态逻辑和正则表达式的各种形式主义，用于指定序列上的查询。与传统的二进制语义不同，本文提出了一种基于相似度的语义。更具体地，范围[0，1]中的距离度量与序列相关联，查询对表示序列满足查询的紧密程度。这些措施被定义使用频谱的赋范向量距离措施。提出了基于查询的语法和传统语义的各种距离度量。提出了计算这些距离测度的有效算法。这些算法可用于从数据库中检索紧密满足给定条件的序列。
2005-01-04 cs.DB cs.LO
Towards a Formal Distributional Semantics: Simulating Logical Calculi with Tensors
University of Oxford（牛津大学）
语义的组合分布模型的发展调和了分布语义的经验方面与形式语义的组合方面，是当代文献中的一个热门话题。本文旨在通过展示如何使用组合分布模型中常用的数学结构（如张量和矩阵）来模拟谓词逻辑的不同方面，进一步实现这种和解。本文讨论了如何利用张量和多线性映射之间的规范同构来模拟一个成熟的无量词谓词演算使用张量。它提供了一组逻辑连接词的张量解释，这些逻辑连接词是建模命题演算所必需的。它提出了这些张量演算的一个变体，能够使用很少的非线性运算来模拟量词。最后讨论了这些变体之间的关系，以及这种关系如何构成未来工作的主题。
2013-04-28 cs.CL cs.LO math.LO
Evaluation and Comparison Semantics for ODRL
University of Southampton（索姆塞特大学）
本文为ODRL提供基于查询回答的直观形式化语义，并定义策略比较方法，以检测等价、更严格或更宽松的策略，支持数据共享场景。
2025-09-05 cs.AI cs.LO
Formal Specification and Integration of Distributed Security Policies
我们提出了安全策略语言（SePL），这是一个形式语言捕获和集成分布式安全策略。SePL的语法包括用于策略集成的几个运算符，并且它被赋予作为通用语义的指称语义，即，它独立于任何评估环境。我们证明了完整的SePL集理论。此外，我们提供了一个可扩展访问控制置标语言（XACML），这是众所周知的标准非正式的规约语言的Web安全策略的子集的形式化。我们还提供了一个语义XACML策略组合算法。
2020-05-09 cs.CR cs.LO
Theorem proving support in programming language semantics
我们描述了几种观点的语义的一个简单的程序设计语言的正式文件中的演算的归纳结构，可以验证的Coq证明系统。涵盖的方面是自然语义、指称语义、公理语义和抽象解释。递归函数的描述也在适当的时候提供，从而产生一个验证条件生成器和一个静态分析器，可以在定理证明器内运行，用于反射证明。还描述了从指称语义提取解释器。所有不同的方面都被正式证明是合理的自然语义规范。
2007-07-10 cs.LO cs.PL
Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable
我们提出了一个形式化证明的不完全信息和完美召回语义下的交替时间时序逻辑的模型检验问题的不可判定性。这个问题被宣布为不可判定的根据个人通信的多人游戏与不完美的信息，但没有正式的证明曾经公布。我们的证明是基于直接减少从非停机问题的图灵机。
2011-02-21 cs.LO cs.MA
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
A Formal, Resource Consumption-Preserving Translation of Actors to Haskell
我们提出了一个正式的翻译的演员为基础的语言与合作调度的功能语言Haskell。翻译被证明是正确的，相对于源语言的形式语义和目标的高级操作语义，即Haskell的子集。主要的正确性定理表示在演员程序的操作语义和他们的翻译之间的模拟关系。这使我们能够证明资源消耗在这种转换中得到了保留，因为我们建立了原始和Haskell转换的执行跟踪的成本等价。
2016-08-10 cs.LO cs.PL
Deriving Relationship Between Semantic Models - An Approach for cCSP
形式语义学为语言提供了一个完整而严格的定义。为一种语言定义不同的语义模型是很重要的，不同的模型服务于不同的目的。在语言的不同语义模型之间建立等价性，加强了语言的形式基础。本文展示了从cCSP语言的操作语义推导出指称语义的过程。其目的是显示操作和跟踪语义之间的对应关系。我们从操作规则中提取轨迹，并使用归纳法来显示cCSP的两个语义之间的对应关系。
2010-02-18 cs.LO cs.SE
B Maude: A formal executable environment for Abstract Machine Notation Descriptions
我们提出了B Maude，一个原型的可执行环境的抽象机器记法实现的Maude语言。B Maude是形式化定义的，它是将AMN的语义实现为$π$框架中的表示的结果，该框架是Mosses的基于一致性的语义和Plotkin的解释自动机的实现。B Maude赋予B方法重写执行、符号搜索和AMN描述的线性时态逻辑模型检验。
2021-08-17 cs.LO cs.SE
Towards a Coq-verified Chain of Esterel Semantics
本文利用 Coq 构建并验证 Esterel 的形式语义链，提出去除 Must/Can 势函数对的微步语义，并证明其对 CSS 的精化以及 CBS 与 CSS 的等价性。
2025-01-06 cs.FL cs.LO cs.PL
Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP
可靠系统工程中使用的模型的复杂性和多样性日益增加，这意味着必须集成各种形式化方法，包括不同的抽象、范式和表示。这种集成依赖于各种符号的统一语义基础，以及各种自动验证工具的协调。本文的贡献是Isabelle/UTP，Hoare和他的统一编程理论的实现，形式语义统一的框架。Isabelle/UTP允许不同范式的计算理论的机械化，以及它们在构建形式化语义模型中的使用。这些可以进一步应用于验证工具的开发，利用Isabelle的证明自动化设施。数学基础的几个层次的发展，包括镜头模型变量和状态空间作为代数对象，字母谓词和关系模型程序，包括代数和公理语义，证明工具霍尔逻辑和细化演算，UTP理论编码计算范式。
2020-06-22 cs.FL cs.LO
Sage: Formalization with Semantic Correction
Huawei Lagrange Mathematics Computing Research Center（华为拉格朗日数学计算研究中心）
Sage 是一个智能体框架，通过四阶段分解生成与双信号语义校正循环，解决自然语言到 Lean 4 形式化的“严谨性幻觉”问题，显著降低答案泄漏并提升编译与语义保真度。
2026-10-01 cs.AI cs.CL cs.LG
An LTL Semantics of Business Workflows with Recovery
我们描述了一个业务工作流的案例研究与异常行为管理（即恢复），并演示了如何时序逻辑和模型检验可以提供一种方法来迭代修改设计，并获得正确的建设系统。要做到这一点，我们定义了一个正式的语义，给出了一个编译的通用工作流模式到LTL，我们使用绑定模型检查器Zot来证明特定的属性和要求的有效性。工作假设是，这种轻量级方法将很容易适应已经存在的流程，而不需要彻底改变程序、工具和人们的态度。形式化的复杂性和方法的侵入性已经被证明是将形式化工程技术部署到平凡项目中的主要缺点和障碍之一。
2014-06-05 cs.LO cs.SE
Characterizing Realizability in Abstract Argumentation
TU Wien（维也纳工业大学）；Leipzig University（莱比锡大学）
知识表示形式化的可实现性研究的问题是：给定一个语义和一组解释，是否存在一个其语义与给定的解释集完全一致的知识库？我们介绍了一个一般的框架，分析可实现性的抽象辩证框架（ADF）和它的各种子类。特别是，该框架适用于Dung论证框架，尼尔森和帕森斯的SETAF，以及双极ADF。我们提出了一个统一的特征化方法的容许，完全，首选和模型/稳定的语义。我们采用这种方法来设计一种算法，决定上述形式主义和语义的可实现性，而且该算法允许构建所需的知识库，只要存在。该算法是内置的一个模块化的方式，因此很容易扩展到新的形式主义和语义。我们还实现了我们的方法在答案集编程，并使用该实现获得了几个新的结果，上述形式主义的相对表现力。
2016-03-31 cs.AI cs.LO
Cognitive Binary Logic - The Natural Unified Formal Theory of Propositional Binary Logic
本文提出了一种形式化理论，它将命题二元逻辑描述为一种语义封闭的形式语言，并允许在相同的（计算）形式语言中，使用相同的数据结构来表达和测试语法和语义上良好的公式、形式证明（在希尔伯特接受中的可论证性）、演绎（根岑的可论证性观点）、CNF化和解构。本文还指出，认知二元逻辑是一种自我描述的理论，它解构了说谎者悖论。
2011-06-12 cs.LO math.LO
(Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs
Department of Mathematical Sciences, Carnegie Mellon University（卡内基梅隆大学数学科学系）
提出Trellis系统，通过确定性约束工作流和LLM代理迭代细化自然语言证明，实现Lean自动形式化，强调严格证明的可细化性。
2026-06-08 cs.AI cs.LO math.CO
An Institutional Framework for Heterogeneous Formal Development in UML
我们提出了一个框架，正式的软件开发与UML。与以前的方法，装备UML与正式的语义，我们遵循一个机构为基础的异构方法。这可以直接表达不同UML图类型的合适的形式语义，而不需要将所有内容映射到一个特定的形式主义（假设它是一阶逻辑或图形语法）。我们展示了如何不同方面的正式开发过程可以连贯地形式化，从设计和霍尔风格的条件代码的实现本身的要求。该框架可以用于水平地验证不同UML图的一致性（例如，各种要求之间的一致性）以及垂直地（例如，设计或实施的正确性的要求）。
2014-03-30 cs.LO cs.SE
Evaluating Autoformalization Robustness via Semantically Similar Paraphrasing
Department of Computer Science and Engineering, The Pennsylvania State University（宾夕法尼亚州立大学计算机科学与工程系）
本文通过语义相似改写生成自然语言变体，评估大语言模型在自动形式化中生成形式证明的鲁棒性，发现自然语言表述的微小变化会显著影响模型输出。
2026-06-03 cs.CL cs.LO
Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models
本文扩展了我们的实时的【形】Maude形式化的平面托勒密II离散事件（DE）模型的语义层次模型，包括模态模型。这是一项具有挑战性的任务，需要将同步定点计算与分层结构相结合。从Ptolemy II DE模型合成一个实时的【形】Maude验证模型，并在实时的【形】Maude中对合成模型进行形式化验证，这些都已集成到Ptolemy II中，从而实现了将Ptolemy II DE建模和仿真的便利性与实时的【形】Maude中的形式化验证相结合的模型工程过程。
2010-09-22 cs.FL cs.LO cs.PL
A vector logic for intensional formal semantics
Center for Possible Minds（可能心智中心）；Indiana University（印第安纳大学）
本文提出一种张量逻辑框架，用于处理意向性语义学中的形式与分布语义学的兼容性，通过线性算子和测度论方法实现语义函数的提升与模态算子的代数推导。
2026-09-22 cs.CL cs.FL cs.LO
Dist-Orc: A Rewriting-based Distributed Implementation of Orc with Formal Analysis
Orc是一种服务编排理论，允许分布式和定时计算的结构化编程。已经提出了几种形式语义的Orc，包括重写逻辑语义的作者开发的。Orc在Java中也有一个完全成熟的实现，具有函数式编程特性。然而，与大多数分布式语言的描述一样，Orc的形式语义和其实现之间存在相当大的差距，因为：（i）Orc中的程序不容易仅通过使用Orc的形式语义在分布式实现中部署，以及（ii）它们不容易在分布式Orc实现的级别上进行形式分析。在这项工作中，我们克服了Orc的问题（i）和（ii）。具体来说，我们描述了一种基于重写逻辑和Maude的实现技术，大大缩小了这一差距。这种技术的启用特性是Maude通过TCP套接字支持外部对象。我们描述了如何使用套接字来实现Orc站点调用和返回，并为Orc表达式和站点提供实时定时信息。然后，我们将展示如何在所得到的分布式实现的Orc程序可以正式分析在一个合理的抽象层次，通过定义一个抽象的时间模型和套接字通信基础设施，并讨论的假设下，分析可以被认为是正确的。最后，通过一个实例说明了分布式实现和形式化分析方法。
2010-09-22 cs.DC cs.LO cs.PL
