. . . . . . . . . "2019-06-03" . . . "Towards Automated Reasoning in Herbrand Structures"^^ . . . . . "Herbrand structures have the advantage, computationally speaking, of being guided by the definability of all elements in them. A salient feature of the logics induced by them is that they internally\r\nexhibit the induction scheme, thus providing a congenial, computationally-oriented framework for\r\nformal inductive reasoning. Nonetheless, their enhanced expressivity renders any effective proof\r\nsystem for them incomplete. Furthermore, the fact that they are not compact poses yet another prooftheoretic challenge. This paper offers several layers for coping with the inherent incompleteness and\r\nnon-compactness of these logics. First, two types of infinitary proof system are introduced\u2014one\r\nof infinite width and one of infinite height\u2014which manipulate infinite sequents and are sound and\r\ncomplete for the intended semantics. The restriction of these systems to finite sequents induces a\r\ncompleteness result for finite entailments. Then, in search of effectiveness, two finite approximations\r\nof these systems are presented and explored. Interestingly, the approximation of the infinite-width\r\nsystem via an explicit induction scheme turns out to be weaker than the effective cyclic fragment of the\r\ninfinite-height system."^^ . . . . . . . . . . .