Those terminologies confuse me. As I understand SAT solver: decide the satisfiability of propositional logic (using DPLL or Local Search).Decision procedure is a procedure to decide the satisfiability of a certain decidable first-order theory.SMT solver is a SAT solver + decision procedure.Theorem prover indicates something like Dynamic Logic, e.g. the KeY toolConstraint solver: I don't know.But I see people calling Z3 a theorem prover. So I don't know how to dishtinguish those terms. And what is the most general term for all of them? Thank you.
Distinguish Decision Procedure vs SMT solver vs Theorem prover vs Constraint solver
algorithms;terminology;reference request;decision problem