My talk will survey how proof theory (in the sense of Gentzen and Girard) has interacted with the logic programming literature over the past 35 years.
I will not speak directly about proving properties of logic programs in this talk. Of course, one uses logic and proof theory as a foundation of programming to have a framework where reasoning about programs is more direct and transparent. But this is not the topic for my talk.
Proving properties of logic programs is an important and doable problem. If you limit yourself to Horn clauses, then provability using such programs can be characterized as a simple inductive definition. I'm sure that one can easily prove that append is associative or plus is commutative using induction within Isabelle/HOL or Coq. To what extent you can do this automatically is interesting and probably open for new ideas.
A lesser-known theorem prover, Abella (abella-prover.org), was designed to reason directly with relational specifications (aka logic programs). The main focus of Abella has been to reason about the meta-theory of specification languages such as the lambda-calculus, the pi-calculus, etc. The operational semantics of these languages is often given as logic programs (also known as structured operational semantics and natural semantics). Thus, reasoning about such logic programs is also a way to prove theorems about, for example, the lambda-calculus.
Examples of Abella proofs (found interactively) about list manipulation functions can be found at http://abella-prover.org/examples/first-order/lists.html.