HOL

HOL μικρή από Ανώτερης Τάξης Λογική είναι ένα προγραμματιστικό περιβάλλον στο οποίο θεωρήματα μπορούν να αποδειχθούν και τα εργαλεία απόδειξη εφαρμοστεί.
Built-in διαδικασίες λήψης αποφάσεων και provers θεώρημα μπορεί να δημιουργήσει αυτόματα πολλές απλές θεωρήματα. Ένας μηχανισμός μαντείο δίνει πρόσβαση σε εξωτερικά προγράμματα, όπως το SAT και BDD κινητήρες.
HOL 4 είναι ιδιαίτερα κατάλληλο ως πλατφόρμα για την εφαρμογή συνδυασμούς έκπτωση, την εκτέλεση και τον έλεγχο ιδιοκτησίας

Τι είναι καινούργιο σε αυτή την έκδοση:.

• HolSmtLib τώρα υποστηρίζει επίσης Z3 απόδειξη ανασυγκρότησης για τους στόχους που περιλαμβάνουν σταθερού πλάτους λόγια και μετάφραση από HOL σε SMT-LIB μορφή 2.
• HolQbfLib υποστηρίζει τον έλεγχο τόσο για το κύρος και την ακυρότητα των πιστοποιητικών για Squolem 2.02. wordsSyntax.mk_word_replicate υπολογίζει το πλάτος του προκύπτοντος λέξη όταν εφαρμόζεται σε αριθμό και σταθερού πλάτους λέξη.
• Το σύστημα υποστηρίζει σύνταξη για δεκαδικά κλάσματα.
• Αυτή η σύνταξη χαρτών με τους όρους διαίρεση της μορφής n / 10μ.
• Στον πυρήνα του συστήματος, αυτή η σύνταξη είναι ενεργοποιημένη για την πραγματική, ορθολογική, και πολύπλοκες θεωρίες.

Τι είναι καινούργιο στην έκδοση 6:

• Η βιβλιοθήκη HolSmtLib υποστηρίζει τώρα απόδειξη για την ανασυγκρότηση SMT λύτης Ζ3 .
• Πολλές μεταβλητές τύπου μπορεί τώρα να αναλυθεί και να εκτυπώνονται ως πεζά ελληνικά γράμματα.
• οριοθετείται επανεγγραφές λειτουργήσει καλύτερα.
• Η απλοποίηση των όρων που αφορούν το χειριστή ΕΛ είναι καλύτερα.
• Βελτιωμένη υποστήριξη για τις πράξεις τσάντα.
• Σύνταξη ενημερώσεις για πράγματα όπως το οικουμενικό σύνολο.
• Άλλες μικρές βελτιώσεις και διορθώσεις σφαλμάτων.