Proof Manipulations for Logic Programming Proof Systems
Tatjana Lutovac, James Harland · 2007
Logic programs consist of formulas of mathematical logic and various proof-theoretic techniques can be used to design and analyse execution models for such programs. In this paper we present some initial work on the problem of making systematic the design of logic programming languages. In particular, we identify and discuss several key properties of proofs. A important aspect of this examination is a a more precise specification of sequent calculi inference rules in order to study permutation properties, which are key aspect of the design of logic programming systems. We also show how this specification can be used to manipulate proofs, as well as to establish properties of sets of inference rules. In addition we describe how Boolean expressions can be used to detect unused formulae in a proof, which is important for debugging purposes. Keywords: sequent calculi, logic programming, search strategies, substructural logic. 1