KIT | KIT-Bibliothek | Impressum
Open Access Logo
§
Volltext
URN: urn:nbn:de:swb:90-AAA404967

Ramified higher-order unification

Goubault-Larrecq, Jean

Abstract:

While unification in the simple theory of types (a.k.a.\
higher-order logic) is undecidable, we show that unification in the
pure ramified theory of types with integer levels is decidable. But
the pure ramified theory of types cannot express even the simplest
formulas of logic. The impure ramified type theory has an
undecidable unification problem even at order 2. However, the
decidability result for the pure subsystem indicates that
unification should fail to terminate less often than general
higher-order unification. We present applications to two expressive
subsystems of second-order Peano arithmetic, $\mbox{ACA}_0$ and
$\Pi^1_{k}\mbox{-CA}_0$.


Zugehörige Institution(en) am KIT Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Jahr 1996
Sprache Englisch
Identifikator KITopen ID: 40496
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,31.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page