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