論文の概要: Refining Labelled Systems for Modal and Constructive Logics with
Applications
- arxiv url: http://arxiv.org/abs/2107.14487v1
- Date: Fri, 30 Jul 2021 08:27:15 GMT
- ステータス: 処理完了
- システム内更新日: 2021-08-02 16:49:18.599455
- Title: Refining Labelled Systems for Modal and Constructive Logics with
Applications
- Title（参考訳）: モーダル論理と構成論理を応用したラベリングシステム
- Authors: Tim Lyon
- Abstract要約: この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。
精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。
導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This thesis introduces the "method of structural refinement", which serves as
a means of transforming the relational semantics of a modal and/or constructive
logic into an 'economical' proof system by connecting two proof-theoretic
paradigms: labelled and nested sequent calculi. The formalism of labelled
sequents has been successful in that cut-free calculi in possession of
desirable proof-theoretic properties can be automatically generated for large
classes of logics. Despite these qualities, labelled systems make use of a
complicated syntax that explicitly incorporates the semantics of the associated
logic, and such systems typically violate the subformula property to a high
degree. By contrast, nested sequent calculi employ a simpler syntax and adhere
to a strict reading of the subformula property, making such systems useful in
the design of automated reasoning algorithms. However, the downside of the
nested sequent paradigm is that a general theory concerning the automated
construction of such calculi (as in the labelled setting) is essentially
absent, meaning that the construction of nested systems and the confirmation of
their properties is usually done on a case-by-case basis. The refinement method
connects both paradigms in a fruitful way, by transforming labelled systems
into nested (or, refined labelled) systems with the properties of the former
preserved throughout the transformation process.
To demonstrate the method of refinement and some of its applications, we
consider grammar logics, first-order intuitionistic logics, and deontic STIT
logics. The introduced refined labelled calculi will be used to provide the
first proof-search algorithms for deontic STIT logics. Furthermore, we employ
our refined labelled calculi for grammar logics to show that every logic in the
class possesses the effective Lyndon interpolation property.
- Abstract（参考訳）: この論文は、モーダル論理および/または構成論理のリレーショナルセマンティクスを2つの証明論的パラダイム(ラベル付きと入れ子付きシークエント計算)を接続して「経済的な」証明システムに変換する手段として機能する「構造的洗練の方法」を導入する。
ラベル付きシークエントの定式化は、論理学の大規模なクラスに対して、望ましい証明理論的性質を持つカットフリーな計算を自動生成することに成功した。
これらの性質にもかかわらず、ラベル付きシステムは関連する論理のセマンティクスを明示的に組み込んだ複雑な構文を用いており、そのようなシステムは典型的にはサブフォーミュラ特性を高いレベルで侵害する。
対照的に、ネストされたシークエント計算はより単純な構文を採用し、サブフォーミュラ特性の厳密な読み取りに固執するので、そのようなシステムは自動推論アルゴリズムの設計に有用である。
しかし、ネストシークエントパラダイムの欠点は、そのような計算の自動化に関する一般的な理論(ラベル付きセッティングの場合のように)が本質的に欠落していることであり、ネスト系の構築とそれらの性質の確認はケースバイケースで行うのが普通である。
改質法は、2つのパラダイムを実りある方法で結合し、ラベリングされたシステムをネストされた(またはリベリングされた)システムに変換し、前者の特性を変換プロセスを通して保持する。
改良の方法とその応用を実証するために,文法論理,一階直観論理,非直観的STIT論理について考察する。
改良されたラベル付き計算は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使われる。
さらに、クラス内の全ての論理が有効なリンドン補間特性を持つことを示すため、文法論理に洗練されたラベル付き計算を用いる。
関連論文リスト
- Inferentialist Resource Semantics [48.65926948745294]
システムモデリングでは、システムは典型的にどのプロセスが実行されるかを示すリソースから構成される。
本稿では,リソースセマンティクスにおいて,推論が汎用的で表現力豊かなフレームワークを実現する方法を示す。
論文 参考訳（メタデータ） (2024-02-14T14:54:36Z) - An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
このアプローチは抽象弁証法フレームワークのコンピュータ支援分析を可能にする。
応用例としては、メタ理論的性質の形式的解析と検証がある。
論文 参考訳（メタデータ） (2023-12-08T09:32:26Z) - LOGICSEG: Parsing Visual Semantics with Neural Logic Learning and
Reasoning [73.98142349171552]
LOGICSEGは、神経誘導学習と論理推論をリッチデータとシンボリック知識の両方に統合する、全体論的視覚意味論である。
ファジィ論理に基づく連続的な緩和の間、論理式はデータとニューラルな計算グラフに基礎を置いており、論理によるネットワークトレーニングを可能にする。
これらの設計によりLOGICSEGは、既存のセグメンテーションモデルに容易に統合できる汎用的でコンパクトなニューラル論理マシンとなる。
論文 参考訳（メタデータ） (2023-09-24T05:43:19Z) - A Hybrid System for Systematic Generalization in Simple Arithmetic
Problems [70.91780996370326]
本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。
提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
論文 参考訳（メタデータ） (2023-06-29T18:35:41Z) - Investigating the Robustness of Natural Language Generation from Logical
Forms via Counterfactual Samples [30.079030298066847]
事前訓練されたモデルに基づく最先端の手法は、標準テストデータセットで顕著なパフォーマンスを達成した。
これらの手法が、テーブルのヘッダーと論理形式の演算子の間の急激な相関にのみ依存するのではなく、論理的推論を行う方法を学ぶかどうかを疑問視する。
本稿では,ショートカットへの依存を減らすための2つのアプローチを提案する。
論文 参考訳（メタデータ） (2022-10-16T14:14:53Z) - Differentiable Inference of Temporal Logic Formulas [1.370633147306388]
信号時相論理式を学習するための最初のリカレントニューラルネットワークアーキテクチャを実演する。
本稿では,式推論法の最初の体系的比較について述べる。
論文 参考訳（メタデータ） (2022-08-10T16:52:23Z) - Discourse-Aware Graph Networks for Textual Logical Reasoning [142.0097357999134]
パッセージレベルの論理関係は命題単位間の係り合いまたは矛盾を表す(例、結論文)
論理的推論QAを解くための論理構造制約モデリングを提案し、談話対応グラフネットワーク(DAGN)を導入する。
ネットワークはまず、インラインの談話接続とジェネリック論理理論を利用した論理グラフを構築し、その後、エッジ推論機構を用いて論理関係を進化させ、グラフ機能を更新することで論理表現を学習する。
論文 参考訳（メタデータ） (2022-07-04T14:38:49Z) - Modeling and Automating Public Announcement Logic with Relativized
Common Knowledge as a Fragment of HOL in LogiKEy [0.0]
本稿では,関連する共通知識を用いた発表ロジックのセマンティックな埋め込みについて述べる。
これにより、古典的な高階論理に対するオフ・ザ・シェルフ定理証明を用いて、この論理を初めて自動化することができる。
この研究は、複数派のLogiKEy知識工学方法論に重要な追加となる。
論文 参考訳（メタデータ） (2021-11-02T15:14:52Z) - Logic-Driven Context Extension and Data Augmentation for Logical
Reasoning of Text [65.24325614642223]
論理的な記号や表現をテキストで理解し、答えにたどり着くよう提案します。
このような論理的情報に基づいて,文脈拡張フレームワークとデータ拡張アルゴリズムを提案する。
本手法は最先端の性能を実現し,論理駆動コンテキスト拡張フレームワークとデータ拡張アルゴリズムの両方が精度向上に寄与する。
論文 参考訳（メタデータ） (2021-05-08T10:09:36Z) - Public Announcement Logic in HOL [0.0]
関連する共通知識を持つ公開告知論理のための浅層セマンティック埋め込みについて述べる。
この埋め込みにより、古典的な高階論理に対するオフ・ザ・シェルフ定理証明を用いて、この論理を初めて自動化することができる。
論文 参考訳（メタデータ） (2020-10-02T06:46:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。