Lecturas compartidas el 30 de abril de 2024
#ITP #Lean4 #IsabelleHOL #Coq #ATP #SMT #FunctionalProgramming #Haskell #Python #Logic #Math
Buenos días
Las lecturas compartidas en Mastodon el 30 de abril de 2024 son
Lecturas compartidas el 29 de abril de 2024. #FunctionalProgramming #Haskell #Python #Math
#Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "si f es inyectiva, entonces ⋂ᵢf[Aᵢ] ⊆ f[⋂ᵢAᵢ]". #ITP #Lean4 #IsabelleHOL #Math
#Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "f⁻¹[⋃ᵢ Bᵢ] = ⋃ᵢ f⁻¹[Bᵢ]". #ITP #Lean4 #IsabelleHOL #Math
#Exercitium: Numeración de las ternas de números naturales. #Haskell #Python #Matemáticas
Mechanised uniform interpolation for modal logics K, GL, and iSL. ~ Hugo Férée, Iris van der Giessen, Sam van Gool, Ian Shillito. #ITP #Coq #Logic
Solving quantified modal logic problems by translation to classical logics. ~ Alexander Steen, Geoff Sutcliffe, Christoph Benzmüller. #ATP #Logic
Type inference for Isabelle2Cpp. ~ Dongchen Jiang, Chenxi Fu. #ITP #IsabelleHOL
Experiments in the irrationality of Sqrt 2 with SMT. ~ Philip Zucker (@sandmouth@types.pl). #ATP #SMT #Math
También están en GitHub.
Saludos, José A.
"Cuando se menciona la libertad, siempre debemos tener cuidado de observar si no es realmente la afirmación de intereses privados lo que con ello se designa." ~ Georg Wilhelm Friedrich Hegel (1770-1831).