論文の概要: Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB
- arxiv url: http://arxiv.org/abs/2607.21191v1
- Date: Thu, 23 Jul 2026 11:16:32 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-24 18:26:25.383842
- Title: Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB
- Title（参考訳）: PrologにおけるEvent-B Proofルールのエンコード: ProBの対話型シーケントプロバー
- Abstract要約: Event-B は述語論理と集合論に根ざした形式的な方法である。
我々は600以上の証明ルールをPrologにエンコードし、体系的で理解可能な証明分析と構築を可能にした。
証明ルールを Prolog ベースの検証ツール ProB に統合することにより,証明木を視覚化した対話型証明システムを得る。
- 参考スコア（独自算出の注目度）: 0.2676349883103403
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Event-B is a formal method rooted in predicate logic and set theory. We encoded over 600 proof rules in Prolog, enabling a systematic, comprehensible proof analysis and construction. By integrating the proof rules into the Prolog-based validation tool ProB, we obtain an interactive proof system with proof tree visualisation. This has advantages in teaching, giving students direct control over the selection of proof rules. Our tool can import proof obligations from the Rodin platform and provides multiple exports: a trace file for proof replay in ProB, an interactive HTML document for tool-independent exploration of the proof tree, and an export back to Rodin, allowing the ProB prover to be used as second chain. Compared to the previous implementation of the proof rules in Java, the encoding in Prolog is more compact, maintainable and extensible. While a preliminary iterative deepening prover with simple heuristics is already available and useful for finding short proofs, we aim to obtain fast automatic provers in the future.
- Abstract（参考訳）: Event-B は述語論理と集合論に根ざした形式的な方法である。
我々は600以上の証明ルールをPrologにエンコードし、体系的で理解可能な証明分析と構築を可能にした。
証明ルールを Prolog ベースの検証ツール ProB に統合することにより,証明木を視覚化した対話型証明システムを得る。
これは、生徒に証明規則の選択を直接制御させるという、教育上の利点がある。
このツールはRodinプラットフォームから証明義務をインポートし,ProBの証明再生のためのトレースファイル,ツールに依存しない証明ツリー探索のためのインタラクティブHTMLドキュメント,Rodinへのエクスポートなど,複数のエクスポートを提供する。
Javaでの証明ルールの以前の実装と比較すると、Prologのエンコーディングはよりコンパクトで、保守性があり、拡張可能である。
簡単なヒューリスティックスを用いた予備的反復的深度証明器はすでに利用可能であり,短い証明を見つけるのに有用であるが,将来的には高速自動証明器の実現を目指している。
関連論文リスト
- Show Me The Money: An Exercise in Proof-Driven Software Understanding [1.678913049066618]
我々は、StellarブロックチェーンのSDEX注文ブックを実装するコアアルゴリズムの形式解析に重点を置いている。
コードの変更を既存の不変量に対して簡単にチェックできるように、アーティファクトを生成します。
この研究は、定理証明とモデル検査の戦略的組み合わせが、レガシーシステムに堅牢な保証を提供するための道を提供することを示す。
論文 参考訳（メタデータ） (2026-07-17T20:39:40Z) - OProver: A Unified Framework for Agentic Formal Theorem Proving [33.14658302112269]
OProverは、Lean 4.0で証明された代理的な形式的な反復定理のための統一されたフレームワークである。
エージェント証明を実行し、新たに証明された証明をOProofsと検索メモリにインデックスし、修理軌跡をSFTデータとして使用し、未解決のハードケースをRLに使用する。
OProver-32BはMiniF2F (93.3%)、ProverBench (58.2%)、PutnamBench (11.3%)で最高のパス@32を獲得し、MathOlympiad (22.8%)、ProofNet (33.2%)で上位にランクインしている。
論文 参考訳（メタデータ） (2026-05-17T06:39:05Z) - Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。
我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。
我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
論文 参考訳（メタデータ） (2026-03-13T01:33:20Z) - PBLean: Pseudo-Boolean Proof Certificates for Lean 4 [27.126691338850254]
PBLean は VeriPB pseudo-Boolean (PB) 証明証明書をLean 4 にインポートする手法である。
リーンで完全証明され、コンパイルされたネイティブコードとして実行されるブールチェッカー関数。
我々のチェッカーは、カットプレーンや証明・バイ・コントラディション・サブプロテクションを含む全てのVeriPBカーネルルールをサポートしている。
論文 参考訳（メタデータ） (2026-02-09T14:13:30Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations [14.748476989228214]
Proofrは、人間の監督を必要とせず、リーンの証明を単純化するために訓練された最初の言語モデルです。
Provrは専門家の反復と強化学習を通じてトレーニングされ、リーンを使って単純化の検証とトレーニング信号を提供する。
Provrは、最先端のRL訓練プローバーが標準ベンチマークで生成した証明を実質的に圧縮する。
論文 参考訳（メタデータ） (2025-10-17T14:45:30Z) - Hierarchical Attention Generates Better Proofs [8.676187819105298]
注意機構を数学的推論構造に整合させる正規化手法であるtextbfHierarchical Attention を導入する。
提案手法は,基礎要素から高レベル概念への5段階階層を確立し,証明生成における構造化情報の流れを確実にする。
論文 参考訳（メタデータ） (2025-04-27T10:35:05Z) - LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。
実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文 参考訳（メタデータ） (2025-02-25T07:46:36Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z) - Prove-It: A Proof Assistant for Organizing and Verifying General
Mathematical Knowledge [0.0]
Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。
Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。
現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
論文 参考訳（メタデータ） (2020-12-20T18:15:12Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。