Teoremi nella logica del primo ordine

I teoremi nella logica del primo ordine sono funzioni logiche deducibili dagli assiomi. A partire da un insieme di assiomi di riferimento è possibile ottenere delle conclusioni seguendo un ragionamento logico deduttivo. Mentre gli assiomi sono i componenti primarie di una base di conoscenza nella logica del primo ordine in quanto definiscono la rappresentazione della realtà. I teoremi sono, invece, componenti secondarie poiché derivano dagli assiomi e dal ragionamento per deduzione. Ad esempio, "se x è fratello di y, allora y è fratello di x". Questo teorema può essere scritto nel seguente modo:

∀ x,y Fratello(x,y) ⇔ Fratello (y,x)

Efficienza computazionle. I teoremi sono componenti secondarie della rappresentazione della conoscenza ma svolgono un'importante funzione nelle basi di conoscenza poiché permettono di ridurre il carico di lavoro computazionale dell'algoritmo. Il teorema consente di giungere subito a una conclusione senza dover rielaborare tutti i passaggi logici degli assiomi.