Αριθμητική υπολοίπων

Από τη Βικιπαίδεια, την ελεύθερη εγκυκλοπαίδεια
Μετάβαση σε: πλοήγηση, αναζήτηση
Ο χρόνος περνά σε αυτό το ρολόι χρησιμοποιώντας την αριθμητική modulo 12.

Στα μαθηματικά, η αριθμητική υπολοίπων είναι ένα σύστημα αριθμητικής για ακέραιους αριθμούς, όπου οι αριθμοί "αναδιπλώνονται" έως την επίτευξη μιας ορισμένης τιμής— συντελεστής (πληθυντικός moduli). Η σύγχρονη προσέγγιση για την αριθμητική υπολοίπων αναπτύχθηκε από τον Καρλ Φρίντριχ Γκάους, στο βιβλίο του Disquisitiones Arithmeticae, που δημοσιεύθηκε το 1801.

Μία γνωστή χρήση της αριθμητικής υπολοίπων είναι το ρολόι 12 ωρών, κατά το οποίο η μέρα χωρίζεται σε δύο 12-ωρες περιόδους. Αν τώρα η ώρα είναι 7:00, τότε σε 8 ώρες αργότερα θα είναι 3:00. Επιπλέον, το συνηθισμένο θα ήταν ο μεταγενέστερος χρόνος να πρέπει να είναι 7 + 8 = 15, αλλά αυτό δεν είναι ορθό, διότι η ώρα του ρολογιού "αναδιπλώνεται" κάθε 12 ώρες: σε ένα 12-ωρο, δεν υπάρχει "η ώρα 15:00". Ομοίως, αν το ρολόι ξεκινά στις 12:00 (το μεσημέρι) και έχουν παρέλθει 21 ώρες, τότε ο χρόνος θα είναι 9:00 την επόμενη μέρα, αντί για 33:00. Επειδή η ώρα ξεκινά ξανά από την αρχή αφού φτάσει στις 12:00, αυτό είναι αριθμητική modulo 12. Σύμφωνα με τον ορισμό παρακάτω, το 12 είναι ισότιμο όχι μόνο με το 12, αλλά και με το 0, έτσι ώστε ο χρόνος που ονομάζεται "12:00" θα μπορούσε επίσης να ονομάζεται "0:00", αφού το 12 είναι ισότιμο με το 0 modulo 12.

Σχέση Ισοτιμίας[Επεξεργασία | επεξεργασία κώδικα]

Αυτή η ενότητα είναι για το ( mod n ) συμβολισμό. Για τη δυαδική mod λειτουργία , δείτε τη λειτουργία modulo .

Η αριθμητική υπολοίπων μπορεί να αντιμετωπιστεί στα μαθηματικά με την εισαγωγή μιας σχέσης ισοτιμίας στους ακέραιους αριθμούς που είναι συμβατή με τις πράξεις στους ακέραιους αριθμούς: πρόσθεση, αφαίρεση, και πολλαπλασιασμό. Για έναν θετικό ακέραιο n, δύο ακέραιοι a και b είναι ισοδύναμοι modulo n και γράφουμε:

εάν η διαφορά τους ab είναι ένα ακέραιο πολλαπλάσιο του n (ή το n διαιρεί το ab). Ο αριθμός n ονομάζεται συντελεστής της ισοτιμίας.

Για παράδειγμα,

επειδή 38 − 14 = 24, το οποίο είναι πολλαπλάσιο του 12.

Ο ίδιος κανόνας ισχύει και για αρνητικές τιμές:

Aντίστοιχα, ab mod n μπορεί επίσης να εξηγηθεί, επιβεβαιώνοντας ότι τo υπόλοιπο της διαίρεσης των a και b από το n είναι το ίδιο. Για παράδειγμα:

επειδή και το 38 και το 14 έχουν το ίδιο υπόλοιπο, το 2, όταν διαιρούνται από το 12. Επίσης το 38 − 14 = 24 είναι ένα ακέραιο πολλαπλάσιο του 12, το οποίο συμφωνεί με τον προηγούμενο ορισμό της σχέσης ισοτιμίας.

