'/%3e%3cpath%20d='M50.3943%2022.237V39.5876H43.5185V22.7481C43.5185%2019.2029%2042.0411%2017.3949%2039.036%2017.3949C35.7325%2017.3949%2034.0778%2019.5338%2034.0778%2023.7585V32.9759H27.2434V23.7585C27.2434%2019.5338%2025.5857%2017.3949%2022.2822%2017.3949C19.2949%2017.3949%2017.8027%2019.2029%2017.8027%2022.7481V39.5876H10.9298V22.237C10.9298%2018.6918%2011.835%2015.8754%2013.6453%2013.7877C15.5128%2011.7049%2017.9623%2010.6355%2021.0028%2010.6355C24.522%2010.6355%2027.1813%2011.9885%2028.9542%2014.6917L30.665%2017.5633L32.3788%2014.6917C34.1517%2011.9885%2036.811%2010.6355%2040.3243%2010.6355C43.3619%2010.6355%2045.8114%2011.7049%2047.6847%2013.7877C49.4931%2015.8734%2050.3963%2018.6899%2050.3943%2022.237Z'%20fill='white'/%3e%3cdefs%3e%3clinearGradient%20id='paint0_linear_89_8'%20x1='30.5'%20y1='0'%20x2='30.5'%20y2='65'%20gradientUnits='userSpaceOnUse'%3e%3cstop%20stop-color='%236364FF'/%3e%3cstop%20offset='1'%20stop-color='%23563ACC'/%3e%3c/linearGradient%3e%3c/defs%3e%3c/svg%3e)
José A. Alonso<p>Readings shared April 13, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/13-readings_shared_04-13-25" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/04/13-readings_shared_04-13-25</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ATP</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Mace4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Mace4</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Prover9" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Prover9</span></a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SetTheory</span></a></p>
#mace4
0 posts0 participants0 posts today
Readings shared February 23, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/23-readings_shared_02-23-25 #ATP #Coq #ITP #IsabelleHOL #Mace4 #Math #Mizar #Prover9 #Rocq
Vestigium · Readings shared February 23, 2025The 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
Fracterm calculus for partial meadows. ~ Jan A. Bergstra, Alban Ponse. https://arxiv.org/abs/2502.13812 #ATP #Prover9 #Mace4 #Math
arXiv.orgFracterm Calculus for Partial MeadowsPartial 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 propositional part of this logic is also known as McCarthy calculus and has been studied extensively.
Axioms for the fracterm calculus of partial meadows are given. The case is made that in this way a rather natural formalisation of fields with division operator is obtained. It is noticed that the logic thus obtained cannot express that division by zero must be undefined.
An interpretation of the three-valued sequential logic into $\bot$-enlargements of partial algebras is given, for which it is concluded that the consequence relation of the former logic is semi-computable, and that the $\bot$-enlargement of a partial meadow is a common meadow.
Readings shared December 13, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/13-readings_shared_12-13-24 #ITP #IsabelleHOL #Coq #Rocq #ATP #Prover9 #Mace4 #Logic #Math
Vestigium · Readings shared December 13, 2024The readings shared in Bluesky on 13 December 2024 are
Readings shared December 12, 2024. #ITP #LeanLang #Lean4 #Math
On extending incorrectness logic with backwards reasoning. ~ Freek Verbeek, Md Sy
Readings shared September 20, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/20-readings_shared_09-20-24 #ITP #Lean4 #IsabelleHOL #Math #Calculemus #ATP #Prover9 #Mace4
Vestigium · Readings shared September 20, 2024The 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
Mapping probability with logic: First order models in puzzle solving. ~ Adrian Groza. https://www.uni.lodz.pl/fileadmin/Projekty/EXTENDD/abstracts.pdf#page=18 #ATP #Prover9 #Mace4
Commutative residual algebra motivation, decision, and applications. ~ Vincent van Oostrom. http://www.javakade.nl/research/pdf/crabytiling-v2.pdf #ATP #Prover9 #Mace4 #Math
Lecturas compartidas el 23 de marzo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-23-de-marzo #AI #ATP #DeepLearning #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #Lean4 #LeanProver #Logic #Mace4 #MachineLearning #NeuralNetwork #Prover9
J.A. Alonso - Newsletter · Lecturas compartidas el 23 de marzo de 2024
Fully evaluated left-sequential logics. ~ Alban Ponse, Daan J.C. Staudt. https://arxiv.org/abs/2403.14576 #ATP #Prover0 #Mace4 #Logic
arXiv.orgFully Evaluated Left-Sequential LogicsWe consider a family of two-valued "fully evaluated left-sequential logics" (FELs), of which Free FEL (defined by Staudt in 2012) is most distinguishing (weakest) and immune to atomic side effects. Next is Memorising FEL, in which evaluations of subexpressions are memorised. The following stronger logic is Conditional FEL (inspired by Guzmán and Squier's Conditional logic, 1990). The strongest FEL is static FEL, a sequential version of propositional logic. We use evaluation trees as a simple, intuitive semantics and provide complete axiomatisations for closed terms (left-sequential propositional expressions).
For each FEL except Static FEL, we also define its three-valued version, with a constant U for "undefinedness" and again provide complete, independent aziomatisations, each one containing two additional axioms for U on top of the axiomatisations of the two-valued case. In this setting, the strongest FEL is equivalent to Bochvar's strict logic.
Automated reasoning for proving non-orderability of groups. ~ Alexei Lisitsa, Zipei Nie, Alexei Vernitski. https://arxiv.org/abs/2310.05891 #ATP #Prover9 #Mace4 #Math
arXiv.orgAutomated reasoning for proving non-orderability of groupsWe demonstrate how a generic automated theorem prover can be applied to establish the non-orderability of groups. Our approach incorporates various tools such as positive cones, torsions, generalised torsions and cofinal elements.
Symmetries for cube-and-conquer in finite model finding. ~ João Araújo, Choiwah Chow, Mikoláš Janota. https://drops.dagstuhl.de/opus/volltexte/2023/19045/pdf/LIPIcs-CP-2023-8.pdf #ATP #Mace4