EVA STAR Trefferanzeige

Volltext Volltext.pdf1.pdf (381 KB)
URN (für Zitat) http://nbn-resolving.org/urn:nbn:de:swb:90-AAA404967
Titel Ramified higher-order unification.
Autor Goubault-Larrecq, Jean
Institution Fakultät für Informatik (INFORMATIK)
Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Dokumenttyp Buch
Jahr 1996
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,31.)
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$.