TypiCal

Résumé:

We consider the problem of automating and checking the use of previously proved lemmas in the proof of some main theorem. In particular, we call the collection of such previously proved results a table and use a partial order on the table's entries to denote the (provability) dependency relationship between tabled items. We incorporate tables into sequent calculus proofs by performing two steps. 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 premise has the lemma inserted into the set of assumptions. Second, to ensure that lemmas are not reproved, we exploit the non-canonicity of focusing systems and specify two specific focusing disciplines for tabled formulas.

1. We allow only atomic formulas in tables. Then, by exploiting the fact that, in focusing systems, atoms can be assigned positive or negative polarity, we impose the following polarity discipline: atoms that are in the table are given positive polarity and those not in the table are given negative polarity.
2. We restrict tabled formulas to fixed point literals, that is, fixed points and their negations, and universally quantified fixed point literals, denoting both finite successes and finite failures. Then, by exploiting the fact that fixed points can be frozen and be treated like atoms, we impose a second focusing discipline: fixed points that are instances of a tabled formula are frozen and those that are not instances of a tabled formula are not frozen.

We show that, in some fragments of first-order-logic, the only existing proofs and open derivations are those that do not attempt to (re)prove a tabled formula: for the first discipline, we use the hereditary Harrop formulas fragment of intuitionistic logic and for the second discipline, we use the fragment of intuitionistic logic with fixed points used in \cite{tiu05eshol}, where only formulas constructed from positive connectives appear in the left-hand-side of sequents and all fixed points are noetherian.