<p><span class="h-card" translate="no"><a href="https://mastodon.social/@whitequark" class="u-url mention">@<span>whitequark</span></a></span> 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: <a href="https://www.philipzucker.com/z3-rise4fun/guide.html" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">philipzucker.com/z3-rise4fun/g</span><span class="invisible">uide.html</span></a></p><p>Then it’s much heavier than an SMT solver but <a href="https://mathstodon.xyz/tags/lean4" class="mention hashtag" rel="tag">#<span>lean4</span></a> 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. <a href="https://lean-lang.org/theorem_proving_in_lean4/introduction.html" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">lean-lang.org/theorem_proving_</span><span class="invisible">in_lean4/introduction.html</span></a></p>