计算机科学中的逻辑

• 新提交
• 交叉列表
• 替换

查看 最近的 文章

显示 2025年07月10日， 星期四 新的列表

新提交 (展示 2 之 2 条目 )

[1] arXiv:2507.06804 [中文pdf, pdf, 其他]

标题： 通过解耦推理和证明解决更具挑战性的IMO问题 显示英文标题

标题： Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, Dong Yu

评论： 进行中

主题： 计算机科学中的逻辑 (cs.LO) ; 人工智能 (cs.AI)

自动定理证明（ATP）在形式语言中是人工智能的基础性挑战。 尽管大型语言模型（LLMs）推动了显著的进步，但它们强大的非正式推理能力与其薄弱的形式证明性能之间仍存在显著差距。 最近的研究表明，在像PutnamBench这样的基准测试中，非正式准确性超过80%，而形式成功性仍低于8%。 我们认为这一差距持续存在是因为当前最先进的证明器通过紧密耦合推理和证明，使用了无意中惩罚深度推理而偏向浅层、策略导向的策略的训练范式。 为了弥合这一根本性差距，我们提出了一种新的框架，将高层推理与低层证明生成解耦。 我们的方法利用两个不同的、专门的模型：一个强大且通用的推理器用于生成多样化的、战略性的子目标引理，以及一个高效的证明器用于严格验证它们。 这种模块化设计释放了模型的全部推理潜力，并避开了端到端训练的陷阱。 我们在一组2000年后的国际数学奥林匹克竞赛（IMO）问题上评估了我们的方法，这是一个之前没有任何开源证明器报告成功的题目集。 我们的解耦框架成功解决了其中的5个问题，展示了在应对极其困难的数学挑战方面自动化推理的重要进展。 为了促进未来的研究，我们发布了生成和验证的引理的完整数据集，适用于各种IMO问题，可在https://tencent-imo.github.io/ 获取。 显示英文摘要

Automated Theorem Proving (ATP) in formal languages is a foundational challenge for AI. While Large Language Models (LLMs) have driven remarkable progress, a significant gap remains between their powerful informal reasoning capabilities and their weak formal proving performance. Recent studies show that the informal accuracy exceeds 80% while formal success remains below 8% on benchmarks like PutnamBench. We argue this gap persists because current state-of-the-art provers, by tightly coupling reasoning and proving, are trained with paradigms that inadvertently punish deep reasoning in favor of shallow, tactic-based strategies. To bridge this fundamental gap, we propose a novel framework that decouples high-level reasoning from low-level proof generation. Our approach utilizes two distinct, specialized models: a powerful, general-purpose Reasoner to generate diverse, strategic subgoal lemmas, and an efficient Prover to rigorously verify them. This modular design liberates the model's full reasoning potential and bypasses the pitfalls of end-to-end training. We evaluate our method on a challenging set of post-2000 IMO problems, a problem set on which no prior open-source prover has reported success. Our decoupled framework successfully solves 5 of these problems, demonstrating a significant step towards automated reasoning on exceptionally difficult mathematical challenges. To foster future research, we release our full dataset of generated and verified lemmas for a wide range of IMO problems, available at https://tencent-imo.github.io/ .

[2] arXiv:2507.06854 [中文pdf, pdf, html, 其他]

标题： 证明论的连通逻辑C的函数完备性 显示英文标题

标题： Proof-Theoretic Functional Completeness for the Connexive Logic C

Sara Ayhan, Hrafn Valtýr Oddsson

评论： 对于已发表的版本，请参见 https://rdcu.be/evpKb

期刊参考： 逻辑学研究（在线发布日期：2025年7月8日）

主题： 计算机科学中的逻辑 (cs.LO) ; 逻辑 (math.LO)

我们通过使用一种已建立的方法，仅采用纯粹的证明论概念，展示了非平凡否定不一致逻辑C的联结词的功能完备性。 首先，考虑到C包含一个强否定，表达了直接反驳的概念，证明需要以双元论的方式进行，即不仅需要考虑证明的高阶规则模式，还需要考虑反驳的高阶规则模式。 其次，考虑到C是一种关联逻辑，我们需要以关联的方式理解推理作为基础，这导致了与通常使用的不同的（高阶）反驳概念。 显示英文摘要

