egzisztenciális példányosítás következtetési szabály

Kapcsolódó fogalmak: 
skolemizáció
Kapcsolódó fogalmak: 
Skolem-konstans
Rövid szöveges bemutatás: 
Az egzisztenciális példányosítás következtetési szabály egy olyan folyamat melynek során általános szabályokat névvel látunk el. Feltétele a folyamatnak, hogy az általános szabályban használt név jelző ne szerepeljen másutt a tudásbázisban. Ezt a név jelzőt skolem-konstansnak nevezik. Például tudjuk, hogy LÉTEZIK-x Megesz(x, Csoki), akkor a példányosítás után írhatom azt, hogy Megesz(A1, Csoki), így kihagyva belőle az egzisztenciális kvantort, helyettesítve azt egy skolem-konstansal. Ezáltal könnyen tudunk hivatkozni erre a konstansra másutt. Tehát a lényeg az, hogy elhagyjuk az egzisztenciális kvantort és beírunk egy skolem-konstasnt. Erre a konstansra tudjuk, hogy igaz lesz az állítás és csakis erre a konstansra, más objektumra nem. Ilyen skolem-konstans például a PI.