(declare-sort 'object-or-man :iff '(or object man)) doesn't work

[alanruttenberg]

(declare-sort 'object)
(declare-sort 'man)
(declare-sort 'object-or-man :iff '(or object man))
==> error: (or object man) has not been declared as a sort.

[alanruttenberg]

I've forked and updated to a slightly later version. It doesn't fix the above issue.

[hoelzl]

The manual for Snark is rather out of date; the sort system of Snark has been rewritten several years ago and the new sort system does not support disjunctive sorts (see function sort-name-expression? in src/sorts-interface.lisp).

A possible implementation for your scenario in the new sort system might be

(declare-sort 'object-or-man :subsorts-incompatible t)
(declare-subsort 'object 'object-or-man)
(declare-subsort 'man 'object-or-man)

With this implementation the following assertions hold

(assert (subsort? (the-sort 'object) (the-sort 'object-or-man)))
(assert (subsort? (the-sort 'man) (the-sort 'object-or-man)))
(assert (sort-disjoint? (the-sort 'object) (the-sort 'man)))

It might be a good idea to contact Richard Waldinger or Vinay Chaudhri whether they still have the source for the Snark tutorial and whether they would be willing to make it available so that it could be kept up to date.

[alanruttenberg]

Thanks for responding. I think I need to be able to work with partitions (hence the disjunctive) and sort complements. Does the following axiom look like something that would do the trick? Do you have an alternate suggestion?

(assert '(forall (c :sort object-or-man)) 
            (or (exists ((a :sort object)) (= a c ))
            (exists ((b :sort man)) (= b c))))

with the sanity check

(prove     
  '(not (exists ((c :sort object-or-man))
            (or (not (exists ((b :sort object)) (= c b)))
                 (not (exists ((a :sort man)) (= c a)))))))

Regarding the source for the tutorial, presumably one can simply check in the current html at http://www.ai.sri.com/snark/tutorial/tutorial.html and then edit from there. But I will see about contacting them. It would be easier to work from the original latex.

[alanruttenberg]

Tex source for the tutorial is now at alanruttenberg@478cc9b