3 ms·

What about SMT vs. Prolog, do Prolog have more expressiveness?

zmonx 9y ago
SMT solvers typically only support decidable theories, and since first-order logic is not decidable (only semi-decidable), such solvers are not as expressive as Prolog. In Prolog, the more natural approach that closely corresponds to SMT is simply implementing the theory as a constraint solver. For example, check out CLP(FD) and CLP(Q) for constraint solvers over integers and rational numbers, respectively. They let you formulate statements over these theories, and search for solutions. Note though that solving equations over the second-order theory Z (i.e., integers) is not decidable either (only semi-decidable), and so you may search indefinitely if there is no solution. Importantly, constraints over these theories blend in completely seamlessly into Prolog, since they are simply available as predicates. For example, we can write: ?- A^N + B^N #= C^N, N #> 2, [A,B,C] ins 1..sup. This expresses Fermat's Last Theorem in terms of CLP(FD). A constraint solver with perfect propagation (which, as we know, cannot exist for the integers) would deduce that this conjunction of constraints cannot hold.
- mjn 9y ago
  Answer-set programming (ASP) is another direction to go in w.r.t. this relationship. It takes a Prolog-like semantics (and syntax), but rebases the solving process on top of a solver-style backend that shares some general similarities with SMT/SAT-style propositional solvers. The semantics of ASP were initially arrived at as one of several attempts to give a conventional logical semantics to Prolog. Prolog's semantics from the perspective of traditional logic are a bit obscure, because it's defined in a somewhat imperative manner as "whatever SLDNF gives you", which includes things like statement order being significant (queries might terminate under one ordering and not under another, which is not something you find in logical semantics). ASP is based on one of those Prolog-semantic proposals, the "stable-model semantics", which competed with other proposals like the "well-founded semantics". Although these are first-order in principle, existing practical tools only implement propositional solvers. ASP systems still take a Prolog-like input language that looks first-order, but they work by first "grounding" the first-order formulae to a propositional representation, and then solving them. If you make suitable assumptions about finite domains etc. this has the same expressivity, but sometimes causes blow-up (other times it causes surprisingly fast-running programs, though). This is a good open-source ASP system: https://potassco.org/ https://potassco.org/

SMT solvers typically only support decidable theories, and since first-order logic is not decidable (only semi-decidable), such solvers are not as expressive as Prolog. In Prolog, the more natural approach that closely corresponds to SMT is simply implementing the theory as a constraint solver. For example, check out CLP(FD) and CLP(Q) for constraint solvers over integers and rational numbers, respectively. They let you formulate statements over these theories, and search for solutions. Note though that solving equations over the second-order theory Z (i.e., integers) is not decidable either (only semi-decidable), and so you may search indefinitely if there is no solution. Importantly, constraints over these theories blend in completely seamlessly into Prolog, since they are simply available as predicates. For example, we can write: ?- A^N + B^N #= C^N, N #> 2, [A,B,C] ins 1..sup. This expresses Fermat's Last Theorem in terms of CLP(FD). A constraint solver with perfect propagation (which, as we know, cannot exist for the integers) would deduce that this conjunction of constraints cannot hold.

mjn 9y ago
Answer-set programming (ASP) is another direction to go in w.r.t. this relationship. It takes a Prolog-like semantics (and syntax), but rebases the solving process on top of a solver-style backend that shares some general similarities with SMT/SAT-style propositional solvers. The semantics of ASP were initially arrived at as one of several attempts to give a conventional logical semantics to Prolog. Prolog's semantics from the perspective of traditional logic are a bit obscure, because it's defined in a somewhat imperative manner as "whatever SLDNF gives you", which includes things like statement order being significant (queries might terminate under one ordering and not under another, which is not something you find in logical semantics). ASP is based on one of those Prolog-semantic proposals, the "stable-model semantics", which competed with other proposals like the "well-founded semantics". Although these are first-order in principle, existing practical tools only implement propositional solvers. ASP systems still take a Prolog-like input language that looks first-order, but they work by first "grounding" the first-order formulae to a propositional representation, and then solving them. If you make suitable assumptions about finite domains etc. this has the same expressivity, but sometimes causes blow-up (other times it causes surprisingly fast-running programs, though). This is a good open-source ASP system: https://potassco.org/ https://potassco.org/