A complete, nonredundant algorithm for reversed Skolemization

From MaRDI portal





The paper deals with the problem of reversing Skolemization and presents several algorithms to accomplish wholly this process. All the algorithms are written in a common language form. It is proved that the first of the algorithms is terminating, sound and non-redundant, but not complete. Therefore, the algorithm is preprocessed to the version which already has the properties of halting, soundness and completeness. From these two algorithms a third one is constructed as their combination, and its elementary properties like above are proved. Finally, the objective algorithm is presented for solving the overall process of de- Skolemization, and its termination, soundness, non-redundancy and completeness are proved.











This page was built for publication: A complete, nonredundant algorithm for reversed Skolemization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1059063)