首页/论文/2310.04090

arXiv 2310.040902023-10-06cs.LO

一种针对构造演算中数学日常语言的证明综合算法

A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions

Gilles Dowek

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

AI总结：

本研究提出了一种针对构造演算的可终止非完全证明综合方法，并基于该方法构建了构造演算的完全日常语言。

摘要：

我们提出了一种针对构造演算的非完全证明综合方法，该方法总是可终止的；还基于此方法提出了一种针对构造演算的完全日常语言。

英文摘要：

We present an incomplete proof synthesis method for the Calculus of Constructions which is always terminating and a complete Vernacular for the Calculus of Constructions based on this method.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

在可实现性假设下利用超位置的合成完备性

Completeness of Synthesis under Realizability Assumptions using Superposition

TU Wien（维也纳工业大学）

本文研究了在可实现性假设下利用超位置进行程序合成的完备性问题，通过改进超位置演算并证明其正确性和完备性，确保能够找到满足规范的可计算程序。

2026-05-19cs.LO

能量μ演算：ω-正则能量博弈的符号不动点算法

Energy mu-Calculus: Symbolic Fixed-Point Algorithms for omega-Regular Energy Games

$ω$-常规能量游戏，这是加权的两个玩家回合制游戏的定量目标，以保持能量水平非负，已被用于验证和合成的上下文中。模态$μ$-演算的逻辑，当应用于具有$ω$-正则获胜条件的博弈图时，允许以定点公式的形式定义用于计算获胜状态集的符号算法。在本文中，我们介绍了能量$μ$-演算，多值扩展的$μ$-演算，作为一个符号框架解决$ω$-经常能源游戏。能量$μ$-演算使现有的，众所周知的符号$μ$-演算算法的无缝重用$ω$-常规游戏，以解决其相应的能量增强的变种。我们定义的语法和语义的能量$μ$-演算的符号表示的游戏图，并展示了如何使用它来解决决策和最小信用问题的$ω$-定期能源游戏，有界和无界的能量水平的积累。

2020-10-18cs.LO

Tableau演算的自动合成

Automated Synthesis of Tableau Calculi

本文提出了一种合成声音和完整画面的方法。给定逻辑的形式语义的规范，该方法生成一组可用于在逻辑内推理的tableau推理规则。该方法保证生成的规则形成一个演算，这是健全的和建设性的完整。如果逻辑可以被证明允许有限过滤相对于一个定义良好的一阶语义，然后添加一个通用的阻塞机制提供了一个终止表演算。生成tableau规则的过程可以完全自动化，并且与阻塞机制一起产生用于生成tableau决策过程的自动化过程。为了说明，我们显示的描述逻辑与传递角色和命题直觉逻辑的方法的可行性。

2012-04-23cs.LOcs.SC

关于通用性能评估与通用控制器综合

On Generalized Performance Evaluation and Generalized Controller Synthesis

College of Computer Science and Technology Nanjing University of Aeronautics and Astronautics（南京航空航天大学计算机科学与技术学院）

本文提出通用性能评估和通用控制器综合的框架，通过并发过程演算建模系统，并提出一个具有格值的性能评估语言作为系统性能规范。文章展示了计算机科学中的几个问题是通用性能评估的特例，并给出了通用性能评估算法。同时，提出通用控制器综合的框架，作为通用性能评估的逆问题，并展示了计算机科学中的几个特例，概述了通用控制器综合算法。

2026-07-14cs.LOcs.PFcs.SY

基于定理综合的直觉主义命题逻辑中的溯因推理

Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis

借助一个紧凑的Prolog为基础的定理证明直觉命题逻辑，我们合成的最小假设下，一个给定的公式公式成为一个定理。应用我们的合成算法，以涵盖基本的溯因推理机制后，我们合成的字面量，模仿行的真值表在经典或中间逻辑和我们的条件假设，把经典或中间逻辑的定理，在直觉逻辑。更进一步，我们推广我们的溯因推理机制，合成更有表现力的前置条件，使用最小的一组规范公式，在微积分中的任意公式可以减少，同时保持其可证明性。组织作为一个独立的文学Prolog程序，本文支持其内容的交互式探索，并确保我们的结果完全可复制。

2022-05-11cs.LO

更多相关论文收起更多论文

环境友好型GR（1）合成

Environmentally-friendly GR(1) Synthesis

反应合成中的许多问题使用两个公式-环境假设和系统保证-来陈述，并且要求在满足其假设的环境中满足保证的实现。反应式合成工具通常通过主动防止环境假设成立来产生正式满足这些规范的策略。虽然形式上是正确的，但这些策略并没有抓住设计者的意图。我们在反应合成中引入了一个额外的要求，即非冲突性，它要求系统策略应该总是允许环境满足其活性要求。我们给出了一个求解GR（1）综合的算法，该算法产生不冲突的策略。我们的算法是由$μ$ -演算中的一个4-套不动点给出的，与GR（1）通常的3-套不动点不同。我们的算法确保，在每一个环境中，满足其自身的假设，所产生的实现的痕迹满足的假设和保证。此外，我们的算法的渐近复杂性是相同的，通常的GR（1）的解决方案。我们已经实现了我们的算法，并显示其性能相比，通常的GR（1）合成算法。

2019-02-14cs.LO

