### On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences

#### David M. Cerna

In: T.B.D, T.B.D (ed.), Proceedings of T.B.D, pp. 1-17. 2019. T.B.D. [pdf]@

author = {David M. Cerna},

title = {{On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences}},

booktitle = {{T.B.D}},

language = {english},

abstract = {We introduce a measure of complexity based on formula occurrence within instance proofs of an inductive statement. Our measure is closely related to {\em Herbrand Sequent length}, but instead of capturing the number of necessary term instantiations, it captures the finite representational difficulty of a recursive sequence of proofs. We restrict ourselves to a class of unsatisfiable primitive recursively defined negation normal form first-order sentences, referred to as {\em abstract sentences}, which capture many problems of interest; for example, variants of the {\em infinitary pigeonhole principle}. This class of sentences has been particularly useful for inductive formal proof analysis and proof transformation. Together our complexity measure and abstract sentences allow use to capture a notion of {\em tractability} with respect to state-of-the-art approaches to inductive theorem proving, namely {\em loop discovery} and {\em tree grammar} based inductive theorem provers. We provide a complexity analysis of two important abstract sentences based on the infinitary pigeonhole principle which we conjecture represent the upper limits of tractability and the intractable with respect to the current approaches. },

pages = {1--17},

isbn_issn = {T.B.D},

year = {2019},

editor = {T.B.D},

refereed = {yes},

length = {17},

conferencename = {T.B.D}

}

**inproceedings**{RISC5841,author = {David M. Cerna},

title = {{On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences}},

booktitle = {{T.B.D}},

language = {english},

abstract = {We introduce a measure of complexity based on formula occurrence within instance proofs of an inductive statement. Our measure is closely related to {\em Herbrand Sequent length}, but instead of capturing the number of necessary term instantiations, it captures the finite representational difficulty of a recursive sequence of proofs. We restrict ourselves to a class of unsatisfiable primitive recursively defined negation normal form first-order sentences, referred to as {\em abstract sentences}, which capture many problems of interest; for example, variants of the {\em infinitary pigeonhole principle}. This class of sentences has been particularly useful for inductive formal proof analysis and proof transformation. Together our complexity measure and abstract sentences allow use to capture a notion of {\em tractability} with respect to state-of-the-art approaches to inductive theorem proving, namely {\em loop discovery} and {\em tree grammar} based inductive theorem provers. We provide a complexity analysis of two important abstract sentences based on the infinitary pigeonhole principle which we conjecture represent the upper limits of tractability and the intractable with respect to the current approaches. },

pages = {1--17},

isbn_issn = {T.B.D},

year = {2019},

editor = {T.B.D},

refereed = {yes},

length = {17},

conferencename = {T.B.D}

}