#rocqprover — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #rocqprover, aggregated by home.social.
-
It’s neat to see that an old (fiddly, complicated) decidability argument I wrote up in the 1990s is getting some attention. Here, Raj Goré and Anthony Peigné formalise (and generalise) my decidability argument for display formulations of some substructural logics. This is interesting work, worth looking into.
https://link.springer.com/article/10.1007/s11225-026-10239-8
-
A general formalised framework for reasoning about display calculi. ~ Rajeev Goré, Anthony Peigné. https://link.springer.com/article/10.1007/s11225-026-10239-8 #RocqProver #ITP #Logic
-
A general formalised framework for reasoning about display calculi. ~ Rajeev Goré, Anthony Peigné. https://link.springer.com/article/10.1007/s11225-026-10239-8 #RocqProver #ITP #Logic
-
A general formalised framework for reasoning about display calculi. ~ Rajeev Goré, Anthony Peigné. https://link.springer.com/article/10.1007/s11225-026-10239-8 #RocqProver #ITP #Logic
-
A general formalised framework for reasoning about display calculi. ~ Rajeev Goré, Anthony Peigné. https://link.springer.com/article/10.1007/s11225-026-10239-8 #RocqProver #ITP #Logic
-
A general formalised framework for reasoning about display calculi. ~ Rajeev Goré, Anthony Peigné. https://link.springer.com/article/10.1007/s11225-026-10239-8 #RocqProver #ITP #Logic
-
On reasoning-centric LLM-based automated theorem proving. ~ Yican Sun, Chengwei Shi, Hangzhou Lyu, Yingfei Xiong. https://arxiv.org/abs/2604.19558v1 #RocqProver #AI4Math
-
Readings shared April 4, 2026. https://jaalonso.github.io/vestigium/posts/2026/04/04-readings_shared_04-04-26 #AI #AI4Math #ATP #Agda #AlphaProof #Autoformalization #CategoryTheory #CoqProver #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LambdaCalculus #LeanProver #Lisp #Logic #LogicProgramming #LLMs #Math #Physics #Programming #Prolog #Racket #RocqProver #Vampire