Computational logic consists of those approaches to general logic in which insights from the theory of computation play an essential part, for example in decision problems in logic, effective semantics of logic, computationally effective frameworks for proofs theory and theorem proving.
The area of logic and artificial intelligence concerned with automating logical inference, implementing theorem provers, and the foundations of logic programming.
A proof-assistant is a computer program with which a user can construct completely formal mathematical proofs in some kind of logical system. In contrast to a theorem prover, a proof-assistant cannot find proofs on its own