Sixth Annual IEEE Symposium on

Logic in Computer Science (LICS 1991)

Paper: Term declaration logic and generalised composita (at LICS 1991)

Authors: Peter Aczel


A generalization of a version of order-sorted logic and an abstract axiomatic setting for the treatment of substitution are given. The two ideas are shown to be related, an equational specification of term declaration logic being a presentation of a finitary generalized composition. The automatic approach to substitution is compared with some other approaches. The relationship between algebraic theories and standard equational logic is reviewed. One of the aims is to lay the foundations for a generalization of these connections to connections between term declaration logic and finitary generalized composita and a suitable generalization of algebraic theories


    author = 	 {Peter Aczel},
    title = 	 {Term declaration logic and generalised composita},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {22--30},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}