Thread

1. greatgib · 1789642177 · focus · HN ↗

   If anyone wondering, because it took me a few hops to find out:

   Z3 is a high-performance theorem prover being developed at Microsoft Research.

   1. 112233 · 1789643836 · focus · HN ↗

      oh, something new! I thought Z3 is SAT/SMT solver, they must have added something.

      1. Jaxan · 1789643934 · focus · HN ↗

         Sometimes you can use SMT for “theorem proving”. It is a rather broad term. I don’t think they added something much different than what they already had.
      2. IshKebab · 1789645670 · focus · HN ↗

         It is. Look up what SMT stands for.

         1. mcphage · 1789651339 · focus · HN ↗

            Shin Megami Tensei?
         2. NooneAtAll3 · 1789651849 · focus · HN ↗

            SMT is SAT+arithmetic, no?

            1. IshKebab · 1789658184 · focus · HN ↗

               Satisfiability Modulo Theories
      3. baq · 1789658234 · focus · HN ↗

         well a SAT solver is kinda sorta a theorem prover right...?

Unofficial Hacker News client; not affiliated with Y Combinator.