Προηγούμενη Πάνω Επίπεδο Επόμενη Περιεχόμενα
Επόμενη: Αντικατάσταση Πάνω Επίπεδο: Ανάλυση Προηγούμενη: Δυνατότητα Υπολογισμού (Computability)

4.2 Αποδεικτικές Διαδικασίες

Ονομάζουμε αποδεικτική διαδικασία κάθε μέθοδο που χρησιμοποιείται για ν' αποδείξουμε ότι ένας τύπος tex2html_wrap_inline660 είναι λογική συνέπεια κάποιου συνόλου τύπων tex2html_wrap_inline1050. Συνήθως, οι τύποι στο tex2html_wrap_inline1050 ονομάζονται υποθέσεις (premises) και ο tex2html_wrap_inline660 συμπέρασμα (conclusion) της απόδειξης.

Μια απόδειξη αποτελείται από ένα ή περισσότερα βήματα, σε καθένα από τα οποία παράγεται ένας νέος τύπος από τις υποθέσεις και τους προηγούμενα παραγμένους τύπους. Κάθε βήμα της απόδειξης βασίζεται σε κάποιους κανόνες παραγωγής (derivation rules). Μια διαδικασία απόδειξης που συνήθως χρησιμοποιείται στα μαθηματικά, είναι η modus ponens. Σύμφωνα με τη διαδικασία αυτή, από το σύνολο των τύπων tex2html_wrap_inline1260 μπορούμε να πάρουμε τον τύπο tex2html_wrap_inline670. Μπορούμε να συνδέσουμε πολλούς κανόνες modus ponens μαζί, ώστε να έχουμε μια απόδειξη. Αν ο τύπος tex2html_wrap_inline660 μπορεί να παραχθεί από το tex2html_wrap_inline1050 με χρήση κάποιων κανόνων παραγωγής, λέμε ότι ο tex2html_wrap_inline660 είναι θεώρημα του υπολογισμού από το tex2html_wrap_inline1050 και των συγκεκριμένων κανόνων παραγωγής.

Η ορθότητα (soundness) και η πληρότητα (completeness) είναι δυο επιθυμητές ιδιότητες των αποδεικτικών διαδικασιών. Μια αποδεικτική διαδικασία ονομάζεται ορθή (sound), όταν επιτρέπει μόνο λογικές συνέπειες να παράγονται από τις υποθέσεις. Ονομάζεται πλήρης (complete), όταν είναι ικανή να παράγει όλες τις λογικές συνέπειες των υποθέσεων. Ο modus ponens είναι ορθός, αλλά όχι πλήρης.



Εργαστήριο Γλωσσών Προγραμματισμού και Τεχνολογίας Λογισμικού
Mon Apr 5 16:25:43 EEST 1999