Z3 is a theorem prover; it's a tool you would use to formally analyze a hardware logic design or a software program to ensure that it meets certain criteria (e.g. that it contains none of a certain class of security vulnerabilities). Theorem provers incorporate a lot of the same basic ideas as Prolog, but they're specialized tools (many have been written in Prolog). Prolog itself is a general-purpose programming language.