Faithful Logic Embeddings in HOL -- Deep and Shallow
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913869308362752 |
|---|---|
| author | Benzmüller, Christoph |
| author_facet | Benzmüller, Christoph |
| contents | Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic. This enables flexible, interactive and automated theorem proving and counterexample finding at meta and object level, as well as automated faithfulness proofs between these logic embeddings. The method is beneficial for logic education, research and application and is illustrated here using a simple propositional modal logic. However, this approach is conceptual in nature and not limited to this simple logic context. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_19311 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Faithful Logic Embeddings in HOL -- Deep and Shallow Benzmüller, Christoph Logic in Computer Science Artificial Intelligence Logic 03Axx, 03Bxx, 03B15, 68T15 F.4; I.2.3; I.2.4 Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic. This enables flexible, interactive and automated theorem proving and counterexample finding at meta and object level, as well as automated faithfulness proofs between these logic embeddings. The method is beneficial for logic education, research and application and is illustrated here using a simple propositional modal logic. However, this approach is conceptual in nature and not limited to this simple logic context. |
| title | Faithful Logic Embeddings in HOL -- Deep and Shallow |
| topic | Logic in Computer Science Artificial Intelligence Logic 03Axx, 03Bxx, 03B15, 68T15 F.4; I.2.3; I.2.4 |
| url | https://arxiv.org/abs/2502.19311 |