A declarative approach for first-order built-in's of Prolog
The aim of the paper is to provide a new non-standard declarative semantic for Prolog programs with built-in's that include arithmetic operations and metalogical relations like var and ground. Completeness of the Prolog computation mechanism w.r.t. this semantics is proved. The authors provide a method for proving termination of Prolog programs with built-in's which uses this semantics.
scientific article; zbMATH DE number 599668