R-calculus is a formal inference system of logical connectives and quantifiers, containing one axiom and six inference rules. It is designed for verifying the process of scientific discovery by deleting those principles of scientific theories which contradict empirical evidences. Two examples are presented to show that the discovery processes of Einstein’s special theory of relativity and Darwin’s theory of evolution of species can be formally verified by using R-calculus. Einstein’s solution is the only and correct choice, but Darwin’s solution is one of the three logically correct choices which may be a reason of the controversies over Darwin’s theory.