A Free Variable Version of the First-Order Predicate Calculus. - Martin Davis; Ronald Fechter (J. Log. Comput., 1991)