[SMT-LIB] SMT-LIB semantics

[Viktor Kuncak]

> > To me, FREE would mean that function symbols come from
> > term algebra, that is, inductively definited data types.
>
> That is not quite how "free" is used in the literature, at least the
> literature *I* am familiar with :)
>
> When people want to say what you mean they refer to those symbols as
> "free constructors" not "free symbols".
> In truth, I have seen some authors use "free symbol" in your sense,
> but, as far as I can tell, it is not the norm (and is of course
> confusing).

One of those authors is Jean Gallier, if you look at Section 2.3.2
(Chapter 2) on Freely Generated Sets, page 21, where the first
requirement is injectivity:

http://www.cis.upenn.edu/~jean/gbooks/logic.html

  Viktor