The Tactician's Web of Large-Scale Formal Knowledge
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911752323596288 |
|---|---|
| author | Blaauwbroek, Lasse |
| author_facet | Blaauwbroek, Lasse |
| contents | The Tactician's Web is a platform offering a large web of strongly interconnected, machine-checked, formal mathematical knowledge conveniently packaged for machine learning, analytics, and proof engineering. Built on top of the Coq proof assistant, the platform exports a dataset containing a wide variety of formal theories, presented as a web of definitions, theorems, proof terms, tactics, and proof states. Theories are encoded both as a semantic graph (rendered below) and as human-readable text, each with a unique set of advantages and disadvantages. Proving agents may interact with Coq through the same rich data representation and can be automatically benchmarked on a set of theorems. Tight integration with Coq provides the unique possibility to make agents available to proof engineers as practical tools. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_02950 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The Tactician's Web of Large-Scale Formal Knowledge Blaauwbroek, Lasse Logic in Computer Science Machine Learning Programming Languages 03B40 (Primary) 68T30, 03B38 (Secondary) F.4.1 The Tactician's Web is a platform offering a large web of strongly interconnected, machine-checked, formal mathematical knowledge conveniently packaged for machine learning, analytics, and proof engineering. Built on top of the Coq proof assistant, the platform exports a dataset containing a wide variety of formal theories, presented as a web of definitions, theorems, proof terms, tactics, and proof states. Theories are encoded both as a semantic graph (rendered below) and as human-readable text, each with a unique set of advantages and disadvantages. Proving agents may interact with Coq through the same rich data representation and can be automatically benchmarked on a set of theorems. Tight integration with Coq provides the unique possibility to make agents available to proof engineers as practical tools. |
| title | The Tactician's Web of Large-Scale Formal Knowledge |
| topic | Logic in Computer Science Machine Learning Programming Languages 03B40 (Primary) 68T30, 03B38 (Secondary) F.4.1 |
| url | https://arxiv.org/abs/2401.02950 |