Skip to main content

Towards Automated Reasoning in Herbrand Structures

Cohen, Liron, Rowe, Reuben, Zohar, Yoni (2019) Towards Automated Reasoning in Herbrand Structures. Journal of Logic and Computation, . ISSN 0955-792X. (doi:10.1093/logcom/exz011) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided)

PDF - Author's Accepted Manuscript
Restricted to Repository staff only until 3 June 2020.
Contact us about this Publication Download (369kB)
Official URL


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 exhibit the induction scheme, thus providing a congenial, computationally-oriented framework for formal inductive reasoning. Nonetheless, their enhanced expressivity renders any effective proof system 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 non-compactness of these logics. First, two types of infinitary proof system are introduced—one of infinite width and one of infinite height—which manipulate infinite sequents and are sound and complete for the intended semantics. The restriction of these systems to finite sequents induces a completeness result for finite entailments. Then, in search of effectiveness, two finite approximations of these systems are presented and explored. Interestingly, the approximation of the infinite-width system via an explicit induction scheme turns out to be weaker than the effective cyclic fragment of the infinite-height system.

Item Type: Article
DOI/Identification number: 10.1093/logcom/exz011
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Reuben Rowe
Date Deposited: 17 Apr 2019 15:40 UTC
Last Modified: 08 Jul 2019 08:27 UTC
Resource URI: (The current URI for this page, for reference purposes)
Rowe, Reuben:
  • Depositors only (login required):


Downloads per month over past year