Cálculo proposicional, (ou cálculo sentencial), é um sistema formal no qual as formulas apresentam proposições que podem ser formadas pela combinação de proposições, usando conectivos lógicos e um sistema de regra de derivação. Quando o sistema tem o propósito de ser um sistema lógico, as expressões devem ser interpretadas como asserções matemáticas, e as regras, conhecidas como regras de inferências, normalmente são preservadoras da verdade. Nessa configuração, as regras podem ser então usadas para derivar "inferir" fórmulas representado asserções verdadeiras.

Exemplo ilustrado no exercício resolvido