The standard already gave the execution model as a stack of states with goal/substition/backtracking info for each state. It looks like they try to redefine the execution model (and also some build-in predicates) using the first order logic.
- What is the purpose of it? It looks like the standard has two different execution models defined and we also have WAM so there are at least 3 execution models..
- Can I code my prolog interpreter completely from that formal semantics? Should I? Maybe it can be beneficial for educational/understanding purposes because it is pure logical and I already feel a bit uncomfortable with the stack model
- Why they try to detalize so many build-in predicates? Isn’t it enough to have input/output/errors specified for the standard?