The Nelson-Oppen simplifier is a great piece of work, but it is not the first SAT solver. Boyer and Moore published their formally verified SAT solver in their 1979 A Computational Logic, the first book on the…
As an insider and major user of this effort in ImandraX, I must say: Moonpool and OCaml5 concurrency have been an absolute game-changer! Awesome read.
Xavier Leroy as Lou Reed... :-) Don't forget the amazing theorem provers too, like Imandra ( https://www.imandra.ai/core ), HOL-Light ( https://hol-light.github.io/ ) and Rocq ( https://rocq-prover.org/ ), ... !
check out Imandra's platform for neurosymbolic AI - https://www.imandra.ai/
Beautiful! Imandra is a modern Boyer-Moore style theorem prover for higher-order functional programming (its logic is based on a typed higher-order subset of OCaml rather than Boyer-Moore's basis on an untyped…
This is interesting work but it totally misses the boat when it talks about the current state of the art. They cite a 2014 version of the Goel-Hunt-et al formal x86 model in ACL2, but they fail to talk about its modern…
The Nelson-Oppen simplifier is a great piece of work, but it is not the first SAT solver. Boyer and Moore published their formally verified SAT solver in their 1979 A Computational Logic, the first book on the…
As an insider and major user of this effort in ImandraX, I must say: Moonpool and OCaml5 concurrency have been an absolute game-changer! Awesome read.
Xavier Leroy as Lou Reed... :-) Don't forget the amazing theorem provers too, like Imandra ( https://www.imandra.ai/core ), HOL-Light ( https://hol-light.github.io/ ) and Rocq ( https://rocq-prover.org/ ), ... !
check out Imandra's platform for neurosymbolic AI - https://www.imandra.ai/
Beautiful! Imandra is a modern Boyer-Moore style theorem prover for higher-order functional programming (its logic is based on a typed higher-order subset of OCaml rather than Boyer-Moore's basis on an untyped…
This is interesting work but it totally misses the boat when it talks about the current state of the art. They cite a 2014 version of the Goel-Hunt-et al formal x86 model in ACL2, but they fail to talk about its modern…