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
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

formal inductive reasoning. Nonetheless, their enhanced expressivity renders any effective proof

non-compactness of these logics. First, two types of infinitary proof system are introduced—one

complete for the intended semantics. The restriction of these systems to finite sequents induces a

of these systems are presented and explored. Interestingly, the approximation of the infinite-width

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