Ubuntu is composed of many software packages, the vast majority of which are distributed under a free software license. The only exceptions are some proprietary hardware drivers.The main license used is the GNU General Public License (GNU GPL) which, along with the GNU Lesser General Public License (GNU LGPL), explicitly declares that users are free to run, copy, distribute, study, change, develop and improve the software. On the other hand, there is also proprietary software available that can run on Ubuntu. Ubuntu focuses on usability, security and stability. The Ubiquity installer allows Ubuntu to be installed to the hard disk from within the Live CD environment, without the need for restarting the computer prior to installation. Ubuntu also emphasizes accessibility and internationalization to reach as many people as possible.

Seguimi in Twitter Seguimi in Facebook Seguimi in Pinterest Seguimi in LinkedIn Seguimi in Google+ Seguimi  in Stumbleupon seguimi  in instagram Sottoscrivi il feed

Emmabuntus, Ubuntu, Derivate, Linux, Open Source BackTrack, Linux, distributions, Ubuntu, derivate, securuty, forensic VirtualBox, Linux, Ubuntu, Raring Ringtail synaptic, Ubuntu, Linux, software packages jwplayer, multimedia, Linux, Ubuntu, flash Meshlab, graphic, software, Ubuntu, open source, Linux Synapse, Linux, Ubuntu, raring, Quantal Gimp, Ubuntu, Linux FreeMind, Linux, open source Linux, infographic, history

HOL(Higher Order Logic), The Higher Order Logic Theorem Prover.

Saturday, August 24, 2013

HOL (Higher Order Logic) denotes a family of interactive theorem proving systems sharing similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library in some programming language.


This library implements an abstract data type of proven theorems so that new objects of this type can only be created using the functions in the library which correspond to inference rules in higher-order logic. As long as these functions are correctly implemented, all theorems proven in the system must be valid. In this way, a large system can be built on top of a small trusted kernel.


Systems in the HOL family use the ML programming language or its successors. ML was originally developed along with LCF to serve the purpose of a meta-language for theorem proving systems; in fact, the name stands for "Meta-Language".



There are four HOL systems (sharing essentially the same logic) that are still maintained and developed.


    The first, HOL4 stems from the HOL88 system, which was the culmination of the original HOL implementation effort, led by Mike Gordon. HOL88 included its own ML implementation, which was in turn implemented on top of Common Lisp.


The implementations following HOL88 (HOL90, hol98 and HOL4) all used Standard ML as the implementation language. The hol98 system is tied to the Moscow ML implementation of Standard ML; HOL4 can be built with either Moscow ML or Poly/ML. Of these four systems, only HOL4 is being maintained and developed. All come with large libraries of theorem proving code. These implement extra automation on top of the very simple core code. HOL4 is BSD licensed.



Which Particular HOL?

There are three main versions of HOL: HOL88, HOL90 and HOL98. Each of these versions is implemented using a different dialect of ML. HOL88 uses Classic ML, HOL90 uses New Jersey Standard ML, and HOL98 uses Moscow ML. We will be using HOL98 on this course.


The differences between the various versions of the HOL system are not great, which is good, because much of the documentation hasn't been updated since HOL88! The most obvious differences between HOL88 and HOL98 are really the differences between Classic ML and Standard ML (Moscow ML). The other obvious differences is that many of the functions that operated on tuples in HOL88 operated on records in HOL98. This isn't a problem because the types of these functions will tell you the names of the record fields - which is pretty much all you need to know.



    The second current implementation is HOL Light. This started as an experimental "minimalist" version of HOL. Although it has subsequently grown into another mainstream HOL variant, its logical foundations remain unusually simple. HOL Light used to be implemented in Caml Light, but now uses OCaml. HOL Light is available under the new BSD license.[2]

    The third current implementation is ProofPower a collection of tools designed to provide special support for working with the Z notation for formal specification. 5 of the 6 tools are GNU GPL v2 licensed. The sixth (PPDaz) has a proprietary license.[3]

    The fourth is HOL Zero, a minimalist implementation focused on trustworthiness. HOL Zero is GNU GPL 3+ licensed[4]

HOL is a predecessor of Isabelle.


If you liked this article, subscribe to the feed by clicking the image below to keep informed about new contents of the blog:


I hope you enjoyed this book. If you have any questions, or want to supplement this post, please write in the comments area. You can also visit Facebook, Twitter, Google +, LinkedIn, Instagram, Pinterest and Feedly where you'll find further information in this blog. SHARE THIS!!


Recent Posts

My Favorites