Unul dintre primele si cele mai importante modele de reprezentare a cunostintelor in inteligenta artificiala este logica simbolica. Logica simbolica a fost dezvoltata de logicieni ca o metoda formala de rationament, in principal in domeniul matematicii, cel mai raspandit model logic fiind logica cu predicate de ordinul I.
Logica cu predicate de ordinul I a fost folosita pentru prima data ca metoda de reprezentare a cunostintelor in inteligenta artificiala in programul de demonstrare a teoremelor al lui Gilmore si in programul "The Logic Theorist" al lui Newell, Shaw si Simon [1963]. Programul lui Gilmore pentru demonstrarea teoremelor in logica cu predicate de ordinul I s-a bazat pe rezultatele teoretice importante ale lui Herbrand [Chang,Lee,1973] care au stabilit conditiile in care o multime de formule (clauze) este inconsistenta. in 1965 Robinson, plecand de la rezultatele lui Herbrand, a propus o metoda mult mai eficienta de stabilire a inconsistentei unei formule: rezolutia. Aceasta metoda si diversele ei rafinari ulterioare au devenit abordarea preferentiala a celor mai multe demonstratoare de teoreme dezvoltate pana in prezent.
Utilizarea logicii simbolice ca model de reprezentare a cunostintelor in inteligenta artificiala este importanta deoarece ofera o abordare formala a rationamentului, cu fundamente teoretice riguroase. Formalismul logic permite derivarea unor cunostinte noi, plecand de la cele existente, pe baza deductiei si a demonstrarii teoremelor. Acest lucru faciliteaza automatizarea proceselor de rationament si executia inferentelor corecte si logic valide. Pe de alta parte, logica simbolica este suficient de expresiva si flexibila pentru a permite reprezentarea cu acuratete a cunostintelor problemei de rezolvat.
