On Modular Termination Proofs of General Logic Programs
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2000
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913899063803904 |
|---|---|
| author | Bossi, Annalisa Cocco, Nicoletta Etalle, Sandro Rossi, Sabina |
| author_facet | Bossi, Annalisa Cocco, Nicoletta Etalle, Sandro Rossi, Sabina |
| contents | We propose a modular method for proving termination of general logic programs (i.e., logic programs with negation). It is based on the notion of acceptable programs, but it allows us to prove termination in a truly modular way. We consider programs consisting of a hierarchy of modules and supply a general result for proving termination by dealing with each module separately. For programs which are in a certain sense well-behaved, namely well-moded or well-typed programs, we derive both a simple verification technique and an iterative proof method. Some examples show how our system allows for greatly simplified proofs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_cs_0005018 |
| institution | arXiv |
| publishDate | 2000 |
| record_format | arxiv |
| spellingShingle | On Modular Termination Proofs of General Logic Programs Bossi, Annalisa Cocco, Nicoletta Etalle, Sandro Rossi, Sabina Logic in Computer Science Programming Languages D.2; D.3; F.3.1; F.3.2 We propose a modular method for proving termination of general logic programs (i.e., logic programs with negation). It is based on the notion of acceptable programs, but it allows us to prove termination in a truly modular way. We consider programs consisting of a hierarchy of modules and supply a general result for proving termination by dealing with each module separately. For programs which are in a certain sense well-behaved, namely well-moded or well-typed programs, we derive both a simple verification technique and an iterative proof method. Some examples show how our system allows for greatly simplified proofs. |
| title | On Modular Termination Proofs of General Logic Programs |
| topic | Logic in Computer Science Programming Languages D.2; D.3; F.3.1; F.3.2 |
| url | https://arxiv.org/abs/cs/0005018 |