Experimental Results for Vampire on the Equational Theories Project
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915456566165504 |
|---|---|
| author | Janota, Mikoláš |
| author_facet | Janota, Mikoláš |
| contents | Equational Theories Project is a collaborative effort, which explores the validity of certain first-order logic implications of certain kind. The project has been completed but triggered further research. This report investigates how much can be automatically proven and disproven by the automated theorem prover Vampire. An interesting conclusion is that Vampire can prove all the considered implications that hold and also is able to refute a vast majority of those that do not hold. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_15856 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Experimental Results for Vampire on the Equational Theories Project Janota, Mikoláš Logic in Computer Science Equational Theories Project is a collaborative effort, which explores the validity of certain first-order logic implications of certain kind. The project has been completed but triggered further research. This report investigates how much can be automatically proven and disproven by the automated theorem prover Vampire. An interesting conclusion is that Vampire can prove all the considered implications that hold and also is able to refute a vast majority of those that do not hold. |
| title | Experimental Results for Vampire on the Equational Theories Project |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2508.15856 |