Faithful Logic Embeddings in HOL — A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level

要約

古典的な高次ロジックにおける非古典的なロジックの深く浅い埋め込みは、近年、さまざまな自動化された推論ツールで調査、実装、および使用されています。
このペーパーでは、古典的な高次ロジックにおける、さまざまな形式の深い形状と浅い埋め込みの同時展開のレシピを紹介します。メタとオブジェクトレベルでの柔軟なインタラクティブで自動化された定理的発見だけでなく、論理埋め込みの間の自動化された忠実さの証拠も可能になります。
このアプローチは、論理教育、研究、応用に実り多いもので、ここでは、単純な命題モーダルロジックを使用して意図的に説明されています。
ただし、提示された作業は本質的に概念的であり、このような単純なロジックコンテキストに限定されません。

要約(オリジナル)

Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various automated reasoning tools in recent years. This paper presents a recipe for the simultaneous deployment of different forms of deep and shallow embeddings in classical higher-order logic, enabling not only flexible interactive and automated theorem proving and counterexample finding at meta and object level, but also automated faithfulness proofs between the logic embeddings. The approach, which is fruitful for logic education, research and application, is deliberately illustrated here using simple propositional modal logic. However, the work presented is conceptual in nature and not limited to such a simple logic context.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google