A Herbrand bázis a Herbrand univerzum kiterjesztése. A bázis tartalmazza az univerzumban előállt összes alapkifejezés és az eredeti vizsgált kijelentésben előforduló összes predikátumszimbólum minden párosítását. Az előállt párosítások továbbra sem tartalmazhatnak változót.