Logic in Computer Science (LICS 1988)

Paper: Complete axiomatizations of the algebras of finite, rational and infinite trees (at LICS 1988)

Authors: Michael J. Maher

Abstract

Complete axiomizations for the algebras of infinite trees and infinite trees are presented. The axiomizations are parameterized by the alphabet of function symbols for both the finite trees and infinite trees. There are two main cases, depending on whether the number of function symbols is finite or infinite. In the former case an extra axiom is necessary to obtain completeness. The method of proof is an elimination of quantifiers. Although a full elimination of quantifiers is not possible, the method forms the basis of decision procedures for the theories of the corresponding algebras. As a corollary to the results in infinite trees, the elementary equivalence of the algebra of rational trees and the algebra of infinite trees is obtained

BibTeX

  @InProceedings{Maher-Completeaxiomatizat,
    author = 	 {Michael J. Maher},
    title = 	 {Complete axiomatizations of the algebras of finite, rational and infinite trees },
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {348--357},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }