3 ms·

> SMT, I don't know much about. It's got nothing to do with Prolog, as far as I know. It's not a programming language, but a framework for boolean constraint so

> SMT, I don't know much about. It's got nothing to do with Prolog, as far as I know. It's not a programming language, but a framework for boolean constraint solving. I don't know why it (or SAT) is compared to Prolog which has nothing to do with boolean satisfiability problems. SMT and SAT are certainly less expressive than Prolog (or more abstract systems, like LambdaProlog, Isabelle/HOL, etc.), so they cannot express the same structures/abstractions. However, given any "concrete" query/program, we can collapse all of its structure, in-line/unroll all of its higher-order parts, etc. to get a SAT formula (modulo the halting problem). The resulting term is usually exponentially-larger than the original; but SAT solvers have become fast enough to handle such giant problems. (SMT solvers are usually wrappers around a SAT solver too)

YeGoblynQueenne 4y ago
I think what you're saying is that you can take a Prolog program and ground it all down to the propositional order so you can then evaluate it with a SAT solver. For example, you can take a Prolog clause like this one: p(X,Y):- q(X,Z), r(Z,Y) And ground it in all possible ways with constants in the domain of discourse: p(a,b):- q(a,c), r(c,b) p(1,3):- q(1,2), r(2,3) ... And so on, at which point you essentially have propositional formulae, like: p1 :- q1, r1 p2 :- q2, r2 ... etc. That's what ASP does (except it's not Prolog). But one problem with that is that it doesn't work in a language with functions, because then you get infinite groundings. So for example, ASP doesn't have lists (because you get infinite lists). Prolog does, and you can't just ground any old Prolog program, just like that. Then again, the motivation behind Prolog's unification is exactly that you don't need to ground the entire Herbrand base of a Prolog program to evaluate it. You can unify variables, until you finally have only ground terms when the proof is complete, but no sooner than that. And of course, you can get a proof before you have only ground terms. So it's really not like SAT solving in my mind (given the very little I understand about SAT solving). If I understand correctly, the Davis-Putnam algorithm used in SAT solving is based on Resolution in the propositional order, and Prolog is SLD-Resolution, that is a restriction of Resolution to definite clauses which are first-order (though Prolog is not first-order but higher-order as I say in another comment). So that's some common structure, there, but still, they're very different things.

YeGoblynQueenne 4y ago

I think what you're saying is that you can take a Prolog program and ground it all down to the propositional order so you can then evaluate it with a SAT solver. For example, you can take a Prolog clause like this one: p(X,Y):- q(X,Z), r(Z,Y) And ground it in all possible ways with constants in the domain of discourse: p(a,b):- q(a,c), r(c,b) p(1,3):- q(1,2), r(2,3) ... And so on, at which point you essentially have propositional formulae, like: p1 :- q1, r1 p2 :- q2, r2 ... etc. That's what ASP does (except it's not Prolog). But one problem with that is that it doesn't work in a language with functions, because then you get infinite groundings. So for example, ASP doesn't have lists (because you get infinite lists). Prolog does, and you can't just ground any old Prolog program, just like that. Then again, the motivation behind Prolog's unification is exactly that you don't need to ground the entire Herbrand base of a Prolog program to evaluate it. You can unify variables, until you finally have only ground terms when the proof is complete, but no sooner than that. And of course, you can get a proof before you have only ground terms. So it's really not like SAT solving in my mind (given the very little I understand about SAT solving). If I understand correctly, the Davis-Putnam algorithm used in SAT solving is based on Resolution in the propositional order, and Prolog is SLD-Resolution, that is a restriction of Resolution to definite clauses which are first-order (though Prolog is not first-order but higher-order as I say in another comment). So that's some common structure, there, but still, they're very different things.