Abstract
We provide here a framework for studying Prolog programs with various built-in's that include arithmetic operations, and such metalogical relations like var and ground. To this end we propose a new, declarative semantics and prove completeness of the Prolog computation mechanism w.r.t. this semantics. We also show that this semantics is fully abstract in an appropriate sense. Finally, we provide a method for proving termination of Prolog programs with built-in's which uses this semantics. The method is shown to be modular and is illustrated by proving termination of a number of programs including the unify program of Sterling and Shapiro [17].
| Original language | English |
|---|---|
| Pages (from-to) | 159-191 |
| Number of pages | 33 |
| Journal | Applicable Algebra in Engineering, Communication and Computing |
| Volume | 5 |
| Issue number | 3-4 |
| DOIs | |
| Publication status | Published - 1 May 1994 |
| Externally published | Yes |
Keywords
- 1991 Mathematics Subject Classification: 68Q40, 68T15
- Builtin's
- Declarative semantics
- F.3.2
- F.4.1
- H.3.3
- I.2.3
- Prolog programs
- Termination