Skolemization and Equality

Equality is a fundamental concept in mathematics, logic, and everyday life - whether we use different terms to represent the same number (such as two plus two and four) or different names for the same person. In research, equality is particularly important in proofs and automated theorem proving. A key method in logic is Skolemization, where specific variables in formulas are replaced by new function symbols (Skolem functions) to simplify proofs. While Skolemization is well- studied, the reverse process, called de-Skolemization, poses challenges, especially when equality is part of the proofs. This reversal is however essential to transform machine- generated proofs into clear, human-readable formats. Our research project aims to develop methods for efficiently removing Skolem functions in proofs involving equality. This will not only provide new theoretical insights into the complexity of de-Skolemization but also advance practical applications in automated reasoning. The results could contribute to making computer-based proof systems more understandable and effective.