We show the functional completeness for the connectives of the non-trivial negation inconsistent logic C by using a well-established method implementing purely proof-theoretic notions only. Firstly, given that C contains a strong negation, expressing a notion of direct refutation, the proof needs to be applied in a bilateralist way in that not only higher-order rule schemata for proofs but also for refutations need to be considered. Secondly, given that C is a connexive logic we need to take a connexive understanding of inference as a basis, leading to a different conception of (higher-order) refutation than is usually employed.

交叉提交 (展示 2 之 2 条目 )

[3] arXiv:2507.06383 (交叉列表自 eess.SY) [中文pdf, pdf, 其他]

标题： 外汇交易机器人使用模糊逻辑 显示英文标题

标题： Forex Trading Robot Using Fuzzy Logic

Mustafa Shabani, Alireza Nasiri, Hassan Nafardi

主题： 系统与控制 (eess.SY) ; 计算工程、金融与科学 (cs.CE) ; 计算机科学中的逻辑 (cs.LO)

在本研究中，我们提出了一种模糊系统，用于进行外汇市场的短期交易。 该系统旨在通过模糊逻辑增强外汇市场中的常见策略，从而提高交易的准确性。 传统上，基于振荡器指标的技术策略依赖于相对强弱指数（RSI）、商品通道指标（CCI）和随机指标等指标的预定义范围来确定交易的入场点。 然而，由于市场随时间变化的特性，这些经典指标的使用已产生了次优的结果。 在我们提出的方法中，我们没有采用经典指标，而是为每个指标引入了一个模糊Mamdani系统。 然后通过投票将这些系统的结果结合起来，设计一个交易机器人。 我们的研究结果表明，与三种其他方法相比，盈利能力因素有了显著增加。 此外，所有方法的净收益、总收益和最大资本减少都被计算并进行了比较。 显示英文摘要

In this study, we propose a fuzzy system for conducting short-term transactions in the forex market. The system is designed to enhance common strategies in the forex market using fuzzy logic, thereby improving the accuracy of transactions. Traditionally, technical strategies based on oscillator indicators have relied on predefined ranges for indicators such as Relative Strength Index (RSI), Commodity Channel Indicator (CCI), and Stochastic to determine entry points for trades. However, the use of these classic indicators has yielded suboptimal results due to the changing nature of the market over time. In our proposed approach, instead of employing classical indicators, we introduce a fuzzy Mamdani system for each indicator. The results obtained from these systems are then combined through voting to design a trading robot. Our findings demonstrate a considerable increase in the profitability factor compared to three other methods. Additionally, net profit, gross profit, and maximum capital reduction are calculated and compared across all approaches.

[4] arXiv:2507.06834 (交叉列表自 math.LO) [中文pdf, pdf, html, 其他]

标题： 直觉主义模态逻辑的基域扩展语义学 显示英文标题

标题： Base-extension Semantics for Intuitionistic Modal Logics

Yll Buzoku, David. J. Pym

评论： 21页

主题： 逻辑 (math.LO) ; 计算机科学中的逻辑 (cs.LO)

直觉主义模态逻辑的证明论和语义学由辛普森通过Prawitz风格的标记自然演绎系统和克里普克模型进行研究。 模型论语义学的一种替代方法是证明论语义学，这是一种推理主义的逻辑实现，在这种实现中，构造的意义是通过其使用来理解的。 证明论语义学的关键思想是原子规则的基，所有这些规则仅涉及命题原子，且不涉及任何逻辑连接词。 一种特定形式的证明论语义学，称为基扩展语义学（B-eS），关注公式的有效性，并提供了一个与克里普克模型直接对应的语义学，该语义学以基中原子公式的可证性为基础。 我们系统地建立了辛普森的直觉主义模态逻辑的B-eS，并且系统地获得了相对于辛普森自然演绎系统的可靠性和完全性定理。 显示英文摘要

The proof theory and semantics of intuitionistic modal logics have been studied by Simpson in terms of Prawitz-style labelled natural deduction systems and Kripke models. An alternative to model-theoretic semantics is provided by proof-theoretic semantics, which is a logical realization of inferentialism, in which the meaning of constructs is understood through their use. The key idea in proof-theoretic semantics is that of a base of atomic rules, all of which refer only to propositional atoms and involve no logical connectives. A specific form of proof-theoretic semantics, known as base-extension semantics (B-eS), is concerned with the validity of formulae and provides a direct counterpart to Kripke models that is grounded in the provability of atomic formulae in a base. We establish, systematically, B-eS for Simpson's intuitionistic modal logics and, also systematically, obtain soundness and completeness theorems with respect to Simpson's natural deduction systems.

替换提交 (展示 3 之 3 条目 )

