Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
この論文は、探索を迅速に行える手続き的な「apply スタイル」の証明スクリプトを、可読性と堅牢性に優れた宣言的な Isar 形式に自動的に変換するツール「Apply2Isar」を提案し、その有効性を Isabelle の形式証明アーカイブのデータセットを用いて実証したものである。
💻 Category
cs.LO
63 件の論文
The Unit Gap: How Sharing Works in Boolean Circuits
この論文は、AND と NOT を用いたブール回路において、回路サイズと論理式サイズの差が常に 0 または 1 であることを証明し、その差が 1 となる条件や共有の必要性に関する厳密な定理を確立したものである。
Step Automata
本論文は、従来のオートマトンやチューリングマシンを拡張し、並列性を考慮した「ステップオートマトン」と「ステップチューリングマシン（STM）」の概念を提案し、計算理論と並行処理の間の未解決のリンクを埋めることを目的としています。
Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
この論文は、Mathlib や PhysLib などの形式化ツールを用いて 2006 年の 2HDM ポテンシャル安定性に関する古典的な研究を Lean で再検証した結果、その主要定理を無効にする誤りが発見されたことを報告し、物理学論文の形式化による検証が初めて非自明な誤りを明らかにした事例としてその重要性を強調しています。
Central Limits via Dilated Categories
本論文は、中央極限定理を統一的に扱うための「拡大半ノルム付加圏」という新たな枠組みを提案し、古典的な定理の強化版から統計力学への応用までを含む抽象的な一般定理を確立したものである。
On the expressive power of inquisitive team logic and inquisitive first-order logic
本論文は、インクワイアティブ・チーム論理の開放式が第一階述語論理の表現力を真に超えること、およびその論理に依存論理の範囲生成普遍量化子を付加すれば有限性を表現可能となり非コンパクトかつ再帰的公理化不可能になることを示すとともに、標準的なインクワイアティブ第一階述語論理においても第一階述語論理では表現できないモデルの性質を記述する文が存在することを明らかにする。
Towards a Higher-Order Mathematical Operational Semantics
この論文は、Turi と Plotkin の抽象 GSOS 枠組みを高次言語へ拡張し、高次言語の操作意味論を「指向付き高次 GSOS 法則」として定式化することで、SKI 計算や計算などの高次言語における構成性の保証を可能にする一般理論を構築したものである。
Consistency-based Abductive Reasoning over Perceptual Errors of Multiple Pre-trained Models in Novel Environments
この論文は、新規環境における複数の事前学習済み知覚モデルの予測矛盾を、整合性に基づく帰納推論（アブダクション）として定式化し、論理的整合性を保ちつつ予測カバレッジを最大化する新しい枠組みを提案することで、単一モデルや標準的なアンサンブル手法を上回る頑健な性能を実現することを示しています。
A Graded Modal Type Theory for Pulse Schedules
この論文は、量子コンピュータの制御パルススケジュールを形式化するための「GRAMPUS」と呼ばれる、時間情報を格（grade）として表現するgraded 型理論を提案し、その構文、意味論、および完全性と健全性の定理を確立するものである。
The Skolem Problem in rings of positive characteristic
この論文は、Dong と Shafrir（2026 年）および Karimov ら（2025 年）の最近の結果に基づき、正標数の有限生成可換環における線形漸化式列のゼロ項存在判定問題（スキョレム問題）が決定可能であることを示しています。
WME: Extending CDCL-based Model Enumeration with Weights
この論文は、重み付きモデル列挙（WME）をソルバーレベルの推論タスクとして確立し、重み伝播や重みに基づく剪除を CDCL 型ソルバーに統合することで、時系列バックトラックと非時系列バックトラックの両方のアプローチが相互補完的に機能することを示しています。
A Formalization of Abstract Rewriting in Agda
この論文は、Agda 証明支援系を用いて抽象リライティングシステムを構成的に形式化し、古典論理の使用を排除・最小化することで終止性と合流性の標準的な結果を再検討・一般化し、ラムダ計算の形式化を通じてその実用性を示すものである。
Duality theory in linear optimization and its extensions -- formally verified
この論文は、Lean 4 において線形順序体上のファルカスの定理を形式的に証明し、係数に「無限大」を許容するケースへと双対性理論を拡張したことを報告しています。
Constraint satisfaction problems, compactness and non-measurable sets
この論文は、有限関係構造のコンパクト性が幅 1 の場合に ZF 公理系で証明可能である一方、それ以外の場合は 3 次元空間における非可測集合の存在を意味することを示しています。
A Topological Rewriting of Tarski's Mereogeometry
この論文は、依存型理論と Coq 証明支援系を用いてタルスキの幾何学を形式化する既存のライブラリ「lambda-MM」を拡張し、単なる部分集合論的枠組みからハウスドルフ空間を含む完全な位相空間を導出することで、タルスキの幾何学をその部分空間として再定式化し、理論の表現力を高めたものである。
Can LLM Aid in Solving Constraints with Inductive Definitions?
この論文は、構造化されたプロンプトを用いて大規模言語モデル（LLM）に帰納的定義の推論に必要な補助的な補題を生成させ、制約ソルバーと協調させるニューロ記号アプローチを提案し、その結果、SMT や CHC ソルバーの性能を約 25% 向上させて帰納的定義を含む証明タスクをより多く解決できることを示しています。
Model Change for Description Logic Concepts
この論文は、記述論理の概念をモデル（点付き解釈）に基づいて変更する「モデル変更」の問題を扱い、排除・受容・修正の 3 種類を定義し、修正が単なる排除と受容の組み合わせに還元できないことを示すとともに、EL および ALC 記述論理におけるこれらの操作の整合性に関する正負の結果を提示するものです。
Classical Explanations in (and of) General Probabilistic Theories
この論文は、確率モデルの圏におけるスパンとして「説明」を定義し、局所有限な確率モデルがすべて標準的な古典的説明（関手的な構成による）を持つことを示しています。
LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning
本論文は、自然言語の曖昧さから線形時相論理（LTL）仕様を生成する際、小規模な言語モデルの限界を克服するため、制約付き生成と軽量な形式的整合性チェックを組み合わせるモジュール型ツールチェーン「LTLGuard」を提案し、その有効性を示すものである。
Diagonalizing Through the -Chain: Iterated Self-Certification on Bounded Turing Machines and its Least Fixed Point
この論文は、有界なチューリング機械における自己検証の時間的オーバーヘッドという制約をドメイン理論の枠組みで定式化し、有限の観測からなる昇る-連鎖のスコット極限を通じて、停止問題の解決を「対角線論法の連続的な先送り」として捉える新たな視点を提供するものである。