Μια παρατήρηση στο συμβολισμό: Επειδή είναι συνηθισμένο να θεωρούμε διάφορες σχέσεις ισοτιμίας για διαφορετικούς συντελεστές συγχρόνως, ο συντελεστής έχει ενσωματωθεί στο συμβολισμό. Παρά τον τριαδικό συμβολισμό, η σχέση ισοτιμίας για έναν δεδομένο συντελεστή είναι δυαδική. Αυτό θα ήταν σαφέστερο, εάν χρησιμοποιούσαμε τον συμβολισμό an b, αντί του συνηθισμένου παραδοσιακού συμβολισμού.

Οι ιδιότητες που καθιστούν αυτή τη σχέση, μια σχέση ισοτιμίας (που σέβεται την πρόσθεση, την αφαίρεση και τον πολλαπλασιασμό) είναι οι ακόλουθες.

Εάν

και

τότε:

Οι δύο παραπάνω ιδιότητες θα ίσχυαν ακόμα αν η θεωρία είχε επεκταθεί για να περιλάβει όλους τους πραγματικούς αριθμούς, δηλαδή αν οι δεν ήταν κατ' ανάγκη όλοι ακέραιοι. Η επόμενη ιδιότητα όμως, δεν θα ίσχυε αν οι μεταβλητές αυτές δεν ήταν όλες ακέραιοι αριθμοί:

Υπόλοιπα[Επεξεργασία | επεξεργασία κώδικα]

Η έννοια της αριθμητικής υπολοίπων αφορά το υπόλοιπο στην Ευκλείδεια διαίρεση. Η λειτουργία εύρεσης του υπολοίπου μερικές φορές αναφέρεται ως λειτουργία modulo και συμβολίζεται με το "mod" που χρησιμοποιείται ως ένθετος τελεστής. Για παράδειγμα, το υπόλοιπο της διαίρεσης του 14 από το 12 συμβολίζεται με 14 mod 12, καθώς αυτό το υπόλοιπο είναι 2, έτσι έχουμε 14 mod 12 = 2.

Η ισοτιμία, με την ένδειξη "", ακολουθούμενη από το "mod" ανάμεσα στις παρενθέσεις, σημαίνει ότι ο τελεστής "mod", εφαρμοσμένος και στα δύο μέλη, δίνει το ίδιο αποτέλεσμα. Αυτό είναι:

είναι ισοδύναμη με την

Η θεμελιώδης ιδιότητα του πολλαπλασιασμού στην αριθμητική υπολοίπων μπορεί να γραφεί έτσι:

ή ισοδύναμα,

Στην επιστήμη των υπολογιστών, είναι το υπόλοιπο του τελεστή, που συνήθως αναφέρεται είτε με το "%" (για παράδειγμα, στις C, C++, Java, JavaScript, Perl, Python και Scala) ή "mod" (για παράδειγμα, σε Pascal, BASIC, SQL, Haskell, ABAP, και MATLAB), με εξαιρέσεις (για παράδειγμα, το Excel). Οι εν λόγω τελεστές συχνά προφέρονται ως "mod", αλλά αυτό συγκεκριμένα είναι ένα υπόλοιπο που υπολογίζεται (αφού στη C++ ένας αρνητικός αριθμός θα επιστραφεί αν το πρώτο επιχείρημα είναι αρνητικό, και στη Python ένας αρνητικός αριθμός θα επιστραφεί αν το δεύτερο επιχείρημα είναι αρνητικό). Η λειτουργία modulo αντί mod, όπως 38 ≡ 14 (modulo 12) μερικές φορές χρησιμοποιείται για να δείξει το κοινό υπόλοιπο και όχι ένα υπόλοιπο (για παράδειγμα, στη Ruby). Για λεπτομέρειες σχετικά με τις ειδικές λειτουργίες που ορίζονται σε διαφορετικές γλώσσες, ανατρέξτε στην λειτουργία modulo της σελίδας.

Συστήματα Υπολοίπων[Επεξεργασία | επεξεργασία κώδικα]

Κάθε κλάση υπολοίπων modulo n μπορεί να εκπροσωπείται από οποιοδήποτε από τα μέλη της, αν και συνήθως αντιπροσωπεύουμε κάθε κλάση υπολοίπων από τον μικρότερο μη αρνητικό ακέραιο, ο οποίος ανήκει σε αυτήν την κλάση (αφού αυτό είναι το σωστό υπόλοιπο που προκύπτει από τη διαίρεση). Οποιαδήποτε δύο μέλη από διαφορετικές κλάσεις υπολοίπων modulo n είναι ασύμβατα modulo n. Επιπλέον, κάθε ακέραιος ανήκει σε μία και μόνο μία κλάση υπολοίπων modulo n.[1]

