論文の概要: Automated Verification of Equivalence Properties in Advanced Logic
Programs -- Bachelor Thesis
- arxiv url: http://arxiv.org/abs/2310.19806v1
- Date: Wed, 11 Oct 2023 08:19:22 GMT
- ステータス: 処理完了
- システム内更新日: 2023-11-05 13:42:38.879253
- 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^*$ はプールを含むプログラムに拡張される。
別の定理は、2つのプログラムの古典論理における強同値を表現するために、$\sigma^*$ と$\tau^*$ を組み合わせる方法を示している。
拡張された$\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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。