En lógica matemática procedimiento deductivo que permite realizar inferencias sin referirse al significado de los signos utilizados. Predomina en él un punto de vista sintáctico de forma tal que unas expresiones se deriven de otras merced a un proceso estrictamente mecánico.