Footnotes

 

(1)

The acronym has been fixed, but its interpretation is still open to discussion: the `C' might stand for `Common', the `A' might stand for `Axiomatic'...  

(2)

The acronym has been fixed, but its interpretation is still open to discussion: the `C' might stand for `Common', the `A' might stand for `Axiomatic'...  

(3)

The notion of explicitly-sorted term is redundant in the many-sorted framework, but becomes significant when subsorts are introduced in a later section.