http://repository.vnu.edu.vn/handle/VNU_123/26848
The HOL Theorem Prover is a general and widely-used computer program for constructing specifications and formal proofs in higher order logic. The system is used in industry and academia to support formal reasoning in many different areas, including hardware design and verification, reasoning about security, proofs about real-time systems, semantics of hardware description languages, compiler verification, program correctness, modelling concurrency, and program refinement. HOL is also used as an open platform for general theorem-proving research, and as a platform for formalized mathematics.
The HOL Theorem Prover is a general and widely-used computer program for constructing specifications and formal proofs in higher order logic. The system is used in industry and academia to support formal reasoning in many different areas, including hardware design and verification, reasoning about security, proofs about real-time systems, semantics of hardware description languages, compiler verification, program correctness, modelling concurrency, and program refinement. HOL is also used as an open platform for general theorem-proving research, and as a platform for formalized mathematics.
Nhận xét
Đăng nhận xét