[SMT-LIB] SMT-LIB semantics

[Cesare Tinelli]

Hi Viktor,

On Feb 8, 2008, at 2:41 AM, Viktor Kuncak wrote:

> Dear Cesare,
>
> Thanks for all answers, they were helpful.
>
>>> are the function symbols FREE?  Was this supposed to mean
>>> UNINTERPRETED?
>>
>> Yes. "Free symbol" is in fact the common terminoly in logic and
>> automated reasoning for what formal methods people traditionally have
>> called "unintepreted symbols".
>
> I think my life-long confusion ends here. :)
>
Glad to hear that :)


> (Perhaps the reason for some confusion in terminology stems from the
> terms "freely generated" and "absolutely free algebra".)
>
Well, the two uses of "free" are not unrelated.
For instance, when checking the validity of an atomic formula in a  
free algebra, the free constants of the formula, if any, behave  
exactly like the free generators of the algebra.
But it is probably safer not to delve further into this now :)

Cheers,


Cesare

> Best regards,
>
>   Viktor