
Skolemization, with Herbrand's theorem, underpins automated theorem proving and various transformations in computer science and mathematics. Skolemization removes strong quantifiers by introducing new function symbols, enabling efficient proof search algorithms. We characterize intermediate first-order logics that admit standard (and Andrews) Skolemization. These are the logics that allow classical quantifier shift principles. For some logics not in this category, innovative forms of Skolem functions are developed that allow Skolemization. Moreover, we analyze predicate intuitionistic logic with quantifier shift axioms and demonstrate its Kripke frame-incompleteness. These findings may foster resolution-based theorem provers for non-classical logics. This article is part of a larger project investigating Skolemization in non-classical logics.
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, FOS: Mathematics, Mathematics - Logic, Logic (math.LO), Logic in Computer Science (cs.LO)
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, FOS: Mathematics, Mathematics - Logic, Logic (math.LO), Logic in Computer Science (cs.LO)
| citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
