[YICES-HELP] quantification basics?

[Bruno Dutertre]

Mark R. Tuttle wrote:
> Can anyone help me understand why YICES says "unknown" instead of
> "unsat" for the following example?
> 
> (define-type elem)
> (define-type set)
> (define mem::(-> elem set bool))
> 
> (define S::set)
> (define T::set)
> 
> (define equal_axiom::bool
>    (forall (a::set b::set)
>       (=> (not (= a b))
>           (exists (x::elem) (not (= (mem x a) (mem x b)))))))
> 
> (define equal_claim::bool
>       (=> (forall (x::elem) (= (mem x S) (mem x T)))
> 	  (= S T)))
> 
> (assert equal_axiom)
> (assert (not equal_claim))
> (check)
> 
> I was hoping that Skolemization and pattern matching would let YICES
> simulate the reasoning
> 
> (forall (x::elem) (= (mem x S) (mem x T)))
> (not (= S T))
> 
> then
> 
> (forall (x::elem) (= (mem x S) (mem x T)))
> (exists (x::elem) (not (= (mem x S) (mem x T))))
> 
> then
> 
> (forall (x::elem) (= (mem x S) (mem x T)))
> (not (= (mem SKL S) (mem SKL T)))
> 
> then
> 
> (= (mem SKL S) (mem SKL T))
> (not (= (mem SKL S) (mem SKL T)))
> 
> then
> 
> false
> 
> I understand that quantification makes things only semi-decidable, I'm
> just looking for a slightly deeper understanding of what YICES can do
> with quantification.  I'm running 1.0.29.
> 
> Thanks
> Mark Tuttle, tuttle at acm.org
> 

Mark,

The problem here is that Yices uses pattern matching
on terms and that an equality is not a term. In general,
for any quantified formula, Yices tries to compute a
set of patterns that are used later for matching.
Each pattern must be a term or set of terms in the
formulas that contain all the quantified variables.
There are various heuristics to select what's a good
pattern: something that's too easy to match is a bad
idea since it can causes a huge blow up.

Based on this, your first assertion is problematic for Yices:

   (forall (a::set b::set) (=> (not (= a b)) (exist ...)))

The heuristics don't find any useful pattern in this
formula: (= a b) is not a term so it can't be used.
the pair of variables (a, b) would work but it's not
considered as a good pattern, since it's not selective
enough.

A possible work around is to add your own eq predicate:

(define-type elem)
(define-type set)
(define mem::(-> elem set bool))

(define eq::(-> set set bool))

(define S::set)
(define T::set)

(define equal_axiom::bool
    (forall (a::set b::set)
       (=> (not (eq a b))
           (exists (x::elem) (not (= (mem x a) (mem x b)))))))

(define equal_claim::bool
       (=> (forall (x::elem) (= (mem x S) (mem x T)))
	  (eq S T)))

(assert equal_axiom)
(assert (not equal_claim))
(check)



But you could also define sets as mappings from elem to bool. Since
Yices already knows about extensionality, you don't need equal_axiom
anymore. You could just write:

(define-type elem)
(define-type set (-> elem bool))
(define mem::(-> elem set bool) (lambda (e::elem s::set) (s e)))

(define S::set)
(define T::set)

(define equal_claim::bool
       (=> (forall (x::elem) (= (mem x S) (mem x T)))
	  (eq S T))))

(assert (not equal_claim))
(check)


Bruno