[SMT-LIB] Multiarity XOR, IFF

[John Matthews]

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