Για να μετατρέψετε τη λογική πρώτης τάξης σε CNF:
- Μετατροπή σε κανονική μορφή άρνησης. Εξάλειψη επιπτώσεων και ισοδυναμιών: επαναλαμβανόμενη αντικατάσταση με; αντικατέστησε με. …
- Τυποποίηση μεταβλητών. …
- Σκολεμίστε τη δήλωση. …
- Αποθέστε όλους τους καθολικούς ποσοτικούς δείκτες.
- Διανομή OR προς τα μέσα σε AND: αντικαταστήστε επανειλημμένα με.
Τι είναι ο τύπος CNF;
Η
Συνδετική κανονική μορφή (CNF) είναι μια προσέγγιση στη λογική Boole που εκφράζει τύπους ως συνδέσμους προτάσεων με AND ή OR. Κάθε πρόταση που συνδέεται με σύνδεσμο ή AND, πρέπει να είναι είτε κυριολεκτική είτε να περιέχει διαχωρισμό ή τελεστή OR. Το CNF είναι χρήσιμο για την αυτοματοποιημένη απόδειξη θεωρημάτων.
Μπορείτε να μετατρέψετε το DNF σε CNF;
Εάν θέλετε να εισαγάγετε πρόσθετες μεταβλητές, μπορείτε να μετατρέψετε από τη μορφή DNF σε CNF σε πολυωνυμικό χρόνο με χρησιμοποιώντας τον μετασχηματισμό Tseitin. Ο προκύπτων τύπος CNF θα είναι ισοδύναμος με τον αρχικό τύπο DNF: ο τύπος CNF θα είναι ικανοποιητικός εάν και μόνο εάν ο αρχικός τύπος DNF ήταν ικανοποιητικός.
Πώς μπορώ να πάρω CNF;
Απλώς γράψτε τον πίνακα αλήθειας, ο οποίος είναι αρκετά εύκολος να βρεθεί, και συμπεράστε το CNF και το DNF σας. Εάν θέλετε να βρείτε το DNF, πρέπει να δείτε όλες τις σειρές που τελειώνουν με T. Όταν βρείτε αυτές τις γραμμές, λάβετε τις τιμές x, y και z από κάθε αντίστοιχη στήλη. Έτσι, παίρνετε (x∧y∧z)∨(x∧¬y∧¬z)∨(¬x∧y∧¬z)∨(¬x∧¬y∧z).
Πώς μετατρέπετε τον διαχωριστικό σεκανονική μορφή;
Μια σύνθετη πρόταση λέγεται ότι είναι σε διαζευκτική κανονική μορφή, ή DNF, εάν είναι διάζευξη συνδέσμων απλών όρων, και εάν, επιπλέον, κάθε προθετικό η μεταβλητή εμφανίζεται το πολύ μία φορά σε κάθε σύνδεσμο και κάθε σύνδεσμος εμφανίζεται το πολύ μία φορά στη διάζευξη.
