- problem Γ ok? （コンテキスト Γ は正しいか？）
- judgement Γ ok （コンテキスト Γ は正しい）
- problem Γ |- t ok? （項 t は、コンテキスト Γ で解釈できるか？）
- judgementm Γ |- t ok （項 t は、コンテキスト Γ で解釈できる）
- problem Γ |- ?t : A （型 A である項 ?t を求めよ）
- judgement Γ |- t : A （項 t は型 A である）
- problem Γ |- t : ?A （項 t の型を求めよ）
- judgement Γ |- t : A （再度：項 t は型 A である）
- problem Γ |- t : A ok? （項 t は型 A であるか？）
- judgement Γ |- t : A （三度目：項 t は型 A である）
- problem Γ |- A ok? （型 A である項が存在するか？）
- judgement Γ |- A ok （型 A である項が存在する）
- existential judgement Γ |- A （型 A である項が存在する）
代表的かつ重要な問題：
- 型検証問題： problem Γ |- t : A ok? （項 t は型 A であるか？）
- 型推論問題： problem Γ |- t : ?A （項 t の型を求めよ）
- 項構成問題： problem Γ |- ?t : A （型 A である項 ?t を求めよ）
ソルバーソフトウェア：
- 型検証問題 → 証明検証系
- 型推論問題 → 結論抽出系
- 項構成問題 → 自動証明系