Το σύνολο των ακεραίων {0, 1, 2, …, n − 1} λέγεται το ελάχιστο σύστημα υπολοίπων modulo n. Οποιοδήποτε σύνολο n ακεραίων, δύο εκ των οποίων δεν είναι ισότιμοι modulo n, ονομάζεται πλήρης σύστημα υπολοίπων modulo n.

Είναι σαφές ότι το ελάχιστο σύστημα υπολοίπων είναι ένα πλήρες σύστημα υπολοίπων, και ένα πλήρες σύστημα υπολοίπων είναι απλά ένα σύνολο που περιέχει ακριβώς έναν εκπρόσωπο από κάθε κλάση υπολοίπων modulo n.[2] Το ελάχιστο σύστημα υπολοίπων modulo 4 είναι το {0, 1, 2, 3}. Κάποια άλλα πλήρη συστήματα υπολοίπων modulo 4 είναι:

  • {1, 2, 3, 4}
  • {13, 14, 15, 16}
  • {−2, −1, 0, 1}
  • {−13, 4, 17, 18}
  • {−5, 0, 6, 21}
  • {27, 32, 37, 42}

Μερικά σύνολα τα οποία δεν είναι πλήρη συστήματα υπολοίπων modulo 4 είναι:

  • {-5, 0, 6, 22} αφού το 6 είναι ισότιμο με το 22 modulo 4.
  • {5, 15} αφού ένα πλήρες σύστημα υπολοίπων modulo 4 πρέπει να έχει ακριβώς 4 ασύμβατες κλάσεις υπολοίπων.

Μειωμένα συστήματα υπολοίπων[Επεξεργασία | επεξεργασία κώδικα]

Κύριο άρθρο: Reduced residue system

Κάθε σύνολο φ(n) ακεραίων αριθμών, που είναι σχετικά πρώτοι στο n και οι οποίοι είναι αμοιβαία ασύμβατοι modulo n, όπου φ(n) δηλώνει τη Συνάρτηση Όιλερ, ονομάζεται μειωμένο σύστημα υπoλοίπων modulo n[3]. Το παραπάνω παράδειγμα, {5,15} είναι ένα παράδειγμα ενός μειωμένου συστήματος υπολοίπων modulo 4.

Κλάσεις ισοτιμίας[Επεξεργασία | επεξεργασία κώδικα]

Όπως κάθε σχέση ισοτιμίας, η ισοτιμία modulo n είναι μία σχέση ισοδυναμίας, και η κλάση ισοδυναμίας του ακέραιου a, που συμβολίζεται με είναι το σύνολο {… a − 2n, an, a, a + n, a + 2n, …}. Αυτό το σετ, που αποτελείται από τους ακεραίους που είναι ισότιμοι με το a modulo n, ονομάζεται κλάση ισοτιμίας ή κλάση υπολοίπων ή απλά υπόλοιπο του ακέραιου a modulo n. Όταν ο συντελεστής n είναι γνωστός από το περιεχόμενο, το υπόλοιπο μπορεί επίσης να συμβολίζεται [a].

Ακέραιοι modulo n[Επεξεργασία | επεξεργασία κώδικα]

Το σύνολο όλων των κλάσεων ισοτιμίας των ακεραίων για ένα συντελεστή n ονομάζεται το σύνολο των ακεραίων modulo n, και συμβολίζεται , ή . Ο συμβολισμός , ωστόσο, δεν συνιστάται επειδή μπορεί να συγχέεται με το σύνολο των [[n-adic ακεραίων]]. Το σύνολο ορίζεται ως εξής.

Όταν n ≠ 0, έχει n στοιχεία και μπορεί να γραφεί ως:

Όταν n = 0, δεν έχει μηδενικά στοιχεία: μάλλον, είναι ισομορφικό στο , όταν .

Μπορούμε να ορίσουμε πρόσθεση, αφαίρεση και πολλαπλασιασμό στο σύνολο με τους ακόλουθους κανόνες:

