Herbrandovo univerzum

Logika nekonečná spočetná množina výrazů utvořených z individuových konstant a funktorů, obsažených v dané formuli. Herbrandovo univerzum tvoří univerzální nosič pro sémantické interpretace formulí dané množiny, používaný napříkladjako obecný základ pro automatické deduktivní mechanismy ve výpočetní technice.