Calculus ratiocinator is Leibniz's term for a formal logical system, which did not exist in his lifetime. A completely formal, calculational form of logical inference is realized in modern developments of mathematical logic; see also proof theory.
