Λογική με πολλούς τύπους

Η λογική με πολλούς τύπους (many-sorted logic) μπορεί να αναπαριστά τυπικά την πρόθεση να μη χειριζόμαστε το σύμπαν σαν μια ομογενή συλλογή από αντικείμενα, αλλά να χωρίζεται αυτό με τρόπο παρόμοιο με αυτόν των τύπων του προγραμματισμού με τύπους. Τα συναρτησιακά και τα βεβαιωτικά (assertive) "μέρη του λόγου" της γλώσσας της λογικής ανακλούν αυτόν τον χωρισμό του σύμπαντος με τύπους, ακόμα και στο συντακτικό επίπεδο: η αντικατάσταση και το πέρασμα παραμέτρων μπορούν να γίνουν μόνο με αυτόν τον τρόπο, σεβόμενοι τους "τύπους".

Υπάρχουν πολλοί τρόποι για την τυποποίηση της παραπάνω πρόθεσης: μια λογική με πολλούς τύπους είναι κάθε "πακέτο" πληροφοριών που την ικανοποιεί. Στις περισσότερες περιπτώσεις δίνονται τα εξής:

• ένα σύνολο από τύπους (sorts), S
• μια κατάλληλη γενίκευση της έννοιας της υπογραφής (ή οπλισμού, αγγλ. signature) για να μπορεί να γίνει χειρισμός της επιπλέον πληροφορίας που έρχεται με τους τύπους.

Το πεδίο τότε κάθε δομής αυτής της υπογραφής χωρίζεται σε διακριτά υποσύνολα, ένα για κάθε τύπο.

Αλγεβροποίηση

Η αλγεβροποίηση της λογικής με πολλούς τύπους εξηγείται στο On the Algebraization of Many-sorted Logics από τους Carlos Caleiro και Ricardo Gonçalves. Το βιβλίο γενικεύει την αφηρημένη αλγεβρική λογική στην περίπωση των πολλών τύπων, αλλά μπορεί να χρησιμοποιηθεί και σαν εισαγωγικό υλικό.

Εξωτερικοί σύνδεσμοι

• "Many-sorted Logic" Αρχειοθετήθηκε 2011-07-19 στο Wayback Machine., το 1ο κεφάλαιο στο Lecture Notes on Decision Procedures του Calogero G. Zarba