Η επαλήθευση ότι αυτός είναι ένας σωστός ορισμός χρησιμοποιεί τις ιδιότητες που δόθηκαν πριν.

Με τον τρόπο αυτό, γίνεται ένας αντιμεταθετικός δαχτύλιος. Για παράδειγμα, στο δακτύλιο , έχουμε

όπως και στην αριθμητική για το 24-ωρο ρολόι.

Ο συμβολισμός χρησιμοποιείται, επειδή είναι ο δαχτύλιος πηλίκο του από το ιδεώδες που περιέχει όλους τους ακεραίους που διαιρούνται με το n, όπου είναι το μονοσύνολο {0}. Έτσι, το είναι ένα σώμα όταν είναι ένα μεγιστοτικό ιδεώδες, αυτό συμβαίνει, όταν το n είναι πρώτος.

Όσον αφορά τις ομάδες, η κλάση υπολοίπων είναι το σύμπλοκο της a στην ομάδα πηλίκου , μια κυκλική ομάδα.[4].

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

Αντί να εξαιρείται η ειδική περίπτωση για n = 0, είναι πιο χρήσιμο να περιλαμβάνει το (το οποίο, όπως προαναφέρθηκε, είναι ισομορφικό με το δακτύλιο των ακεραίων), για παράδειγμα, όταν συζητάμε για το χαρακτηριστικό ενός δακτυλίου.

Ο δακτύλιος των ακεραίων modulo n είναι ένα πεπερασμένο σώμα , αν και μόνο αν ο n είναι πρώτος αριθμός. Αν ο n δεν είναι ένας πρώτος με πρωταρχική δύναμη, υπάρχει ένα μοναδικό (μέχρι ισομορφισμό) πεπερασμένο σώμα GF(n) με n στοιχεία, τα οποία δεν πρέπει να συγχέονται με τον δακτύλιο των ακεραίων modulo n, αν και έχουν τον ίδιο αριθμό στοιχείων.

Εκθετοποίηση υπολοίπων[Επεξεργασία | επεξεργασία κώδικα]

Είναι πολύ χρήσιμο το γεγονός ότι η τιμή yax (mod n) μπορεί να υπολογιστεί πολύ αποτελεσματικά, ακόμη και όταν ο αριθμός ax είναι πολύ μεγάλος για να υπολογιστεί (βλέπε εκθετοποίηση υπολοίπων για λεπτομέρειες.) Το y μπορεί να υπολογιστεί χωρίς κάθε φορά να ασχολούμαστε με νούμερα μεγαλύτερα από το n2.

Εφαρμογές[Επεξεργασία | επεξεργασία κώδικα]

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

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

Η αριθμητική υπολοίπων συχνά χρησιμοποιείται για να υπολογίσει τα αθροίσματα ελέγχου που χρησιμοποιούνται μέσα σε αναγνωριστικά. Διεθνείς Αριθμοί Τραπεζικών λογαριασμών (IBANs), για παράδειγμα, κάνουν χρήση του modulo 97 για να εμποδίσουν λάθη του χρήστη κατά την είσοδο σε αριθμούς τραπεζικών λογαριασμών.

Στην κρυπτογραφία, η αριθμητική υπολοίπων άμεσα στηρίζει τα συστήματα δημοσίων κλειδιών όπως το RSA και Diffie–Hellman και παρέχει πεπερασμένα πεδία που αποτελούν το θεμέλιο των ελλιπτικών καμπυλών, και χρησιμοποιείται σε μια ποικιλία αλγορίθμων συμμετρικών κλειδιών συμπεριλαμβανομένης της Advanced Encryption Standard (AES), International Data Encryption Algorithm (IDEA), και RC4. RSA και Diffie–Hellman χρησιμοποιούν modular ύψωση σε δύναμη.

Στην άλγεβρα υπολογιστών, η αριθμητική υπολοίπων συνήθως χρησιμοποιείται για να περιορίζει το μέγεθος των ακέραιων συντελεστών σε ενδιάμεσους υπολογισμούς και δεδομένα. Χρησιμοποιείται στην παραγοντοποίηση πολυωνύμου, ένα πρόβλημα για το οποίο όλοι οι γνωστοί αποδοτικοί αλγόριθμοι χρησιμοποιούν αριθμητική υπολοίπων. Χρησιμοποιείται από τις πιο αποδοτικές υλοποιήσεις του μέγιστου κοινού διαιρέτη πολυωνύμου , ακριβή γραμμική άλγεβρα και Gröbner βάση αλγορίθμους πάνω στους ακέραιους και στους ρητούς αριθμούς.

