[SMT-LIB] Multiarity XOR, IFF

[Aaron Stump]

Dear John,

That is true, but notice that Gries & Scheider 1993 includes two
equivalence operators, one parsed conjunctionally and the other
associatively (section 2.2).  Also, I think it is fair to say that their
proposal for developing propositional logic by heavily using associative
equivalence has not been widely adopted.  The simple reason is probably
that, while extremely clever, their development is not as intuitive as
one based on natural deduction (just look at the proofs of the lemmas in
chapter 3).

Anyhow, I agree with Sava (and several others) that the conjunctional
reading of "iff" is more intuitive and should be adopted in the SMT-LIB
format.

Aaron

> On Nov 7, 2007, at 9:18 AM, Sava Krstic sava.krstic-at-intel.com |SMT- 
> LIB| wrote:
> 
> > but has
> > anyone ever seen expressions like "IFF a b c" or "a IFF b IFF c" to  
> > mean
> >   "(a IFF b) IFF c"?
> >
> 
> David Gries and Fred Schneider have for a long time advocated exactly  
> this interpretation of IFF as an elegant way to calculationally  
> reason about propositional logic. See for example:
> 
>    http://www.cs.cornell.edu/gries/Logic/Calculational.html
> 
> and
> 
>    "A Logical Approach to Discrete Math"
>    David Gries and Fred B. Schneider
>    Springer, 1993
> 
>    (See in particular Chapter 3 "Propositional Calculus", Section 3.2  
> "Equivalence and True" (p. 43). You can
>     read part of this section online at:
>       http://books.google.com/books?id=IGe1miveVI4C&dq=gries+logical 
> +approach+to+discrete 
> +math&pg=PP1&ots=4e7cbS9Dbq&sig=i_2kyozjgs4Yi0b2R5ej1maFXo8&prev=http:// 
> www.google.com/search%3Fclient%3Dsafari%26rls%3Den%26q%3Dgries% 
> 2Blogical%2Bapproach%2Bto%2Bdiscrete%2Bmath%26ie%3DUTF-8%26oe% 
> 3DUTF-8&sa=X&oi=print&ct=title&cad=one-book-with-thumbnail )
> 
> and
> 
>    "Equational Propositional Logic"
>    Gries and Schneider
>    Information Processing Letters, Volume 53, Issue 3 (February 1995)
>    http://portal.acm.org/citation.cfm? 
> id=202402.202416&coll=GUIDE&dl=GUIDE&CFID=4767970&CFTOKEN=98366167
> 
> Best,
> -john
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib