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 proc

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/