Recent searches
Search options
SMT people write useful fucking documentation challenge (impossible)
@whitequark i don’t really know anything about SMT-LIB but do know something about formal (and first order specifically) logic but this documentation has a long section on quantifiers: https://www.philipzucker.com/z3-rise4fun/guide.html
Then it’s much heavier than an SMT solver but #lean4 is really powerful with good documentation on using quantifiers. I really like it. But it has a heavy emphasis on using tooling and I’m the kind of person who likes rustfmt. https://lean-lang.org/theorem_proving_in_lean4/introduction.html
@gigapixel I did read that document and I found it to not really advance my understanding of the topic
re Lean, I've actually been learning Lean but it won't help me automatically verify compiler optimizations by lowering before/after netlists to it