Στην επιστήμη των υπολογιστών, η αριθμητική υπολοίπων συχνά εφαρμόζεται σε bitwise πράξεις και άλλες πράξεις που αφορούν σταθερού πλάτους, κυκλικές δομές δεδομένων. Η λειτουργία modulo, όπως εφαρμόζεται σε πολλές γλώσσες προγραμματισμού και αριθμομηχανές, είναι μια εφαρμογή της αριθμητικής υπολοίπων που χρησιμοποιείται συχνά σε αυτό το πλαίσιο. XOR είναι το άθροισμα των 2 bits, modulo 2.

Στη χημεία, το τελευταίο ψηφίο του CAS αριθμού μητρώου (ένας αριθμός ο οποίος είναι μοναδικός για κάθε χημική ένωση) είναι ένα ψηφίο ελέγχου, το οποίο υπολογίζεται επιλέγοντας το τελευταίο ψηφίο από τα δύο πρώτα μέρη του CAS αριθμού μητρώου 1 φορά, το προηγούμενο ψηφίο 2 φορές, το προηγούμενο ψηφίο 3 φορές κ.λ.π., προσθέτοντας σε όλα αυτά και τον υπολογισμό του ποσού modulo 10.

Στη μουσική, το modulo 12 χρησιμοποιείται στην εξέταση του συστήματος του δωδεκάτονου ίσου τέμπου, όπου προκύπτει η οκτάβα και η εναρμόνια ισοδυναμία (δηλαδή, τόνος σε 1∶2 ή 2∶1 αναλογία είναι ισοδύναμα, και η C-Δίεση θεωρείται η ίδια ως D-ύφεση).

Η μέθοδος casting out nines προσφέρει ένα γρήγορο έλεγχο των δεκαδικών αριθμητικών υπολογισμών που εκτελούνται με το χέρι. Βασίζεται στην αριθμητική υπολοίπων modulo 9, και συγκεκριμένα στην κρίσιμη ιδιότητα όπου 10 ≡ 1 (mod 9).

Το modulo 7 χρησιμοποιείται σε αλγορίθμους που προσδιορίζουν την ημέρα της εβδομάδας για μια συγκεκριμένη ημερομηνία. Ειδικότερα, η συνεκτικότητα Zeller και ο αλγόριθμος της ημέρας της κρίσεως κάνουν μεγάλη χρήση του modulo-7.

Γενικότερα, η αριθμητική υπολοίπων, επίσης, έχει εφαρμογή σε κλάδους όπως το δίκαιο (βλέπε, για παράδειγμα, κατανομή), τα οικονομικά, (βλέπε, για παράδειγμα, τη θεωρία παιγνίων) και σε άλλους τομείς των κοινωνικών επιστημών, όπου η αναλογική κατανομή και η κατανομή των πόρων αποτελεί κεντρικό μέρος της ανάλυσης.

Υπολογιστική πολυπλοκότητα[Επεξεργασία | επεξεργασία κώδικα]

Από τη στιγμή που η αριθμητική υπολοίπων έχει ένα τέτοιο ευρύ φάσμα εφαρμογών, είναι σημαντικό να γνωρίζουμε πόσο δύσκολο είναι να λύσουμε ένα σύστημα ισοτιμίας. Ένα γραμμικό σύστημα ισοτιμίας μπορεί να λυθεί σε πολυωνυμικό χρόνο με μια μορφή απαλοιφής Gauss, για περισσότερες λεπτομέρειες βλέπε θεώρημα γραμμικής ισοτιμίας . Αλγόριθμοι, όπως η αναγωγή Μοντγκόμερι , υπάρχουν, επίσης, για να επιτρέπουν απλές αριθμητικές πράξεις, όπως ο πολλαπλασιασμός και η εκθετοποίηση ή ύψωση σε δύναμη modulo n, να εκτελούνται αποτελεσματικά σε μεγάλους αριθμούς.

