BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Faithful Logic Embeddings in HOL:  Deep and Shallow\, Propositiona
 l and Quantified - Christoph Benzmüller (Otto-Friedrich-Universität Bamb
 erg and Freie Universität Berlin)
DTSTART:20260312T170000Z
DTEND:20260312T180000Z
UID:TALK242896@talks.cam.ac.uk
CONTACT:Jonas Bayer
DESCRIPTION:Deep and shallow embeddings of numerous logic formalisms in cl
 assical higher-order logic have been explored\, implemented\, and used in 
 various reasoning tools in recent years. This paper presents a method for 
 the simultaneous provision of deep and shallow embeddings of various degre
 es (maximal/minimal) in classical higher-order logic. This enables flexibl
 e\, interactive and automated theorem proving and counterexample finding a
 t meta and object level\, as well as automated faithfulness proofs between
  these logic embeddings. The method is beneficial for logic education\, re
 search and application and is illustrated here initially using simple prop
 ositional modal logic. However\, the approach is conceptual in nature and 
 not limited to this simple logic context. For example\, it also supports q
 uantifiers. To illustrate this\, this paper additionally introduces deep a
 nd shallow embeddings of quantified Boolean formulas\, and\, maintaining a
  high degree of proof automation\, faithfulness between these embeddings i
 s proved using respective lemmata\, including a substitution lemma. This w
 ork demonstrates how mathematical proof assistant systems can facilitate t
 he exploration and rapid prototyping of formal logics. This is relevant no
 t only for formalisation of mathematical knowledge\, but also for the mech
 anisation of legal and normative reasoning and the encoding of foundationa
 l metaphysical theories\, for example.\n\nThe presented material significa
 ntly extents the work covered in the following two papers:\nChristoph Benz
 müller: Faithful Logic Embeddings in HOL - Deep and Shallow. CADE 2025: 2
 80-301. Doi: 10.1007/978-3-031-99984-0_16 (Preprint: arXiv:2502.19311)\nCh
 ristoph Benzmüller: Faithful Logic Embeddings in HOL - Deep and Shallow (
 Isabelle/HOL dataset). Arch. Formal Proofs 2025 (2025). https://www.isa-af
 p.org/entries/FaithfulPMLinHOL.html\n\n\n=== Online talk ===\n\nJoin Zoom 
 Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAm
 bXLO8HbY.1\n\nMeeting ID: 898 5609 1954 Passcode: ITPtalk
LOCATION:Online\; live-streamed at MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR