4 citations · 4 across the 2 of their papers we have counts for
2 papers
cs.LO2026
Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)
Christoph Benzmueller, Daniel Kirchner
In Isabelle/HOL, we apply the deep-and-shallow embedding methodology of our prior work to monadic second-order logic (MSO). Three embeddings are developed side by side: a deep embe…
cs.AI2009★ 4 cited
Granularity-Adaptive Proof Presentation
Marvin Schiller, Christoph Benzmueller
When mathematicians present proofs they usually adapt their explanations to their didactic goals and to the (assumed) knowledge of their addressees. Modern automated theorem prover…