Логическите формули се строят от атомарни формули и логическата константа true чрез операциите отрицание, конюнкция, дизюнкция, импликация, еквиваленция и поставяне на квантори (за общност или за съществуване). Дава се индуктивна дефиниция за вярностна стойност на формула в дадена структура при дадена оценка на променливите. Тази стойност може да бъде 0 или 1. Когато тя е 1, казваме, че формулата е вярна в дадената структура при дадената оценка. Ако една формула е вярна  в дадена структура при всяка оценка на променливите, казваме, че формулата е тъждествено вярна в тази структура, а ако е вярна в структурата при поне една оценка на променливите, казваме, че формулата е изпълнима в структурата. Една формула се нарича тъждествено вярна, ако тя е тъждествено вярна във всяка структура.
    Дефинират се конюнкция и за дизюнкция на краен списък от формули и се дава условие за вярност на така дефинираните конюнкции и дизюнкции. Произволна хорнова цел се представя чрез конюнкцията на нейните членове, а произволна хорнова клауза - чрез импликация от конюнкцията на членовете на тялото към главата. Една хорнова програма се представя чрез конюнкцията на импликациите, представящи нейните клаузи (ако формулата A представя в този смисъл дадена хорнова програма P, а формулата B е конюнкция на членовете на дадена хорнова цел G, то G е изпълнима при P точно тогава, когато B е изпълнима във всяка структура, в която е тъждествено вярна A, и G е тъждествено изпълнена при P точно тогава, когато B е тъждествено вярна във всяка структура, в която е тъждествено вярна A).
    Индуктивно се дефинират множество VAR(A) на свободните променливи и множество BVAR(A) на свързаните променливи на коя да е формула A. Форнулите с празно множество на свободните променливи се наричат затворени. Универсално и екзистенциално затваряне на една формула се извършва като пред нея се поставят съответно квантори за общност или квантори за съществуване по отношение на всичките й свободни променливи. Дефинира се какво значи една затворена формула да е вярна в дадена структура. Въпросите дали дадена хорнова цел е изпълнима или тъждествено изпълнена при дадена хорнова програма се свеждат към въпроси за тъждествена вярност на съответни затворени формули.