Options
Faithful Logic Embeddings in HOL : Deep and Shallow
Benzmüller, Christoph (2025): Faithful Logic Embeddings in HOL : Deep and Shallow, in: Clark Barret, Uwe Waldmann, Clark Barret, u. a. (Hrsg.), Automated Deduction – CADE 30 : 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings, Cham: Springer Nature Switzerland, S. 280–301, doi: 10.1007/978-3-031-99984-0_16.
Faculty/Chair:
Author:
Title of the compilation:
Automated Deduction – CADE 30 : 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings
Editors:
Barret, Clark
Waldmann, Uwe
Conference:
CADE 30 : 30th International Conference on Automated Deduction, July 28-31, 2025 ; Stuttgart, Germany
Publisher Information:
Year of publication:
2025
Pages:
ISBN:
9783031999833
9783031999840
Language:
English
Abstract:
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.
Keywords: ; ;
Logic embeddings
Faithfulness
Automated Reasoning
Peer Reviewed:
Yes:
International Distribution:
Yes:
Type:
Conferenceobject
Activation date:
July 27, 2026
Versioning
Question on publication
Permalink
https://fis.uni-bamberg.de/handle/uniba/116345