Nella teoria della progettazione di una base di dati gli Assiomi di Armstrong, formalizzati nel 1974, costituiscono un insieme di regole che permettono di comprendere le implicazioni logiche che intercorrono tra dipendenze funzionali.
Gli assiomi di Armstrong sono di Riflessività, Aumento e Transitività. In tutti i casi si suppone di considerare uno schema di relazione con un insieme di attributi , con l'insieme universale di attributi, ed un insieme di dipendenze funzionali che implichino solo attributi di .
Se allora è logicamente implicato da .
Se vale e è un qualunque sottoinsieme di allora .
Se e allora .
Oltre agli Assiomi di Armstrong esistono altre regole di inferenza addizionali per derivazioni di una dipendenza funzionali:
Dato uno schema e un insieme di attributi , la chiusura di X rispetto a F, denotata con X+, è l'insieme di attributi:
Si arriva così al teorema fondamentale che per determinare se sia derivabile attraverso gli Assiomi di Armstrong, è risolvibile calcolando la chiusura dell'insieme X, formalmente:
Dato uno schema , siano X e Y insieme di attributi contenuti in T:
Algoritmo per il calcolo della chiusura di un insieme di attributi X rispetto ad F (X+).
Begin
X+ := X;
while X+ è cambiato do
for each with and do
End
Sia dato uno schema , con T={A,B,C,D,E,G,H,I} e . Inoltre, sia il valore della variabile X+ alla fine della j-esima iterazione del ciclo while:
Sia X = BCE:
L'algoritmo termina con BCE+=T (BCE superchiave).
Gli assiomi di Armstrong sono corretti quando ogni dipendenza funzionale derivata attraverso l'applicazione degli assiomi è implicata logicamente:
Gli assiomi di Armstrong sono completi quando ogni dipendenza funzionale implicata logicamente è derivata attraverso l'applicazione degli assiomi: