  Since Val Tannen's pioneer work on the combination of simply-typed
lambda-calculus and first-order rewriting (LICS'88), many authors have
contributed to this subject by extending it to richer typed lambda-calculi and
rewriting paradigms, culminating in calculi like the Calculus of Algebraic
Constructions. These works provide theoretical foundations for type-theoretic
proof assistants where functions and predicates are defined by oriented
higher-order equations. This kind of definitions subsumes induction-based
definitions, is easier to write and provides more automation. On the other
hand, checking that user-defined rewrite rules are strongly normalizing and
confluent, and preserve the decidability of type-checking when combined with
beta-reduction, is more difficult. Most termination criteria rely on the term
structure. In a previous work, we extended to dependent types and higher-order
rewriting, the notion of ``sized types'' studied by several authors in the
simpler framework of ML-like languages, and proved that it preserves strong
normalization. The main contribution of the present paper is twofold. First, we
prove that, in the Calculus of Algebraic Constructions with size annotations,
the problems of type inference and type-checking are decidable, provided that
the sets of constraints generated by size annotations are satisfiable and admit
most general solutions. Second, we prove the later properties for a size
algebra rich enough for capturing usual induction-based definitions and much
more.
