[SMT-LIB] Naming of SMTLIB logics

[cok at frontiernet.net]

SMT-LIB community: (resend, this time to smt-lib)


My second question, prompted by the SMTEVAL and the proposal of a new 
theory concerns the naming of logics.

The names of logics are essentially a combination of 
characteristics/theories that are largely but not completely 
independent. Current names have a syntax something like
   [QF_] [UF] [A|AX] [BV] [ ([N|L][IA|RA|IRA]) | IDL | RDL ]
Not nearly all combinations currently exist, but most of them could. 
Now we are adding S (for Separation Logic) into the mix. But we may also 
soon have a String theory and a Floating Point theory to include.

I don't have a proposal on this point, but it seems to me that creating 
logics in this fashion is becoming unwieldy. At least the naming might 
be simplified, standardized, with a clear means for expansion as new 
theories are proposed and combined with existing theories.

I would welcome some discussion and a path to resolution on this.

- David Cok