IMHO, SAT/SMT solvers does mostly the same, so why would you designate separate PL for this task, when you use these tools or libraries?
However, Prolog lets you tackle not only propositional logic, but tasks that go far beyond this, belonging to a logic called classical first order logic, of which propositional logic is only a subset. In first order logic, we reason about predicates between terms, and this lets you tackle much more complex tasks, far beyond what SAT/SMT solvers can solve for you.
In fact, first order logic is so powerful that it lets you describe everything you can in principle perform with a computer. It lets you describe how a compiler works, for example. Or how numerical integration works. And all other computations you have ever seen computers perform.
In short, Prolog is a programming language, and can in fact even be used to implement a SAT solver, which is impossible to do with just a SAT solver. Many Prolog implementations even ship with a SAT solver as one of their libraries.
There are also even higher-order constructs in Prolog, such as predicates that let you invoke other predicates, making programming in Prolog very expressive and convenient.
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.
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/
Not quite sure what you're referring to here, but induction schemata seem to be a notable exception. There's a reason higher-order logic is often preferred for software verification.
I guess FOL is adequate if you're allowed to have an infinite number of axioms, but that doesn't seem very satisfying (pun intended).