Calculus ratiocinator

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 starting with the Begriffsschrift, and subsequent advances in proof theory.