Comment by weinzierl

Which is strange considering how old and limited Prolog in a sense is. I wonder why no superset ever gained traction and what it would look like. I imagine it fitting somewhere in the hierarchy

Theorem Prover ⊃ SMT Solver ⊃ SAT Solver

since

Theorem Prover ⊃ Prolog