|
|
|
|
|
|
by chaoskanzlerin
744 days ago
|
|
|
The main upside Isabelle has over other proof assistants is the existence of Sledgehammer: invoke it, and your current proof state gets handed off to a SMT solver like cvc4, veriT, z3, vampire, etc. If the SMT solver finds a solution, Isabelle then reconstructs the proof. It's essentially a brute-force button that no other proof assistant (aside from Coq) has. |
|
|