Nondeterminism and Language Design in Deep Inference: A Proof Theoretic Approach to Logic Programming