Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

LICS

2003

IEEE

2003

IEEE

We show that the ﬁrst-order theory of structural subtyping of non-recursive types is decidable, as a consequence of a more general result on the decidability of term powers of decidable theories. Let Σ be a language consisting of function symbols and let C (with a ﬁnite or inﬁnite domain C) be an L-structure where L is a language consisting of relation symbols. We introduce the notion of Σ-term-power of the structure C, denoted PΣ(C). The domain of PΣ(C) is the set of Σ-terms over the set C. PΣ(C) has one term algebra operation for each f ∈ Σ, and one relation for each r ∈ L deﬁned by lifting operations of C to terms over C. We extend quantiﬁer elimination for term algebras and apply the Feferman-Vaught technique for quantiﬁer elimination in products to obtain the following result. Let K be a family of L-structures and KP the family of their Σ-termpowers. Then the validity of any closed formula F on KP can be effectively reduced to the validity of some closed f...

Related Content

Added |
05 Jul 2010 |

Updated |
05 Jul 2010 |

Type |
Conference |

Year |
2003 |

Where |
LICS |

Authors |
Viktor Kuncak, Martin C. Rinard |

Comments (0)