[SMT-LIB] Multiarity XOR, IFF

[Cesare Tinelli]

On Nov 7, 2007, at 2:35 PM, Michal Moskal wrote:

> On 11/7/07, Cesare Tinelli <tinelli at cs.uiowa.edu> wrote:
>> The standard *does* allow a multiarity = (with arity starting at 2).
>> See, e.g., pages 36 and 37 of the standard.
>> The semantics of (= a b c) is meant to be (and (= a b) (= b c)), as
>> one would expect.
>
> I find it strange, that (= a b c) is different from (iff a b c).
>
The different treatment is motivated by their different type: = is a  
predicate symbol, takes terms and produces a formula, while IFF is a  
logical connective, takes formulas and produces a formula.

The only possible interpretation for (= a b c) is the conjunctive one  
as (= (= a b) c) is not even well typed in the SMT-LIB type system.
For (iff a b c) on the other hand, it is possible and reasonable to  
adopt either one. Which one to prefer is a matter of convenience for  
the intended user-base.


Cesare


> -- 
>    Michał
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib