sigmoid.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
A social space for people researching, working with, or just interested in AI!

Server stats:

612
active users

#z3

0 posts0 participants0 posts today
Alexander Kmoch<p>Kevin Sahr DGGRID 8.41 was released, with full support for <a href="https://fosstodon.org/tags/IGEO7" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IGEO7</span></a> <a href="https://fosstodon.org/tags/Z7" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z7</span></a> <a href="https://fosstodon.org/tags/ZORDER" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ZORDER</span></a> and <a href="https://fosstodon.org/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a> indexing for <a href="https://fosstodon.org/tags/ISEA" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ISEA</span></a> 3,4 and 7 H <a href="https://fosstodon.org/tags/DGGS" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>DGGS</span></a> the binaries on conda-forge are updated. And we are now testing HTML readme/docs:</p><p><a href="https://github.com/sahrk/DGGRID/releases" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">github.com/sahrk/DGGRID/releas</span><span class="invisible">es</span></a></p><p><a href="https://dggrid.readthedocs.io/latest/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">dggrid.readthedocs.io/latest/</span><span class="invisible"></span></a></p><p><a href="https://anaconda.org/conda-forge/dggrid" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">anaconda.org/conda-forge/dggri</span><span class="invisible">d</span></a></p>
José A. Alonso<p>Readings shared June 11, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/12-readings_shared_06-11-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/06/12-readings_shared_06-11-25</span></a> <a href="https://mathstodon.xyz/tags/AIforMath" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>AIforMath</span></a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CompSci</span></a> <a href="https://mathstodon.xyz/tags/IA" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IA</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/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</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/RustLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>RustLang</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p>
José A. Alonso<p>Z3Guide: A scalable, student-centered, and extensible educational environment for logic modeling. ~ Ruanqianqian Huang, Ayana Monroe, Peli de Halleux, Sorin Lerner, Nikolaj Bjørner. <a href="https://arxiv.org/abs/2506.08294v1" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2506.08294v1</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a> <a href="https://mathstodon.xyz/tags/Teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Teaching</span></a></p>
Verfassungklage@troet.cafe<p>Ein <a href="https://troet.cafe/tags/Relaisrechner" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Relaisrechner</span></a> in Aktion zum 115. <a href="https://troet.cafe/tags/Zuse" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Zuse</span></a> - <a href="https://troet.cafe/tags/Geburtstag" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Geburtstag</span></a>: </p><p><a href="https://troet.cafe/tags/Computer" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Computer</span></a> ohne Bildschirm, Maus oder Tastatur, wie funktionierte das überhaupt? Zum 115. Geburtstag von <a href="https://troet.cafe/tags/KonradZuse" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>KonradZuse</span></a> zeigt das <a href="https://troet.cafe/tags/ZCOM" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ZCOM</span></a> am Sonntag, den 22.06.2025 ab 13 Uhr im Rahmen der Reihe „Anfassen &amp; Verstehen“ ein funktionsfähiges Modell eines <a href="https://troet.cafe/tags/historischen" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>historischen</span></a> <a href="https://troet.cafe/tags/Relaisrechners" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Relaisrechners</span></a>. Mit Klicks, <a href="https://troet.cafe/tags/Klacken" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Klacken</span></a> und <a href="https://troet.cafe/tags/Kontaktfedern" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Kontaktfedern</span></a> wird erlebbar, wie <a href="https://troet.cafe/tags/Zuse" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Zuse</span></a> seine <a href="https://troet.cafe/tags/bahnbrechende" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>bahnbrechende</span></a> <a href="https://troet.cafe/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a> entwickelte und damit einen Grundstein... </p><p><a href="https://zuse-computer-museum.com/veranstaltung/ein-relaisrechner-in-aktion-zum-115-zuse-geburtstag-2151/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">zuse-computer-museum.com/veran</span><span class="invisible">staltung/ein-relaisrechner-in-aktion-zum-115-zuse-geburtstag-2151/</span></a></p>
José A. Alonso<p>Readings shared May 8, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/08-readings_shared_05-08-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/05/08-readings_shared_05-08-25</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/Autoformalization" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Autoformalization</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/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/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Programming</span></a> <a href="https://mathstodon.xyz/tags/SAT_solvers" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SAT_solvers</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p>
José A. Alonso<p>SAT-solving the poset cover problem. ~ Chih-Cheng Rex Yuan, Bow-Yaw Wang. <a href="https://arxiv.org/abs/2505.04013" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2505.04013</span><span class="invisible"></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/SAT_solvers" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SAT_solvers</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p>
Jan :rust: :ferris:<p>The inner magic behind the Z3 theorem prover - Microsoft Research (October 2019):</p><p><a href="https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">microsoft.com/en-us/research/b</span><span class="invisible">log/the-inner-magic-behind-the-z3-theorem-prover/</span></a></p><p><a href="https://floss.social/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a> <a href="https://floss.social/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalVerification</span></a> <a href="https://floss.social/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ModelChecking</span></a> <a href="https://floss.social/tags/Proof" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Proof</span></a></p>
José A. Alonso<p>Readings shared April 19, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/19-readings_shared_04-19-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/19-readings_shared_04-19-25</span></a> <a href="https://mathstodon.xyz/tags/Algorithms" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Algorithms</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/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MachineLearning</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/Python" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Python</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p>
José A. Alonso<p>Knuckledragger: A low barrier proof assistant. ~ Philip Zucker. <a href="https://github.com/philzook58/knuckledragger" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">github.com/philzook58/knuckled</span><span class="invisible">ragger</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/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a> <a href="https://mathstodon.xyz/tags/Python" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Python</span></a></p>
José A. Alonso<p>Readings shared April 1, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/01-readings_shared_04-01-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/01-readings_shared_04-01-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/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/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LogicProgramming</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/Prolog" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Prolog</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p>
José A. Alonso<p>A small Prolog on the Z3 AST. ~ Philip Zucker. <a href="https://www.philipzucker.com/knuck_prolog/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="">philipzucker.com/knuck_prolog/</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Prolog</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LogicProgramming</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a></p>
José A. Alonso<p>Readings shared March 18, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/18-readings_shared_03-18-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/03/18-readings_shared_03-18-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/ASP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ASP</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/CLP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CLP</span></a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CommonLisp</span></a> <a href="https://mathstodon.xyz/tags/Datalog" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Datalog</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/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LogicProgramming</span></a> <a href="https://mathstodon.xyz/tags/Mace" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Mace</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/Otter" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Otter</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Prolog</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/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p>
José A. Alonso<p>Lessons learned with the Z3 SAT/SMT solver. ~ John D. Cook. <a href="https://www.johndcook.com/blog/2025/03/17/lessons-learned-with-the-z3-sat-smt-solver" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">johndcook.com/blog/2025/03/17/</span><span class="invisible">lessons-learned-with-the-z3-sat-smt-solver</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p>
José A. Alonso<p>Readings shared March 11, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/11-readings_shared_03-11-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/03/11-readings_shared_03-11-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/Emacs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Emacs</span></a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalVerification</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/Jape" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Jape</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/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LogicProgramming</span></a> <a href="https://mathstodon.xyz/tags/MAS" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MAS</span></a> <a href="https://mathstodon.xyz/tags/Mace" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Mace</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/Otter" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Otter</span></a> <a href="https://mathstodon.xyz/tags/PVS" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>PVS</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Prolog</span></a> <a href="https://mathstodon.xyz/tags/SMLs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMLs</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Scala" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Scala</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p>
José A. Alonso<p>Knuth Bendix solver on Z3 AST. ~ Philip Zucker. <a href="https://www.philipzucker.com/knuth_bendix_knuck/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">philipzucker.com/knuth_bendix_</span><span class="invisible">knuck/</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p>
LAYERED<p>Part 2 of building the Z3 replica.</p><p><a href="https://www.youtube.com/watch?v=wnRMQ5bVQF4" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">youtube.com/watch?v=wnRMQ5bVQF</span><span class="invisible">4</span></a></p><p><a href="https://chaos.social/tags/RetroComputer" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>RetroComputer</span></a> <a href="https://chaos.social/tags/VintageComputer" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>VintageComputer</span></a> <a href="https://chaos.social/tags/Zuse" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Zuse</span></a> <a href="https://chaos.social/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p>
LAYERED<p>Another, a bit more longer, very interesting documentary about the more "modern" replica of the original Zuse Z3. Built and presented by Konrad Zuse's son Prof. Dr. Horst Zuse (German).</p><p>Part 1</p><p><a href="https://chaos.social/tags/RetroComputer" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>RetroComputer</span></a> <a href="https://chaos.social/tags/VintageComputer" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>VintageComputer</span></a> <a href="https://chaos.social/tags/Zuse" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Zuse</span></a> <a href="https://chaos.social/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p><p><a href="https://www.youtube.com/watch?v=mxIbNPpmFT8" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">youtube.com/watch?v=mxIbNPpmFT</span><span class="invisible">8</span></a></p>
José A. Alonso<p>Readings shared February 1, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/02/01-readings_shared_02-01-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/02/01-readings_shared_02-01-25</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/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</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/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</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/Erlang" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Erlang</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/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LLMs</span></a></p>
José A. Alonso<p>Instantiation-based formalization of logical reasoning tasks using language models and logical solvers. ~ Mohammad Raza, Natasa Milic-Frayling. <a href="https://arxiv.org/abs/2501.16961" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2501.16961</span><span class="invisible"></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/Reasoning" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Reasoning</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/Z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Z3</span></a></p>
Philip Zucker<p>[New Blog Post] Egg-style Equality Saturation using only Z3 <a href="https://philipzucker.com/z3_eq_sat/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">philipzucker.com/z3_eq_sat/</span><span class="invisible"></span></a> <a href="https://types.pl/tags/z3" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>z3</span></a> <a href="https://types.pl/tags/smt" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>smt</span></a> <a href="https://types.pl/tags/egg" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>egg</span></a></p>