Two styles of theorem-proving

[gmhwxi]

I finished a short article on two styles of theorem-proving in ATS:

http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP-bool-vs-prop/index.html

I noticed in the past that many users of ATS had confusion of the sort 'bool' with the sort 'prop',
which are closely related but also fundamentally different. I hope this article can clarify the issue
for the good.

Cheers!

--Hongwei

[Artyom Shalkhakov]

Curious: does Z3 support theorem proving over finite sets/maps?

For instance, a sort for finite sets of labels and a static function from label to a t@ype could be used to model an extensible record (or a finite map from labels/strings to t@ype). Then it would "only" be necessary to figure out how to represent these records at runtime. From what I understand, sqlite, pgsql and mysql client libraries simply use CSV (basically) for representing records in a result set, though.

 

Cheers!

--Hongwei

[gmhwxi]

I would think so. Z3 is quite advanced.