Stream: Beginner Questions

Topic: First-order logic on graphs

view this post on Zulip Robert Soeldner (Apr 29 2021 at 19:06):

Hi, I want to formalize first-order logic on graphs (see ;Section 3) using a deep embedding. I started reading "Concrete Semantics" by Nipkow and Klein followed by "Certifying Machine Code Safety: Shallow versus Deep Embedding" by Wildmoser and Nipkow and recently found a techn. report by Volker "A Deep Embedding of ZC in Isabelle/HOL" ( in which De Bruijn terms are used. Based on my limited understanding, this approach makes much sense to represent my logic, so-far . Any thoughts\guidance\comments would be highly appreciated.

Last updated: Sep 25 2021 at 08:21 UTC