#Prover9

@jalonso.eurosky.social

1 month ago

Readings shared January 24, 2026 The readings shared in Bluesky on 24 January 2026 are: Abel's limit theorem (in Isabelle/HOL). ~ Kangfeng Ye. #ITP #IsabelleHOL #Math A formalization of the downward Löwenheim-Skolem theorem in Coq.

Readings shared January 24, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #ATP #CoqProver #HOL_Light #ITP #IsabelleHOL #LeanProver #Logic #Math #Prover9 #RocqProver

0 1 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

Elementary proofs of ring commutativity theorems Jacobson's commutativity theorem says that a ring is commutative if, for each $x$, $x^n = x$ for some $n > 1$. Herstein's generalization says that the condition can be weakened to $x^n-x$ being centra...

Elementary proofs of ring commutativity theorems. ~ Michael Kinyon, Desmond MacHale. arxiv.org/abs/2601.125... #ATP #Prover9 #Math

3 1 0 0

José A. Alonso

@jalonso.eurosky.social

8 months ago

Readings shared July 12, 2025 The readings shared in Bluesky on 12 July 2025 are A formalization of divided powers in Lean. ~ Antoine Chambert-Loir, María Inés de Frutos-Fernández. #ITP #LeanProver #Math Completeness of the decre

Readings shared July 12, 2025. jaalonso.github.io/vestigium/po... #ASP #ATP #CLP #CategoryTheory #CoqProver #Emacs #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog #ProofTheory #Prover9

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

8 months ago

Marginal subsemigroups and commutators in inverse semigroups - Semigroup Forum Marginal subgroups, introduced by P. Hall, are characteristic subgroups induced by group words. The goal of this paper is to extend the notion to inverse semigroups. Our first main result establishes ...

Marginal subsemigroups and commutators in inverse semigroups. ~ Gonçalo Araújo, João Araújo, Michael Kinyon link.springer.com/article/10.1... #ATP #Prover9 #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

9 months ago

Readings shared June 10, 2025 The readings shared in Bluesky on 10 June 2025 are Inductive definitions. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math The equational theories project: advancing collaborative mathematical research at

Readings shared June 10, 2025. jaalonso.github.io/vestigium/po... #AI #AIforMath #ATP #AlphaProof #Emacs #ITP #IsabelleHOL #LLMs #LeanProver #Math #Prover9

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

9 months ago

Are LLMs Reliable Translators of Logical Reasoning Across Lexically Diversified Contexts? Neuro-symbolic approaches combining large language models (LLMs) with solvers excels in logical reasoning problems need long reasoning chains. In this paradigm, LLMs serve as translators, converting n...

Are LLMs reliable translators of logical reasoning across lexically diversified contexts? ~ Qingchuan Li et als. arxiv.org/abs/2506.045... #LLMs #Math #ATP #Prover9

0 0 0 0

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

0 0 0 0

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

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

11 months ago

Readings shared February 24, 2025 The readings shared in Bluesky on 24 March 2025 are Formal verification of machine learning models in Lean. ~ Matéo H. Petel. #ITP #LeanProver #MachineLearning Why Lisp syntax works. ~ Fernando Borre

Readings shared March 24, 2025. jaalonso.github.io/vestigium/po... #AI #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Lisp #LogicProgramming #MachineLearning #Math #Otter #Prolog #Prover9

1 1 1 0

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

2 0 0 0

José A. Alonso

@jalonso.eurosky.social

11 months ago

Readings shared February 18, 2025 The readings shared in Bluesky on 18 March 2025 are Lessons learned with the Z3 SAT/SMT solver. ~ John D. Cook. #SMT #Z3 Teaching logic programming: a review. ~ Serhiy O. Semerikov, Iryna S. Mintii,

Readings shared March 18, 2025. jaalonso.github.io/vestigium/po... #AI #ASP #ATP #CLP #CommonLisp #Datalog #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Logic #LogicProgramming #Mace #Math #Otter #Prolog #Prover9 #SMT #Z3

0 0 0 0

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

2 0 0 0

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

0 0 0 0

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

3 0 0 0

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

0 0 0 0

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

1 0 0 0

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

0 0 0 0

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

2 1 0 0

José A. Alonso

@jalonso.eurosky.social

1 year ago

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

2 1 0 0

José A. Alonso

@jalonso.eurosky.social

1 year ago

First-order theorem proving with power maps in semigroups. ~ Yi Lin1, Ranganathan Padmanabhan & Yang Zhang. ceur-ws.org/Vol-3754/pap... #ATP #Prover9 #Math

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 year ago

Lecturas compartidas el 7 de junio de 2024 Las lecturas compartidas en Mastodon el 7 de junio de 2024 son Lecturas compartidas el 6 de junio de 2024. #ITP #Lean4 #IsabelleHOL #HOLLight #Math #Calculemus: Demostraciones con Lean4 e Isabelle/HO

Lecturas compartidas el 7 de junio de 2024. jaalonso.github.io/vestigium/po... #ITP #Lean4 #IsabelleHOL #PVS #Math #ATP #Prover9 #SMT #Z3 #FunctionalProgramming #Haskell #LLMs

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 year ago

A Closer Look at Logical Reasoning with LLMs: The Choice of Tool Matters Logical reasoning serves as a cornerstone for human cognition. Recently, the emergence of Large Language Models (LLMs) has demonstrated promising progress in solving logical reasoning tasks...

A closer look at logical reasoning with LLMs: The choice of tool matters. ~ Long Hei Matthew Lam, Ehsan Shareghi. arxiv.org/abs/2406.00284 #LLMs #ATP #Prover9 #SMT #Z3

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 year ago

Lecturas compartidas el 30 de mayo de 2024 Las lecturas compartidas en Mastodon el 30 de mayo de 2024 son Lecturas compartidas el 29 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #Python #Calculemus: Demostra

Lecturas compartidas el 30 de mayo de 2024. jaalonso.github.io/vestigium/po... #ITP #Lean4 #IsabelleHOL #Coq #Theorema #HOL_Light #Math #ATP #Prover9 #Vampire #TPTP #FunctionalProgramming #Haskell #LogicProgramming #Prolog #AI #LLMs

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 year ago

Prover9 unleashed: Automated configuration for enhanced proof discovery. ~ Kristina Aleksandrova, Jan Jakubuv and Cezary Kaliszyk. easychair.org/publications... #ATP #Prover9

0 0 0 0

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

0 0 0 0

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

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 year ago

Prover9 unleashed: Automated configuration for enhanced proof discovery. ~ Kristina Aleksandrova, Jan Jakubuv, Cezary Kaliszyk. formalweb3.uibk.ac.at/docs/24/kajj... #ATP #Prover9

0 0 0 0

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

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 years ago

LINC: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. ~ Theo X. Olausson et als. arxiv.org/abs/2310.15164 #LLMs #Reasoning #ATP #Prover9

0 0 0 0

Posts tagged #Prover9