Kevin Sahr DGGRID 8.41 was released, with full support for #IGEO7 #Z7 #ZORDER and #Z3 indexing for #ISEA 3,4 and 7 H #DGGS the binaries on conda-forge are updated. And we are now testing HTML readme/docs:
https://github.com/sahrk/DGGRID/releases
#z3
0 posts0 participants0 posts today
Readings shared June 11, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/12-readings_shared_06-11-25 #AIforMath #CompSci #IA #ITP #LeanProver #Logic #Math #RustLang #SMT #Z3
Vestigium · Readings shared June 11, 2025The readings shared in Bluesky on 11 June 2025 are
LeanTutor: A formally-verified AI tutor for mathematical proofs. ~ Manooshree Patel et als. #ITP #LeanProver #Math #AIforMath #Teaching
Common Lean
Z3Guide: A scalable, student-centered, and extensible educational environment for logic modeling. ~ Ruanqianqian Huang, Ayana Monroe, Peli de Halleux, Sorin Lerner, Nikolaj Bjørner. https://arxiv.org/abs/2506.08294v1 #Logic #SMT #Z3 #Teaching
arXiv.orgZ3Guide: A Scalable, Student-Centered, and Extensible Educational Environment for Logic ModelingConstraint-satisfaction problems (CSPs) are ubiquitous, ranging from budgeting for grocery shopping to verifying software behavior. Logic modeling helps solve CSPs programmatically using SMT solvers. Despite its importance in many Computer Science disciplines, resources for teaching and learning logic modeling are scarce and scattered, and challenges remain in designing educational environments for logic modeling that are accessible and meet the needs of teachers and students. This paper explores how to design such an environment and probes the impact of the design on the learning experience. From a need-finding interview study and a design iteration with teachers of logic modeling, we curated 10 design guidelines spanning three main requirements: providing easy access, supporting various educational modalities, and allowing extensions for customized pedagogical needs. We implemented nine guidelines in Z3Guide, an open-source browser-based tool. Using Z3Guide in a logic modeling learning workshop with more than 100 students, we gathered positive feedback on its support for learning and identified opportunities for future improvements.
Ein #Relaisrechner in Aktion zum 115. #Zuse - #Geburtstag:
#Computer ohne Bildschirm, Maus oder Tastatur, wie funktionierte das überhaupt? Zum 115. Geburtstag von #KonradZuse zeigt das #ZCOM am Sonntag, den 22.06.2025 ab 13 Uhr im Rahmen der Reihe „Anfassen & Verstehen“ ein funktionsfähiges Modell eines #historischen #Relaisrechners. Mit Klicks, #Klacken und #Kontaktfedern wird erlebbar, wie #Zuse seine #bahnbrechende #Z3 entwickelte und damit einen Grundstein...
zuse-computer-museum.comEin Relaisrechner in Aktion zum 115. Zuse-Geburtstag – Zuse-Computer-Museum Hoyerswerda
SAT-solving the poset cover problem. ~ Chih-Cheng Rex Yuan, Bow-Yaw Wang. https://arxiv.org/abs/2505.04013 #ATP #SAT_solvers #Z3
arXiv.orgSAT-Solving the Poset Cover ProblemThe poset cover problem seeks a minimum set of partial orders whose linear extensions cover a given set of linear orders. Recognizing its NP-completeness, we devised a non-trivial reduction to the Boolean satisfiability problem using a technique we call swap graphs, which avoids the complexity explosion of the naive method. By leveraging modern SAT solvers, we efficiently solve instances with reasonable universe sizes. Experimental results using the Z3 theorem prover on randomly generated inputs demonstrate the effectiveness of our method.
The inner magic behind the Z3 theorem prover - Microsoft Research (October 2019):
https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/
Microsoft Research · Model-based approach behind Z3 theorem prover’s efficiency, powerIn 10-plus years, the Z3 theorem prover has surpassed the use cases that motivated its design in exciting ways. Researchers Nikolaj Bjørner and Leonardo de Moura explain how a model-based approach has contributed to the SMT solver’s success.
Knuckledragger: A low barrier proof assistant. ~ Philip Zucker. https://github.com/philzook58/knuckledragger #ITP #SMT #Z3 #Python
Readings shared April 1, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/01-readings_shared_04-01-25 #AI #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog #SMT #Z3
Vestigium · Readings shared April 1, 2025The readings shared in Bluesky on 1 April 2025 are
A small Prolog on the Z3 AST. ~ Philip Zucker. #Prolog #LogicProgramming #Z3 #SMT
STP: Self-play LLM theorem provers with iterative conjecturing and
A small Prolog on the Z3 AST. ~ Philip Zucker. https://www.philipzucker.com/knuck_prolog/ #Prolog #LogicProgramming #Z3 #SMT
Hey There Buddo! · A Small Prolog on the Z3 ASTOne nice thing about Knuckledragger https://github.com/philzook58/knuckledragger is that I have built a raft of little functionality such that now I can rip out cute little examples.
Lessons learned with the Z3 SAT/SMT solver. ~ John D. Cook. https://www.johndcook.com/blog/2025/03/17/lessons-learned-with-the-z3-sat-smt-solver #SMT #Z3
John D. Cook | Applied Mathematics Consulting · Lessons Learned With the Z3 SAT/SMT SolverSAT and SMT solvers have many industrial uses. Tricks of the trade for getting them to perform better can be useful. Here are a few that I have found.
Knuth Bendix solver on Z3 AST. ~ Philip Zucker. https://www.philipzucker.com/knuth_bendix_knuck/ #SMT #Z3
Hey There Buddo! · Knuth Bendix Solver on Z3 ASTKnuth bendix completion takes in a set of equational axioms and a term ordering (defining which side is “simpler”), and tries to produce a rewrite rule system that is confluent. You can read more here
Continued thread
Part 2 of building the Z3 replica.
Continued thread
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).
Part 1
Readings shared February 1, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/01-readings_shared_02-01-25 #ITP #LeanProver #IsabelleHOL #Coq #SMT #Z3 #Math #Erlang #AI #LLMs
Vestigium · Readings shared February 1, 2025The readings shared in Bluesky on 1 February 2025 are
The continuous functional calculus in Lean. ~ Anatole Dedecker, Jireh Loreaux. #ITP #LeanProver #Math
Formally verifying a transformation from ML
Instantiation-based formalization of logical reasoning tasks using language models and logical solvers. ~ Mohammad Raza, Natasa Milic-Frayling. https://arxiv.org/abs/2501.16961 #LLMs #Reasoning #SMT #Z3
arXiv.orgInstantiation-based Formalization of Logical Reasoning Tasks using Language Models and Logical SolversRobustness of reasoning remains a significant challenge for large language models, and addressing it is essential for the practical applicability of AI-driven reasoning systems. We introduce Semantic Self-Verification (SSV), a novel approach that addresses the key challenge in combining language models with the rigor of logical solvers: to accurately formulate the reasoning problem from natural language to the formal language of the solver. SSV uses a consistency-based approach to produce strong abstract formalizations of problems using concrete instantiations that are generated by the model and verified by the solver. In addition to significantly advancing the overall reasoning accuracy over the state-of-the-art, a key novelty that this approach presents is a feature of verification that has near-perfect precision over a significant coverage of cases, as we demonstrate on open reasoning benchmarks. We propose such *near-certain reasoning* as a new approach to reduce the need for manual verification in many cases, taking us closer to more dependable and autonomous AI reasoning systems.
[New Blog Post] Egg-style Equality Saturation using only Z3 https://philipzucker.com/z3_eq_sat/ #z3 #smt #egg
Hey There Buddo! · Egg-style Equality Saturation using only Z3An egraph is a data structure for storing many ground equalities at once in a highly shared way. Egg style equality saturation searches over this egraph for patterns and asserts nondestructive rewrites into the egraph. Once you’re sick of doing that, you can use extract a best term from the egraph. This may enable you to avoid valleys that greedy rewriting may stick you in and makes the system more robust to the order of rewrites.