Επόμενη: Ενοποίηση Πάνω Επίπεδο: Ανάλυση Προηγούμενη: Αποδεικτικές Διαδικασίες

4.3 Αντικατάσταση

Πρόκειται για τη διαδικασία αντικατάστασης μεταβλητών μιας έκφρασης από τύπους. Χρησιμοποιούμε τη λέξη έκφραση (expression) για ν' αναφερόμαστε στους όρους, στα λεκτικά στοιχεία καθώς και στις διαζεύξεις ή συζεύξεις λεκτικών στοιχείων. Για παράδειγμα, μπορούμε ν' αντικαταστήσουμε τη μεταβλητή x της πρότασης με τον όρο g(c) και να πάρουμε την πρόταση .

Μια αντικατάσταση είναι ένα πεπερασμένο σύνολο της μορφής

όπου x_i είναι διακεκριμένες μεταβλητές και t_i είναι όροι. Κάθε x_i/t_i ονομάζεται δέσμευση (binding) του x_i. Μια αντικατάσταση θα ονομάζεται βασική αντικατάσταση (ground substitution), αν κάθε όρος t_i είναι βασικός.

Για μια έκφραση E και μια αντικατάσταση για τις μεταβλητές της E, η νέα έκφραση που λαμβάνεται από την εφαρμογή της στην E ονομάζεται στιγμιότυπο (instance) της E στη και συμβολίζεται . Αν, επιπλέον, η είναι βασική θα ονομάζεται βασικό στιγμιότυπο (ground instance). Αν είναι ένα πεπερασμένο σύνολο προτάσεων, θα συμβολίζουμε με το σύνολο . Αν είναι δύο αντικαταστάσεις, η αντικατάσταση είναι το αποτέλεσμα της εφαρμογής της στην έκφραση .