DocumentCode
2759944
Title
Reasoning in CSP via the HOL theorem prover
Author
Camilleri, Albert John
Author_Institution
Hewlett-Packard Lab., Bristol, UK
fYear
1990
fDate
22-25 Oct 1990
Firstpage
173
Lastpage
183
Abstract
A proof tool developed for CSP by customizing an existing general-purpose theorem prover based on higher order logic is described, and it is demonstrated how it can be used to conduct formal reasoning about CSP. The focus is on illustrating the usefulness of the approach. It is shown how reasoning about CSP can be done using a natural deduction theorem prover by illustrating how some standard CSP laws can be mechanically proved from semantic definitions mechanized previously by the author (1990)
Keywords
theorem proving; CSP; HOL theorem prover; formal reasoning; higher order logic; natural deduction theorem prover; proof tool; semantic definitions; Algebra; Concurrent computing; Humans; Laboratories; Logic functions; Mechanical factors; System recovery;
fLanguage
English
Publisher
ieee
Conference_Titel
Information Technology, 1990. 'Next Decade in Information Technology', Proceedings of the 5th Jerusalem Conference on (Cat. No.90TH0326-9)
Conference_Location
Jerusalem
Print_ISBN
0-8186-2078-1
Type
conf
DOI
10.1109/JCIT.1990.128283
Filename
128283
Link To Document