A note on assumptions about Skolem functions (Q1904405)

The paper presents a sharpened Skolem theorem for first-order logic. This optimized skolemization technique does not produce an equivalent proposition, but it preserves satisfiability, which is enough for its use in refutational automated theorem-proving . This optimized skolemization can be decomposed into a transformation of the proposition to be refuted, followed by a standard skolemization. It generalizes optimized skolemization techniques known in special fields such as many-sorted first-order logic and modal logic.