#isabellehol — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #isabellehol, aggregated by home.social.
-
New and formalized proofs for right-forward closures and core matrix interpretations. ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.32 #IsabelleHOL #ITP
-
New and formalized proofs for right-forward closures and core matrix interpretations. ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.32 #IsabelleHOL #ITP
-
New and formalized proofs for right-forward closures and core matrix interpretations. ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.32 #IsabelleHOL #ITP
-
New and formalized proofs for right-forward closures and core matrix interpretations. ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.32 #IsabelleHOL #ITP
-
New and formalized proofs for right-forward closures and core matrix interpretations. ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.32 #IsabelleHOL #ITP
-
Termination restricted to right-forward closures (in Isabelle/HOL). ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://isa-afp.org/entries/Right_Forward_Closures.html #IsabelleHOL #ITP
-
Termination restricted to right-forward closures (in Isabelle/HOL). ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://isa-afp.org/entries/Right_Forward_Closures.html #IsabelleHOL #ITP
-
Termination restricted to right-forward closures (in Isabelle/HOL). ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://isa-afp.org/entries/Right_Forward_Closures.html #IsabelleHOL #ITP
-
Termination restricted to right-forward closures (in Isabelle/HOL). ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://isa-afp.org/entries/Right_Forward_Closures.html #IsabelleHOL #ITP
-
Termination restricted to right-forward closures (in Isabelle/HOL). ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. https://isa-afp.org/entries/Right_Forward_Closures.html #IsabelleHOL #ITP
-
Conway's circle theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Conway_Circle.html #IsabelleHOL #ITP #Math
-
Conway's circle theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Conway_Circle.html #IsabelleHOL #ITP #Math
-
Conway's circle theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Conway_Circle.html #IsabelleHOL #ITP #Math
-
Conway's circle theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Conway_Circle.html #IsabelleHOL #ITP #Math
-
Conway's circle theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Conway_Circle.html #IsabelleHOL #ITP #Math
-
Polynomial commitment schemes (in Isabelle/HOL). ~ Tobias Rothmann. https://isa-afp.org/entries/Polynomial_Commitment_Schemes.html #IsabelleHOL #ITP
-
Polynomial commitment schemes (in Isabelle/HOL). ~ Tobias Rothmann. https://isa-afp.org/entries/Polynomial_Commitment_Schemes.html #IsabelleHOL #ITP
-
Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/MSOinHOL.html #IsabelleHOL #ITP #Logic
-
Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/MSOinHOL.html #IsabelleHOL #ITP #Logic
-
Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/MSOinHOL.html #IsabelleHOL #ITP #Logic
-
Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/MSOinHOL.html #IsabelleHOL #ITP #Logic
-
Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. https://isa-afp.org/entries/MSOinHOL.html #IsabelleHOL #ITP #Logic
-
The Chevalley-Warning theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Chevalley_Warning.html #IsabelleHOL #ITP #Math
-
The Chevalley-Warning theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. https://isa-afp.org/entries/Chevalley_Warning.html #IsabelleHOL #ITP #Math
-
First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. https://arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic
-
First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. https://arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic
-
First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. https://arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic
-
First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. https://arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic
-
First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. https://arxiv.org/abs/2607.10880 #IsabelleHOL #ITP #Logic
-
Formalizing paradoxes in grounded arithmetic using Isabelle/HOL. ~ Ananthajit Srikanth, Bryan Ford. https://bford.info/pub/lang/paradox/paradox.pdf #IsabelleHOL #ITP #Math
-
Formalizing paradoxes in grounded arithmetic using Isabelle/HOL. ~ Ananthajit Srikanth, Bryan Ford. https://bford.info/pub/lang/paradox/paradox.pdf #IsabelleHOL #ITP #Math
-
Complete elliptic integrals and the arithmetic–geometric mean (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Arithmetic_Geometric_Mean.html #IsabelleHOL #ITP #Math
-
Complete elliptic integrals and the arithmetic–geometric mean (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Arithmetic_Geometric_Mean.html #IsabelleHOL #ITP #Math
-
Bessel functions of the first kind (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Bessel.html #IsabelleHOL #ITP #Math
-
Bessel functions of the first kind (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Bessel.html #IsabelleHOL #ITP #Math
-
The exponential and logarithmic integral (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Exp_Log_Integral.html #IsabelleHOL #ITP #Math
-
The exponential and logarithmic integral (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Exp_Log_Integral.html #IsabelleHOL #ITP #Math
-
Generalised hypergeometric series (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Generalized_Hypergeometric_Series.html #IsabelleHOL #ITP #Math
-
Generalised hypergeometric series (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Generalized_Hypergeometric_Series.html #IsabelleHOL #ITP #Math
-
Rademacher's series for the partition function (in Isabelle/HOL). ~ Manuel Eberl, Lawrence C. Paulson. https://isa-afp.org/entries/Rademacher_Series.html #IsabelleHOL #ITP #Math
-
Rademacher's series for the partition function (in Isabelle/HOL). ~ Manuel Eberl, Lawrence C. Paulson. https://isa-afp.org/entries/Rademacher_Series.html #IsabelleHOL #ITP #Math
-
The incomplete gamma function (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Incomplete_Gamma.html #IsabelleHOL #ITP #Math
-
The incomplete gamma function (in Isabelle/HOL). ~ Manuel Eberl. https://isa-afp.org/entries/Incomplete_Gamma.html #IsabelleHOL #ITP #Math