Logic for Computable Functions

Logic for Computable Functions (LCF), Edinburgh ve Stanford araştırmacıları tarafından geliştirilmiş bir otomatik teorem kanıtlama aracıdır. 1972'de Robin Milner'ın önderlik ettiği çalışmayla temelleri atılmış olup ML programlama dili yardımıyla özelleştirilebilir bir yapıya kavuşmuştur. Bu işlem "theorem" adlı soyut veri tipi aracılığıyla yapılabilmektedir.

Kaynakça

  • Gordon, Michael J. C. (2000). "From LCF to HOL: a short history". Proof, language, and interaction. Cambridge, MA: MIT Press. ss. 169-185. ISBN 0-262-16188-5. Erişim tarihi: 1 Ocak 2018.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.