#Mace4

José A. Alonso

@jalonso.eurosky.social

11 months ago

Readings shared April 13, 2025 The readings shared in Bluesky on 13 April 2025 are Completeness of decreasing diagrams for the least uncountable cardinality (in Isabelle/HOL). ~ Ievgen Ivanov. #ITP #IsabelleHOL #Math #SetTheory Ef

Readings shared April 13, 2025. jaalonso.github.io/vestigium/po... #AI #ATP #Coq #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Mace4 #Math #Prover9 #SetTheory

José A. Alonso

@jalonso.eurosky.social

11 months ago

Curso "Razonamiento automático (2011-12)". jaalonso.github.io/cursos/m-ra-11 #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

José A. Alonso

@jalonso.eurosky.social

11 months ago

Curso "Razonamiento automático (2008-09)". jaalonso.github.io/cursos/d-ra-08 #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

José A. Alonso

@jalonso.eurosky.social

11 months ago

Curso "Razonamiento automático (2007-08)". jaalonso.github.io/cursos/d-ra-07 #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

José A. Alonso

@jalonso.eurosky.social

1 year ago

Readings shared February 23, 2025 The readings shared in Bluesky on 23 February 2025 are Power operator for lists (in Isabelle/HOL). ~ Štěpán Holub, Martin Raška, Štěpán Starosta, Tobias Nipkow. #ITP #IsabelleHOL Strands Rocq: Why is

Readings shared February 23, 2025. jaalonso.github.io/vestigium/po... #ATP #Coq #ITP #IsabelleHOL #Mace4 #Math #Mizar #Prover9 #Rocq

José A. Alonso

@jalonso.eurosky.social

1 year ago

Fracterm Calculus for Partial Meadows Partial algebras and datatypes are discussed with the use of signatures that allow partial functions, and a three-valued short-circuit (sequential) first order logic with a Tarski semantics. The propo...

Fracterm calculus for partial meadows. ~ Jan A. Bergstra, Alban Ponse. arxiv.org/abs/2502.13812 #ATP #Prover9 #Mace4 #Math

José A. Alonso

@jalonso.eurosky.social

1 year ago

Readings shared December 13, 2024. jaalonso.github.io/vestigium/po... #ITP #IsabelleHOL #Coq #Rocq #ATP #Prover9 #Mace4 #Logic #Math

José A. Alonso

@jalonso.eurosky.social

1 year ago

Univocity of intuitionistic and classical connectives. ~ Rodolfo C. Ertola-Biraben, Branden Fitelson. philarchive.org/archive/FITUOI #ATP #Prover9 #Mace4 #Logic #Math

José A. Alonso

@jalonso.eurosky.social

1 year ago

Readings shared September 20, 2024 The readings shared in Mastodon on September 20, 2024 are Readings shared September 19, 2024. #ITP #Coq #Math #Haskell #FunctionalProgramming #Logic #AI Proofs of "∑i<n. i = n(n-1)/2" in Lean4 and Is

Readings shared September 20, 2024. jaalonso.github.io/vestigium/po... #ITP #Lean4 #IsabelleHOL #Math #Calculemus #ATP #Prover9 #Mace4

José A. Alonso

@jalonso.eurosky.social

1 year ago

Mapping probability with logic: First order models in puzzle solving. ~ Adrian Groza. www.uni.lodz.pl/fileadmin/Pr... #ATP #Prover9 #Mace4

José A. Alonso

@jalonso.eurosky.social

1 year ago

Lecturas compartidas el 2 de mayo de 2024 #ITP #Lean4 #IsabelleHOL #Coq #Prover9 #Mace4 #FunctionalProgramming #Haskell #Python #Math #AI #ChatGPT

Lecturas compartidas el 2 de mayo de 2024. jalonso.substack.com/lecturas-com... #ITP #Lean4 #IsabelleHOL #Coq #Prover9 #Mace4 #FunctionalProgramming #Haskell #Python #Math #AI #ChatGPT

José A. Alonso

@jalonso.eurosky.social

1 year ago

Commutative residual algebra motivation, decision, and applications. ~ Vincent van Oostrom. www.javakade.nl/research/pdf... #ATP #Prover9 #Mace4 #Math

José A. Alonso

@jalonso.eurosky.social

1 year ago

Lecturas compartidas el 23 de marzo de 2024 #AI #ATP #DeepLearning #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #Lean4 #LeanProver #Logic #Mace4 #MachineLearning #NeuralNetwork #Prover9

Lecturas compartidas el 23 de marzo de 2024. jalonso.substack.com/lecturas-com... #AI #ATP #DeepLearning #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #Lean4 #LeanProver #Logic #Mace4 #MachineLearning #NeuralNetwork #Prover9

José A. Alonso

@jalonso.eurosky.social

1 year ago

Fully evaluated left-sequential logics. ~ Alban Ponse, Daan J.C. Staudt. arxiv.org/abs/2403.14576 #ATP #Prover0 #Mace4 #Logic