home.social

#isabellehol — Public Fediverse posts

Live and recent posts from across the Fediverse tagged #isabellehol, aggregated by home.social.

  1. New and formalized proofs for right-forward closures and core matrix interpretations. ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. drops.dagstuhl.de/entities/doc #IsabelleHOL #ITP

  2. New and formalized proofs for right-forward closures and core matrix interpretations. ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. drops.dagstuhl.de/entities/doc #IsabelleHOL #ITP

  3. Termination restricted to right-forward closures (in Isabelle/HOL). ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. isa-afp.org/entries/Right_Forw #IsabelleHOL #ITP

  4. Termination restricted to right-forward closures (in Isabelle/HOL). ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. isa-afp.org/entries/Right_Forw #IsabelleHOL #ITP

  5. Conway's circle theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Conway_Cir #IsabelleHOL #ITP #Math

  6. Conway's circle theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Conway_Cir #IsabelleHOL #ITP #Math

  7. Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. isa-afp.org/entries/MSOinHOL.h #IsabelleHOL #ITP #Logic

  8. Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. isa-afp.org/entries/MSOinHOL.h #IsabelleHOL #ITP #Logic

  9. Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. isa-afp.org/entries/MSOinHOL.h #IsabelleHOL #ITP #Logic

  10. Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. isa-afp.org/entries/MSOinHOL.h #IsabelleHOL #ITP #Logic

  11. Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. isa-afp.org/entries/MSOinHOL.h #IsabelleHOL #ITP #Logic

  12. The Chevalley-Warning theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Chevalley_ #IsabelleHOL #ITP #Math

  13. The Chevalley-Warning theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Chevalley_ #IsabelleHOL #ITP #Math

  14. First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic

  15. First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic

  16. First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic

  17. First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic

  18. First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic

  19. Formalizing paradoxes in grounded arithmetic using Isabelle/HOL. ~ Ananthajit Srikanth, Bryan Ford. bford.info/pub/lang/paradox/pa #IsabelleHOL #ITP #Math

  20. Formalizing paradoxes in grounded arithmetic using Isabelle/HOL. ~ Ananthajit Srikanth, Bryan Ford. bford.info/pub/lang/paradox/pa #IsabelleHOL #ITP #Math

  21. Complete elliptic integrals and the arithmetic–geometric mean (in Isabelle/HOL). ~ Manuel Eberl. isa-afp.org/entries/Arithmetic #IsabelleHOL #ITP #Math

  22. Complete elliptic integrals and the arithmetic–geometric mean (in Isabelle/HOL). ~ Manuel Eberl. isa-afp.org/entries/Arithmetic #IsabelleHOL #ITP #Math

  23. Rademacher's series for the partition function (in Isabelle/HOL). ~ Manuel Eberl, Lawrence C. Paulson. isa-afp.org/entries/Rademacher #IsabelleHOL #ITP #Math

  24. Rademacher's series for the partition function (in Isabelle/HOL). ~ Manuel Eberl, Lawrence C. Paulson. isa-afp.org/entries/Rademacher #IsabelleHOL #ITP #Math

  25. Correctness and complexity of BMSSP in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/BMSSP_Corr #IsabelleHOL #ITP

  26. Correctness and complexity of BMSSP in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/BMSSP_Corr #IsabelleHOL #ITP

  27. Freiman's 3k - 4 theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Freiman_3k #IsabelleHOL #ITP #Math

  28. Freiman's 3k - 4 theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. isa-afp.org/entries/Freiman_3k #IsabelleHOL #ITP #Math

  29. Axiomatic theory of hereditarily finite sets and its fragments (in Isabelle/HOL). ~ Štěpán Holub, Zuzana Haniková. isa-afp.org/entries/ZF_finite. #IsabelleHOL #ITP #Math

  30. Axiomatic theory of hereditarily finite sets and its fragments (in Isabelle/HOL). ~ Štěpán Holub, Zuzana Haniková. isa-afp.org/entries/ZF_finite. #IsabelleHOL #ITP #Math

  31. Certified infinite descent criteria (in Isabelle/HOL). ~ Jamie Wright, Liron Cohen, Reuben Rowe, Andrei Popescu. isa-afp.org/entries/Infinite_D #IsabelleHOL #ITP

  32. Certified infinite descent criteria (in Isabelle/HOL). ~ Jamie Wright, Liron Cohen, Reuben Rowe, Andrei Popescu. isa-afp.org/entries/Infinite_D #IsabelleHOL #ITP

  33. Formalization of 3-independence of simple tabulation hashing (in Isabelle/HOL). ~ Wei De Leong, Yong Kiam Tan, Seng Joe Watt. isa-afp.org/entries/Tabulation #IsabelleHOL #ITP

  34. Formalization of 3-independence of simple tabulation hashing (in Isabelle/HOL). ~ Wei De Leong, Yong Kiam Tan, Seng Joe Watt. isa-afp.org/entries/Tabulation #IsabelleHOL #ITP