Preparing Logic for Machines: PNF and Skolemization

In the world of automated theorem proving, raw logical formulas are often too messy for algorithms to handle directly. Before a computer can prove a theorem, we usually need to standardize the format. Today, we look at two critical transformation ste...