Ditemukan 1 dokumen yang sesuai dengan query
Ade Azurat
"
HOL is a theorem prover based on a higher order logic. Its expressive logic makes it suitable for embedding programming logics. Compared to other theorem provers, HOL is attractive because of its familiar and intuitive logic and because it is highly programmable. In this paper we will compare a number of commonly used embedding approaches in HOL and outline their strength and weakness. We will also outline a new alternative called hybrid embedding that combines ...
"
2002
JIKT-2-1-Mei2002-18
Artikel Jurnal Universitas Indonesia Library
