Logic programming is a programming language paradigm. In it, a programmer creates a bunch of axioms in the form of horn clauses, representing computations, which the implementation of the language then solves to generate the output.
My question is, are there any proof assistants based on logic programming? That is, are there any proof assistants whose proof language is a Logic programming language?
If not, is it because no one has bothered, or is there something fundamentally wrong with the idea?