Readings shared April 19, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/19-readings_shared_04-19-25 #Algorithms #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #MachineLearning #Math #Python #SMT #Z3

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

A small Prolog on the Z3 AST. ~ Philip Zucker. https://www.philipzucker.com/knuck_prolog/ #Prolog #LogicProgramming #Z3 #SMT

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

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

Readings shared March 11, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/11-readings_shared_03-11-25 #AI #ATP #Emacs #FormalVerification #Haskell #ITP #IsabelleHOL #Jape #LLMs #LeanProver #Logic #LogicProgramming #MAS #Mace #Math #Otter #PVS #Prolog #SMLs #SMT #Scala #Z3

Knuth Bendix solver on Z3 AST. ~ Philip Zucker. https://www.philipzucker.com/knuth_bendix_knuck/ #SMT #Z3

Part 2 of building the Z3 replica.

https://www.youtube.com/watch?v=wnRMQ5bVQF4

#RetroComputer #VintageComputer #Zuse #Z3

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

#RetroComputer #VintageComputer #Zuse #Z3

https://www.youtube.com/watch?v=mxIbNPpmFT8

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

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

[New Blog Post] Egg-style Equality Saturation using only Z3 https://philipzucker.com/z3_eq_sat/ #z3 #smt #egg

🌘 重載__bool__以實現符號執行
➤ 利用Python中的__bool__函數實現符號執行
✤ https://www.philipzucker.com/overload_bool/
本文介紹瞭如何通過重載Python中的__bool__函數來實現符號執行，以及利用Z3類別記錄Python代碼中的所有路徑的技巧，進行符號執行而無需傳統的流程。
+ 這篇文章對於如何在Python中進行符號執行提供了一個有趣的觀點，讓人對Python的應用產生更多想像。
+ 通過重載__bool__函數來實現符號執行，為語言處理和程式設計帶來了新的可能性，對於技術開發有啟發意義。
#符號執行 #Python #Z3

Readings shared December 16, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/16-readings_shared_12-16-24 #ITP #LeanLang #Lean4 #Logic #SMT #Z3 # #Haskell #FunctionalProgramming #CommonLisp #Programming #AI #Math

'Lean-style' tactics in Knuckledragger. ~ Philip Zucker (@sandmouth.bsky.social). https://www.philipzucker.com/knuckle_lemma/ #Logic #SMT #Z3 #Python

I've completed "Claw Contraption" - Day 13 - Advent of Code 2024

I was looking for an excuse to use z3 again after the hailstones puzzle last year. Part 2 was one extra line.

https://github.com/jstanden/advent-of-code-python/blob/main/2024/day13.ipynb

#AdventOfCode #python #z3 #programming

Readings shared December 10, 2024. https://jaalonso.github.io/vestigium/posts/2024/12/10-readings_shared_12-10-24 #Haskell #Python #Math #Logic #SMT #Z3 #Python #LLMs #Prolog #LogicProgramming

Dyckhoff intuitionistic propositional prover. ~ Philip Zucker (@sandmouth.bsky.social). https://www.philipzucker.com/ljt/ #Logic #SMT #Z3 #Python