All serious Prolog systems provide constraint logic programming over finite domains, called CLP(FD) for short, with which you can solve many such equations easily. For example, with SICStus Prolog, SWI and Yap:
?- use_module(library(clpfd)).
true.
?- 5+X #= 7.
X = 2.
Apparently, the answer is 2 instead of -2. Also check out constraint logic programming over other domains, like the rationals with library(clpq).
与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…