Forgot your password?
New user?
ACL2 3.0
Welcome to the QPQ Deductive Software Repository
Document Actions
HOL 4
HOL 4 is the latest version of the HOL automated proof system for higher order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems. An oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking.
Size 17.9 kB - File type application/x-tar
Click here to get the file