浅电路的相位小工具综合

Phase Gadget Synthesis for Shallow Circuits

我们给出了一个概述的电路优化方法使用的tket，编译系统的量子软件开发的剑桥量子计算有限公司，我们专注于一种新的技术，基于周围的相位小工具，一个家庭的多量子比特量子操作自然发生在广泛的量子线路的实际利益。相位小工具在ZX演算中有一个简单的表示，这使得它们很容易推理。利用这一点，我们提出了一种有效的方法，将相位小工具转换回CNOT门和适合在量子计算机上执行的单量子位操作，从而显着减少门数和电路深度。我们证明了这些方法的有效性的量子化学基准集的基础上变分电路的小分子的基态估计。

2020-05-01cs.LOquant-ph

简单不动点迭代法求解奇偶对策

Simple Fixpoint Iteration To Solve Parity Games

解决μ演算的模型检查问题的一种简单方法是使用不动点迭代。然而，传统上μ演算模型检查是通过将线性时间减少到奇偶博弈来解决的，然后使用奇偶博弈的许多算法之一来解决。我们现在考虑一种通过朴素不动点迭代求解奇偶博弈的方法。文献中已经提出了几个奇偶博弈的不动点算法。在这项工作中，我们介绍了一种算法，依赖于分心的概念。这个想法是，这为理解平价博弈提供了一个新的视角。然后，我们表明，该算法实际上是相同的两个早期公布的不动点算法的奇偶校验游戏，因此，这些早期的算法是相同的。此外，我们修改我们的算法更新后，只部分重新计算更深的不动点更高的设置，并表明这种修改使一个简单的方法来获得获胜的策略。我们表明，由此产生的算法是简单的实现，并提供了良好的性能，在实际的奇偶游戏。我们经验证明，这使用来自模型检查，等价性检查和反应合成的游戏，并表明我们的不动点算法是最快的解决方案模型检查游戏。

2019-09-17cs.LO

有限域上度量时间约束Golog规划的控制器综合

Controller Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints

RWTH Aachen University（亚琛工业大学）

在实际机器人上执行Golog程序通常需要额外的步骤来考虑机器人平台的硬件或软件细节，这些细节可以被公式化为对程序的约束。这些约束通常是时间性的，指的是度量时间，并且需要对抽象Golog程序进行修改。我们描述了如何制定这样的约束的基础上的模态变量的情况演算。这些约束连接抽象程序与平台模型，我们使用时间自动机描述。我们表明，在有限域和完全已知的初始状态的程序，合成的控制器，满足约束，同时保持原程序的效果的问题可以减少到MTL合成。我们这样做是通过构建一个时间自动机的抽象程序和合成MTL控制器从这个自动机，平台模型和约束。我们证明，合成的控制器的执行轨迹是相同的原始程序，可能交错与平台相关的行动，他们满足所有的约束条件，并且它们具有相同的效果作为原始程序的痕迹。通过这样做，我们得到一个可判定的过程来合成一个控制器，满足规格，同时保留原始程序。

2021-02-19cs.AIcs.LO

运行时间防护罩的设计与优化反应综合

Specification and Optimal Reactive Synthesis of Run-time Enforcement Shields

具有偶发误差的系统（SSE）是一种控制器，它产生高质量的输出，但它可能偶尔违反一个关键的要求<$（I，O）。一个运行时间执行屏蔽是一个控制器，它把（I，O）（来自SSE）作为它的输入，它产生一个校正的输出O'，保证了需求I（I，O'）的不变性。此外，输出序列O'必须尽可能少地偏离O“以保持质量。本文给出了一种利用逻辑量化离散时间演算（QDDC）公式对屏蔽进行逻辑规范的方法。该规范包括一个正确性要求和一个硬偏差约束HDC，屏蔽必须强制和不变地满足这两个要求。此外，我们还使用定量优化给出了一个屏蔽，最大限度地减少了H-最优方式的累积偏差的期望值。我们展示了如何工具DCSynth实现软需求指导的合成可以用于自动合成屏蔽从给定的规范。接下来，我们给出逻辑公式，指定几个概念的盾牌，包括k-稳定盾牌的Bloem“等。以及Wu等人的突发错误屏蔽。“，和一个新的E，D-盾牌。使用DCSynth工具可以自动合成所有这些规格的屏蔽。我们给出的实验结果显示我们的屏蔽合成工具的性能与以前的工作。我们还比较了不同的硬偏差约束下合成的盾牌在其预期偏差和最坏情况下的突发偏差延迟的性能。

2019-09-17cs.FLcs.GTcs.LO

吸引缠结解奇偶博弈

Attracting Tangles to Solve Parity Games

奇偶博弈在形式化验证和综合中有重要的实际应用，特别是在解决模态μ演算的模型检验问题上。从理论的角度来看，它们也很有趣，因为它们被广泛认为是多项式解，但到目前为止还没有这样的算法。我们提出了一个新的算法来解决基于学习缠结，这是强连接的子图，其中一个玩家有一个策略，赢得所有的循环在子图的奇偶游戏。我们认为，缠结发挥了重要的作用，在突出的奇偶博弈求解算法。我们证明了缠结学习在实践中是有竞争力的，并且是大型随机游戏的最快求解器。

2018-04-14cs.GTcs.LO