☆ Term Algebras with Length Function and Bounded Quantifier Alternation ☆ <title> <base href="http://www.cs.stanford.edu/~tingz/"> </head> <div class=content> <h1>Term Algebras with Length Function and Bounded Quantifier Alternation <br><br> <a href=""><font style="font-size: 14px;">Ting Zhang</font></a>, <a href="http://theory.stanford.edu/~sipma"><font style="font-size: 14px;">Henny B. Sipma</font></a>, <a href="http://theory.stanford.edu/~zm"><font style="font-size: 14px;">Zohar Manna</font></a> </h1> <br><br> <div class=page> <a name="abstract"></a> <h2>Abstract</h2> <P><BR>Term algebras have wide applicability in computer science. Unfortunately, the decision problem for term algebras has a nonelementary lower bound, which makes the theory and any extension of it intractable in practice. However, it is often more appropriate to consider the <b>bounded class</b>, in which formulae can have arbitrarily long sequences of quantifiers but the quantifier alternation depth is bounded. In this paper we present new quantifier elimination procedures for the first-order theory of term algebras and for its extension with integer arithmetic. The elimination procedures deal with a block of quantifiers of the same type in one step. We show that for the bounded class of at most <i>k</i> quantifier alternations, regardless of the total number of quantifiers, the complexity of our procedures is <i>k</i>-fold exponential (resp. <i>2k</i>-fold exponential) for the theory of term algebras (resp. for the extended theory with integers). <br><br> </div> <div class=page> <a name="download"></a> <h2>Download</h2> <br> Proceeding Version: <A href="papers/tphols04/tphols04.ps"><img border="0" src="//gif/ps.gif"></A> <A href="papers/tphols04/tphols04.pdf"><img border="0" src="//png/pdf.png"></A> <br> Full version: <A href="papers/tphols04/tphols04_full.ps"><img border="0" src="//gif/ps.gif"></A> <A href="papers/tphols04/tphols04_full.pdf"><img border="0" src="//png/pdf.png"></A> <br> Talk slides: <A href="papers/tphols04/tphols04_talk.ps"><img border="0" src="//gif/ps.gif"></A> <A href="papers/tphols04/tphols04_talk.pdf"><img border="0" src="//png/pdf.png"></A> <br> Talk slides (Lite): <A href="papers/tphols04/tphols04_talk_lite.ps"><img border="0" src="//gif/ps.gif"></A> <A href="papers/tphols04/tphols04_talk_lite.pdf"><img border="0" src="//png/pdf.png"></A> </div>  <div class="footer"> <a href="index.html">Home</a> <a href="papers/papers_by_category.html">By Category</a> <a href="papers/papers_by_year.html">By Year</a> <a href="papers/papers_by_topic.html">By Topic</a> </div> </body> </html>