And in 1963 Alan Robinson suggested the idea of resolution theorem proving, in which one constructs ¬ theorem ∨ axioms , then typically writes this in conjunctive normal form and repeatedly applies rules like ( ¬ p ∨ q) ∧ (p ∨ q)  q to try to reduce it to False , thereby proving given axioms that theorem is True .

In the late 1970s it was noted that by evaluating PowerMod[a, n - 1, n]  1 for several random integers a one can with high probability quickly deduce PrimeQ[n] . … And in the 1980s many such randomized algorithms were invented, but by the mid-1990s it was realized that most did not require any kind of true randomness, and could readily be derandomized and made more predictable. … And the same is true when one picks unique IDs, say to keep track of repeat web transactions with a low probability of collisions.