Dear Anggha,
I'm afraid it's been a very long time since I was a HOL user, so I can't answer
your question. But I hereby forward your query to the HOL mailing list, hoping
some active user can help.
Best regards,
Tom
From: Anggha Nugraha <[email protected]<mailto:[email protected]>>
Reply-To: Anggha Nugraha <[email protected]<mailto:[email protected]>>
Date: Tuesday, 12 June 2012 06:14
To: Tom Melham <[email protected]<mailto:[email protected]>>
Subject: Asking about HOL TP (sum syntax)
Good evening Professor Melham.
Firstly, let me introduce my self. My name is Anggha and now I'm a master
student in Faculty of Computer Science in University of Indonesia. Now, I'm
making my master thesis about proving the partial correctness of matrix
multiplication program. I plan to making the manual proof using Hoare logic and
then making the automation in HOL Theorem Proving.
I have read your paper entitled,"A MECHANIZED THEORY OF THE -CALCULUS IN HOL"
and I know that you're an expert in HOL TP.
I have a problem in writing in HOL. I wanna write: C[i,j] = sum z=1..n
A[i,z]*B[z,j]
I use # to indicate array, so C[i,j] is written as (C#i)#j. Am I right doc?
About the summation, I don't have any idea how to write this in HOL. How I
define the syntax of sum? What library that I have to use prof?
May you help me prof? And if you don't mind, can you give me an example?
Thank you very much Prof. Melham and I really sorry if I disturb you prof.
--
Best regards,
Anggha Satya Nugraha
Graduate Student in Faculty of Computer Science
University of Indonesia (Universitas Indonesia)
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