[5] arXiv:2501.13603 (替换) [中文pdf, pdf, html, 其他]

标题： 在分离逻辑中验证图算法：代数方法的案例（扩展版本） 显示英文标题

标题： Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)

Marcos Grandury, Aleksandar Nanevski, Alexander Gryzlov

期刊参考： 程序设计语言协会论文集 9，ICFP，文章241（2025年8月）

主题： 计算机科学中的逻辑 (cs.LO) ; 编程语言 (cs.PL)

验证图算法在分离逻辑中一直被认为具有挑战性，主要是由于图子组件之间的结构共享。 我们表明，通过将图表示为部分交换独异幂等半群（PCM），并利用保持结构的函数（PCM同态），包括高阶组合器，可以有效地解决这些挑战。 PCM同态很重要，因为它们推广了分离逻辑中的局部推理原则。 虽然传统的框架仅在规范的顶层隔离堆的相关部分，但同态允许上下文定位：它们在独异幂等半群操作上分布，以隔离相关子图，即使嵌套在规范的深层中。 我们通过两个经典图基准的新颖且简洁的验证来展示同态的有效性：Schorr-Waite图标记算法和并查集数据结构。 显示英文摘要

Verifying graph algorithms has long been considered challenging in separation logic, mainly due to structural sharing between graph subcomponents. We show that these challenges can be effectively addressed by representing graphs as a partial commutative monoid (PCM), and by leveraging structure-preserving functions (PCM morphisms), including higher-order combinators. PCM morphisms are important because they generalize separation logic's principle of local reasoning. While traditional framing isolates relevant portions of the heap only at the top level of a specification, morphisms enable contextual localization: they distribute over monoid operations to isolate relevant subgraphs, even when nested deeply within a specification. We demonstrate the morphisms' effectiveness with novel and concise verifications of two canonical graph benchmarks: the Schorr-Waite graph marking algorithm and the union-find data structure.

[6] arXiv:2504.15645 (替换) [中文pdf, pdf, html, 其他]

标题： SMT与实数上的函数方程求解：来自IMO的挑战 显示英文标题

标题： SMT and Functional Equation Solving over the Reals: Challenges from the IMO

Chad E. Brown, Karel Chvalovský, Mikoláš Janota, Mirek Olšák, Stefan Ratschan

主题： 计算机科学中的逻辑 (cs.LO)

我们使用SMT技术来解决涉及未解释函数和非线性实数算术的一类问题。 特别是，我们关注在数学竞赛中常见的问题，例如国际数学奥林匹克竞赛（IMO），其中任务是确定对未解释函数的约束的所有解。 尽管这些问题只需要高中水平的数学知识，但最先进的SMT求解器通常会遇到困难。 我们提出几种技术来提高在此情境下的SMT性能。 显示英文摘要

We use SMT technology to address a class of problems involving uninterpreted functions and nonlinear real arithmetic. In particular, we focus on problems commonly found in mathematical competitions, such as the International Mathematical Olympiad (IMO), where the task is to determine all solutions to constraints on an uninterpreted function. Although these problems require only high-school-level mathematics, state-of-the-art SMT solvers often struggle with them. We propose several techniques to improve SMT performance in this setting.

[7] arXiv:2507.05519 (替换) [中文pdf, pdf, html, 其他]

标题： 用s(CASP)目标导向谓词答案集编程系统对(义务)模态算子进行建模 显示英文标题

标题： Modeling (Deontic) Modal Operators With the s(CASP) Goal-directed Predicate Answer Set Programming System

Gopal Gupta, Abhiramon Rajasekharan, Alexis R. Tudor, Elmer Salazar, Joaquín Arias

主题： 人工智能 (cs.AI) ; 计算机科学中的逻辑 (cs.LO)

我们考虑实现义务模态逻辑的问题。 我们展示如何使用默认否定（失败否定）和强否定来优雅地表达（义务）模态算子，这些在答案集编程（ASP）中存在。 我们建议使用ASP的全局约束来表示义务模态逻辑中的义务和禁止。 我们表明，我们提出的表示方法能够优雅地解决义务模态逻辑的各种悖论。 显示英文摘要

We consider the problem of implementing deontic modal logic. We show how (deontic) modal operators can be expressed elegantly using default negation (negation-as-failure) and strong negation present in answer set programming (ASP). We propose using global constraints of ASP to represent obligations and impermissibilities of deontic modal logic. We show that our proposed representation results in the various paradoxes of deontic modal logic being elegantly resolved.