Name
Abstract | ||
|---|---|---|
We explore several ways to formalize the algebraic laws of CSP-likelanguages in HOL. The intent of the paper is to show how HOL can betailored to acting as a proof assistant. The emphasis is therefore on theconsequences of various choices to be made during the formalization forwriting tactics. We end up with a proof assistant that allows a user tomake steps of the granularity of an algebraic law. It is not the purposeof this paper to show in HOL that the algebraic laws of some CSP-like... |
Year | DOI | Venue |
|---|---|---|
1995 | 10.1007/3-540-60117-1_17 | MPC |
Keywords | Field | DocType |
algebraic proof assistants,proof assistant | HOL,Discrete mathematics,Algebraic number,Computer science,Granularity,Proof assistant,Algebraic laws | Conference |
ISBN | Citations | PageRank |
3-540-60117-1 | 5 | 0.57 |
References | Authors | |
4 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rix Groenboom | 1 | 125 | 19.05 |
| Chris Hendriks | 2 | 5 | 0.57 |
| Indra Polak | 3 | 69 | 19.09 |
| Jan Terlouw | 4 | 24 | 3.52 |
| Jan Tijmen Udding | 5 | 233 | 46.50 |