A Curiously Effective Backtracking Strategy for Connection Tableaux
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911758659092480 |
|---|---|
| author | Färber, Michael |
| author_facet | Färber, Michael |
| contents | Automated proof search with connection tableaux, such as implemented by Otten's leanCoP prover, depends on backtracking for completeness. Otten's restricted backtracking strategy loses completeness, yet for many problems, it significantly reduces the time required to find a proof. I introduce a new, less restricted backtracking strategy based on the notion of exclusive cuts. I implement the strategy in a new prover called meanCoP and show that it greatly improves upon the previous best strategy in leanCoP. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2106_13722 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | A Curiously Effective Backtracking Strategy for Connection Tableaux Färber, Michael Logic in Computer Science F.4.1 Automated proof search with connection tableaux, such as implemented by Otten's leanCoP prover, depends on backtracking for completeness. Otten's restricted backtracking strategy loses completeness, yet for many problems, it significantly reduces the time required to find a proof. I introduce a new, less restricted backtracking strategy based on the notion of exclusive cuts. I implement the strategy in a new prover called meanCoP and show that it greatly improves upon the previous best strategy in leanCoP. |
| title | A Curiously Effective Backtracking Strategy for Connection Tableaux |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2106.13722 |