Questions tagged [smt]
The smt tag has no usage guidance.
2
questions
4
votes
3
answers
345
views
How does Z3 "exhaustively search" real numbers?
I was looking at this tutorial: https://colab.research.google.com/github/philzook58/z3_tutorial/blob/master/Z3%20Tutorial.ipynb#scrollTo=4yuA2Fry68Y6&line=4&uniqifier=1 .
It says "Proof = ...
- 143
1
vote
1
answer
295
views
How does one translate Lean to Coq (and visa versa)?
I am interested in translated Lean to Coq and visa versa. One first reason is because I want to translate the miniF2F data set in Lean to Coq but lack the expertise to do it. Though in general I'd ...
- 333