Two styles of theorem-proving

Google Group
1

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

2

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.

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.

3

I would think so. Z3 is quite advanced.On Wednesday, January 6, 2016 at 12:36:13 AM UTC-5, Artyom Shalkhakov wrote:

On Wednesday, January 6, 2016 at 2:09:46 AM UTC+6, gmhwxi wrote:

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.

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