Reglas de inferencia con cuantificadores

• devuelve el resultado de aplicar la substitución en la sentencia
  
• eliminación del universal: para cualquier sentencia , variable v y término sin variables (ground term)
  
• eliminación del existencial: para cualquier sentencia , variable v y constante k que no aparece en ningún otro lugar de la KB
  
• introducción del existencial: para cualquier sentencia , variable v que no aparece en , y término sin variables g (ground term) que aparece en