Towards an Implicit Characterization of NCk

We define a hierarchy of term systems Tk by means of restrictions of the recursion schema. We essentially use a pointer technique together with tiering. We prove Tk NCk Tk+1 , for k 2. Special attention is put on the description of T2 and T3 and on the proof of T2 NC2 T3 . Such a hierarchy yields a characterization of NC.

• Type: Conference
• Year: 2006
• Where: CSL
• Authors: Guillaume Bonfante, Reinhard Kahle, Jean-Yves Marion, Isabel Oitavem
• Keywords: Automated Reasoning, CSL 2006, Pointer Technique, Recursion Schema, Tk NCk