Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866929221787451392 |
|---|---|
| author | Gonzalez, Salwa Tabet Janičić, Predrag Narboux, Julien |
| author_facet | Gonzalez, Salwa Tabet Janičić, Predrag Narboux, Julien |
| contents | Conjecturing and theorem proving are activities at the center of mathematical practice and are difficult to separate. In this paper, we propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions and with an under-specified goal into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof. Our approach is focused on synthetic geometry, and uses coherent logic and constraint solving. The proposed approach is uniform for all three kinds of tasks, flexible and, to our knowledge, unique such approach. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_11898 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving Gonzalez, Salwa Tabet Janičić, Predrag Narboux, Julien Artificial Intelligence Logic in Computer Science Conjecturing and theorem proving are activities at the center of mathematical practice and are difficult to separate. In this paper, we propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions and with an under-specified goal into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof. Our approach is focused on synthetic geometry, and uses coherent logic and constraint solving. The proposed approach is uniform for all three kinds of tasks, flexible and, to our knowledge, unique such approach. |
| title | Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving |
| topic | Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2401.11898 |