論文の概要: Automated Verification of Equivalence Properties in Advanced Logic Programs -- Bachelor Thesis
- arxiv url: http://arxiv.org/abs/2310.19806v4
- Date: Wed, 17 Jul 2024 10:23:59 GMT
- ステータス: 処理完了
- システム内更新日: 2024-07-18 23:18:25.751147
- Title: Automated Verification of Equivalence Properties in Advanced Logic Programs -- Bachelor Thesis
- Title（参考訳）: 先進論理プログラムにおける等価性の自動検証 -- Bachelor Thesis
- Authors: Jan Heuer,
- Abstract要約: 最適化されたサブプログラムが元のサブプログラムを置き換えることができるかどうかを自動的に検証できるツールを持つことが望ましい。
そのため、翻訳ツールのアンセムが開発された。
2つのプログラムが強い同値であることを検証するために、古典論理のための自動定理証明器と併用することができる。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: With the increase in industrial applications using Answer Set Programming, the need for formal verification tools, particularly for critical applications, has also increased. During the program optimisation process, it would be desirable to have a tool which can automatically verify whether an optimised subprogram can replace the original subprogram. Formally this corresponds to the problem of verifying the strong equivalence of two programs. In order to do so, the translation tool anthem was developed. It can be used in conjunction with an automated theorem prover for classical logic to verify that two programs are strongly equivalent. With the current version of anthem, only the strong equivalence of positive programs with a restricted input language can be verified. This is a result of the translation $\tau^*$ implemented in anthem that produces formulas in the logic of here-and-there, which coincides with classical logic only for positive programs. This thesis extends anthem in order to overcome these limitations. First, the transformation $\sigma^*$ is presented, which transforms formulas from the logic of here-and-there to classical logic. A theorem formalises how $\sigma^*$ can be used to express equivalence in the logic of here-and-there in classical logic. Second, the translation $\tau^*$ is extended to programs containing pools. Another theorem shows how $\sigma^*$ can be combined with $\tau^*$ to express the strong equivalence of two programs in classical logic. With $\sigma^*$ and the extended $\tau^*$, it is possible to express the strong equivalence of logic programs containing negation, simple choices, and pools. Both the extended $\tau^*$ and $\sigma^*$ are implemented in a new version of anthem. Several examples of logic programs containing pools, negation, and simple choice rules, which the new version of anthem can translate to classical logic, are presented. Some a...
- Abstract（参考訳）: アンサー・セット・プログラミングを用いた産業用アプリケーションの増加に伴い、特に重要なアプリケーションにおいて、正式な検証ツールの必要性も高まっている。
プログラム最適化プロセスの間は、最適化されたサブプログラムが元のサブプログラムを置き換えることができるかどうかを自動的に検証できるツールを持つことが望ましい。
形式的には、2つのプログラムの強い同値性を検証する問題に対応する。
そのため、翻訳ツールのアンセムが開発された。
2つのプログラムが強い同値であることを検証するために、古典論理のための自動定理証明器と併用することができる。
現行のアンセムでは、制限された入力言語を持つ正のプログラムの強い等価性しか検証できない。
これは、ここで論理式を生成するアンセムで実装された翻訳$\tau^*$の結果であり、これは正のプログラムに対してのみ古典論理と一致する。
この論文は、これらの制限を克服するために国歌を拡張している。
まず、変換 $\sigma^*$ が提示され、ここでの論理から古典論理へ公式を変換する。
定理は、$\sigma^*$ が古典論理学のここでの論理における同値性を表現するのにどのように使用できるかを定式化する。
第二に、$\tau^*$はプールを含むプログラムに拡張される。
別の定理は、$\sigma^*$を$\tau^*$と組み合わせて古典論理学における2つのプログラムの強い同値性を表現する方法を示している。
$\sigma^*$ と拡張 $\tau^*$ では、否定や単純な選択、プールを含む論理プログラムの強い等価性を表現できる。
拡張された $\tau^*$ と $\sigma^*$ は、アンセムの新バージョンで実装されている。
アンセムの新しいバージョンが古典論理に翻訳できるプール、否定、簡単な選択規則を含む論理プログラムのいくつかの例を示す。
いくつか...
関連論文リスト
- Faithful Logical Reasoning via Symbolic Chain-of-Thought [39.94884827166363]
シンボリック表現と論理規則をChain-of-Thoughtプロンプトと統合するフレームワークであるSymbCoTを提案する。
我々は、SymbCoTがCoT法よりも大幅に改善されていることを示す。
これは、論理的推論のために記号表現と規則をCoTに結合する最初の方法である。
論文 参考訳（メタデータ） (2024-05-28T16:55:33Z) - Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
我々は、LMコード駆動推論を改善するシンプルながら驚くほど効果的な拡張であるChain of Codeを提案する。
キーとなるアイデアは、プログラム内のセマンティックなサブタスクを、インタープリタが明示的にキャッチできるフレキシブルな擬似コードとしてフォーマットすることを、LMに促すことである。
論文 参考訳（メタデータ） (2023-12-07T17:51:43Z) - LINC: A Neurosymbolic Approach for Logical Reasoning by Combining
Language Models with First-Order Logic Provers [60.009969929857704]
論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。
本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。
我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
論文 参考訳（メタデータ） (2023-10-23T17:58:40Z) - Empower Nested Boolean Logic via Self-Supervised Curriculum Learning [67.46052028752327]
大規模言語モデルを含む事前学習された言語モデルは、多言語論理に直面するランダムセレクタのように振る舞う。
この基本的能力で言語モデルを強化するために,本稿では,新たな自己教師付き学習手法であるtextitCurriculum Logical Reasoning (textscClr) を提案する。
論文 参考訳（メタデータ） (2023-10-09T06:54:02Z) - Normative Conditional Reasoning as a Fragment of HOL [0.0]
本稿では(参照に基づく)条件付き規範推論の機械化について論じる。
我々の焦点は条件付き義務のためのAqvistのシステムEとその拡張である。
フレームワークの2つの可能性について検討する。
論文 参考訳（メタデータ） (2023-08-21T12:47:30Z) - Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical
Perspective [1.160208922584163]
順序ディジャンクション付き論理プログラム (LPOD) は古典論理プログラムを拡張し、優先ディジャンクションを表現できる。
本稿では,4値論理の論理等価性としてLPODの強い等価性を純粋に論理的に評価する。
LPODに対する強同値のcoNP完全性の新たな証明を提供するが、これはプログラムの特別な構造に依存しているため、それ自体が興味を持つ。
論文 参考訳（メタデータ） (2022-05-10T13:33:32Z) - Verification of Locally Tight Programs [8.005641341294732]
プログラム完了は、論理プログラムの言語から一階理論の言語への変換である。
この定理の厳密性条件は、より制限の少ない「局所的厳密性」要件に置き換えることができることを示す。
証明アシスタントAnthem-p2pは、局所的に密なプログラム間の等価性を検証できると結論付ける。
論文 参考訳（メタデータ） (2022-04-18T23:22:54Z) - An Extensible Logic Embedding Tool for Lightweight Non-Classical
Reasoning [91.3755431537592]
論理埋め込みツールは、古典的でない推論問題を古典的な高階論理にプロシージャエンコーディングする。
推論ターゲットとして、多くの非古典論理をサポートすることができる。
論文 参考訳（メタデータ） (2022-03-23T12:08:51Z) - A Logic-Based Framework for Natural Language Inference in Dutch [1.0178220223515955]
オランダ語文ペア間の関係を導出するための枠組みを提案する。
提案するフレームワークは、推論ラベルにつながる検査可能な証明を生成するために、論理ベースの推論に依存している。
我々は最近作成されたオランダの自然言語推論データセットの推論パイプラインを評価する。
論文 参考訳（メタデータ） (2021-10-07T10:34:46Z) - Logic-Driven Context Extension and Data Augmentation for Logical
Reasoning of Text [65.24325614642223]
論理的な記号や表現をテキストで理解し、答えにたどり着くよう提案します。
このような論理的情報に基づいて,文脈拡張フレームワークとデータ拡張アルゴリズムを提案する。
本手法は最先端の性能を実現し,論理駆動コンテキスト拡張フレームワークとデータ拡張アルゴリズムの両方が精度向上に寄与する。
論文 参考訳（メタデータ） (2021-05-08T10:09:36Z) - Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
本稿では,意図的および拡張的クラス数$lambda$-free高階論理に対して,難解な完全重ね合わせ計算を導入する。
計算は完全単調でなくてもよい項順でパラメタ化され、$lambda$フリーの高次語彙パスとKnuth-Bendixの順序を使うことができる。
論文 参考訳（メタデータ） (2020-05-05T12:10:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。