Ορισμένες λειτουργίες, όπως η εύρεση ενός διακριτού λογαρίθμου ή οι δευτεροβάθμιες ισοτιμίες φαίνεται να είναι τόσο δύσκολες όσο η παραγοντοποίηση ακεραίων και, επομένως, το σημείο εκκίνησης είναι η Κρυπτογραφία αλγορίθμων και η Κρυπτογράφηση. Αυτά τα προβλήματα είναι NP-ενδιάμεσα.

Η επίλυση του συστήματος των μη-γραμμικών εξισώσεων αριθμητικής υπολοίπων είναι NP-πλήρης.[5]

Παράδειγμα υλοποίησης[Επεξεργασία | επεξεργασία κώδικα]

Παρακάτω είναι δύο αρκετά γρήγορες C λειτουργίες για την εκτέλεση πολλαπλασιασμού υπολοίπων στους μη προσημασμένους ακεραίους όχι μεγαλύτερους από 63 bits, χωρίς υπερχείλιση από τις παροδικές πράξεις. Ένας αλγοριθμικό τρόπο για να υπολογίσουμε το a × b (mod m):

uint64_t mul_mod(uint64_t a, uint64_t b,                                                                                               uint64_t m)                                                                                                                                   {                                                                                                                                      uint64_t d = 0, mp2 = m >> 1;                                                                                                               int i;                                                                                                                                       if (a >= m) a %= m;                                                                                                                          if (b >= m) b %= m;                                                                                                                         for (i = 0; i < 64; ++i)                                                                                                                      {                                                                                                                                             d = (d > mp2) ? (d << 1) - m : d << 1;                                                                                                       if (a & 0x8000000000000000ULL)                                                                                                                d += b;                                                                                                                                      if (d > m) d -= m;                                                                                                                                       a <<= 1;                                                                                                                                      }                                                                                                                                               return d;                                                                                                                                     }                                                                                                                                         

Στις αρχιτεκτονικές των υπολογιστών, όπου μια εκτεταμένης ακριβείας μορφή, με τουλάχιστον 64 bits mantissa, είναι διαθέσιμη (όπως ο long double τύπος των περισσοτέρων x86 C compilers), η παρακάτω ρουτίνα είναι πιο γρήγορη από οποιαδήποτε αλγοριθμική λύση, χρησιμοποιώντας το τέχνασμα αυτό, με το υλικό, ο πολλαπλασιασμός κινητής υποδιαστολής έχει ως αποτέλεσμα τη διατήρηση των πιο σημαντικών bits του προϊόντος, ενώ ο πολλαπλασιασμός ακεραίων οδηγεί στη διατήρηση των λιγότερο σημαντικών bits: Ένας αλγοριθμικός τρόπος για να υπολογίσουμε το a × b (mod m):

uint64_t mul_mod(uint64_t a, uint64_t b,                                                                                                           uint64_t m)                                                                                                                                                                        {                                                                                                                                            long double x;                                                                                                                           uint64_t c;                                                                                                                               int64_t r;                                                                                                                                    if (b >= m) b %= m;                                                                                                                           x = a;                                                                                                                                        c = x * b / m;                                                                                                                                  r = (int64_t)(a * b - c * m) %                                                                                                         (int64_t)m;                                                                                                                               return r < 0 ? r + m : r;                                                                                                                         }

Ωστόσο, και για τις δύο ρουτίνες για να λειτουργήσουν, το m δεν πρέπει να υπερβαίνει τα 63 bits.

Δείτε επίσης[Επεξεργασία | επεξεργασία κώδικα]

Σημειώσεις[Επεξεργασία | επεξεργασία κώδικα]

Αναφορές[Επεξεργασία | επεξεργασία κώδικα]

Εξωτερικοί σύνδεσμοι[Επεξεργασία | επεξεργασία κώδικα]

Αυτοματοποιημένη αριθμητική υπολοίπων θεώρημα provers[Επεξεργασία | επεξεργασία κώδικα]

  • Spear
  • AAProver - Simple C++ - πλαίσιο εύκολο στη χρήση σε εφαρμογές, υποστηρίζοντας, μεταξύ άλλων, όλους τους ακέραιους φορείς που είναι παρόντες σε γλώσσες όπως οι C/C++/Java και αυθαίρετου πλάτους bit.