# Is there a simple algorithm for proof search on CoC?

Given the usual Calculus of Constructions with an extra primitive, _, that stands for "attempt to fill this location in a way that type-checks", is there any simple/elegant algorithm capable of solving this problem for a large class of terms? For example, given the term below:

λ (N : Type)
λ (S : {x : N} N)
λ (Z : N)
λ (A : {x : N} Type)
λ (B : {x : N} (A x))
λ (C : {x : (A (S (S (S Z))))} Type)
(C _)


The algorithm would replace _ by (B (S (S (S Z)))), as it is the only substitution that makes the resulting term well-typed. I'm specifically looking for keywords / references, as I believe this is a pretty well-researched subject (given that most theorem provers feature proof search), but I've never seen an algorithm described in a simpler setup (like plain CoC).