Incorporating tables into proofs

nigam at lix.inria.fr dale.miller at inria.fr Abstract. We consider the problem of automating and checking the use of previously proved lemmas in the proof of some main theorem. In particular, we shall call the collection of such previously proved results a table and use a partial order on the table’s entries to denote the (prov-ability) dependency relationship between tabled items. Tables can arise in a number of situations: in automated deduction via previously proved subgoals or in interactive theorem proving via a sequence of lemmas in-troduced by a user to direct the proof system towards its final theorem. We link tables involving literals with sequent calculus proofs using two ideas. First, cuts are used to incorporate tabled items into a proof: one premise of the cut requires a proof of the lemma and the other branch of the cut inserts the lemma into the set of assumptions. Second, in order to require that inserted lemma is not reproved, we exploit the fact that in focused proofs, atoms can have different polarity. As we shall see, such a use of focused proofs along with literals of either positive or negative po-larities allows tables to be merged with proofs in such a way that simple logic engines that do focused proof search (such as logic programming interpreters) will be able to check proofs for correctness with guarantees that previous work will not be redone. We also discuss how such integra-tion of tables into proof can, at times, significantly compress proofs and discuss how this work might be used within a proof carry code setting.