Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized delta-Rule but Without Skolemization

this paper including all proofs. We discuss how to analytically prove first-order theorems in contexts where Skolemization is not appropriate. Skolemization has at least three problematic aspects. 1. Skolemization enrichs the signature or introduces higher-order variables. Unless special care is taken, this may introduce objects into empty universes and change the notion of term-generatedness or Herbrand models. Above that, the Skolem functions occur in answers to goals or solutions of constraint