Loading...
Please wait, while we are loading the content...
Similar Documents
An Integrated Development of Buchberger's Algorithm in Coq
| Content Provider | Hyper Articles en Ligne (HAL) |
|---|---|
| Author | Persson, Henrik |
| Abstract | We present an integrated formal development of Buchberger's algorithm in Coq, that is we prove constructively the existence of Gröbner bases without explicitly writing the algorithm. This formalisation is based on an external formalisation in Coq by Théry, and an integrated abstract development in Agda. We end by discussing some experiences and differences between the two proof-styles and theorem-provers. This report was completed in March 2000. |
| File Format | |
| Language | English |
| Publisher Date | 2001-09-01 |
| Publisher Institution | INRIA |
| Access Restriction | Open |
| Subject Keyword | AGDA COQ INTEGRATED PROGRAMMING LOGIC BUCHBERGER'S ALGORITHM THEOREM PROVING COMPUTER ALGEBRA info Computer Science [cs] Other [cs.OH] |
| Content Type | Text |
| Resource Type | Article |