Per concludere la parte relativa alla logica proposizionale classica, si presenta un esempio in cui i concetti visti finora vengono utilizzati per verificare la progettazione di un semplice circuito logico.
Si vuole progettare un circuito logico che implementi un half adder. Esso ha due input, $a$ e $b$, e due output, sum (la somma) e carry (il riporto):
Il suo comportamento è specificato da due funzioni booleane, chiamate anch’esse sum e carry poichè indicano i valori degli omonimi output al variare di a e b. Tali funzioni sono descritte dalla seguente tavola di verità:
Per i teoremi di completezza funzionale, si sa che è possibile scriere delle formule logiche che descrivano il comportamento di queste due funzioni booleane.
Un modo per ottenere tali formule sarebbe costruire le DNF / CNF come indicato dalle dimostrazioni dei teoremi di completezza funzionale; in alternativa, si può ottenere una formula più semplice ed espressiva osservando la tavola di verità e scegliendo, in base a essa, i connettivi più opportuni:
$$ \text{HA}_\text{SPEC}(a, b, sum, carry)=(carry\lrarr a\land b)\land(sum\lrarr \neg (a\lrarr b)) $$
Infatti:
Osservazione: Tipicamente, una funzione booleana viene rappresentata da una formula nella quale gli argmoenti della funzione corrispondono a variabili proposizionali, mentre il risultato è dato direttamente dal valore di verità assunto dalla formula. La formula appena mostrata, invece, contiene variabili proposizionali sia per gli input che per gli output, e descrive le funzioni booleane $sum$ e $carry$ nel senso che è verificata se e solo se la combinazione di valori di input e output è “corretta”. Così facendo, si possono descrivere più funzioni booleane con una sola formula.
Le componenti che verranno utilizzate per realizzare il circuito (il quale, se progettato correttamente, dovrà avere lo stesso comportamento delle funzioni booleane riportate sopra) sono le seugenti porte logice:
che sono descrittte dalle formule
