Abstract
In this paper an alternative Skolemization method is introduced that for
a large class of formulas is sound and complete with respect to intuitionistic
logic. This class extends the class of formulas for which standard
Skolemization is sound and complete and includes all formulas in which
all strong quantifiers are existential. The method makes use of an existence
predicate first introduced by Dana Scott.
a large class of formulas is sound and complete with respect to intuitionistic
logic. This class extends the class of formulas for which standard
Skolemization is sound and complete and includes all formulas in which
all strong quantifiers are existential. The method makes use of an existence
predicate first introduced by Dana Scott.
| Original language | English |
|---|---|
| Pages (from-to) | 269-295 |
| Number of pages | 27 |
| Journal | Annals of Pure and Applied Logic |
| Volume | 142 |
| Issue number | (1-3) |
| Publication status | Published - 2006 |
Keywords
- Skolemization
- eSkolemization
- Herbrand’s theorem
- intuitionistic logic
- Kripke models
- existence predicate