Towards automated reasoning in Herbrand structures. / Cohen, Liron; Rowe, Reuben; Zohar, Yoni.

In: Journal of Logic and Computation, Vol. 29, No. 5, 09.2019, p. 693-721.

Research output: Contribution to journalArticlepeer-review

Published

Standard

Towards automated reasoning in Herbrand structures. / Cohen, Liron; Rowe, Reuben; Zohar, Yoni.

In: Journal of Logic and Computation, Vol. 29, No. 5, 09.2019, p. 693-721.

Research output: Contribution to journalArticlepeer-review

Harvard

Cohen, L, Rowe, R & Zohar, Y 2019, 'Towards automated reasoning in Herbrand structures', Journal of Logic and Computation, vol. 29, no. 5, pp. 693-721. https://doi.org/10.1093/logcom/exz011

APA

Cohen, L., Rowe, R., & Zohar, Y. (2019). Towards automated reasoning in Herbrand structures. Journal of Logic and Computation, 29(5), 693-721. https://doi.org/10.1093/logcom/exz011

Vancouver

Cohen L, Rowe R, Zohar Y. Towards automated reasoning in Herbrand structures. Journal of Logic and Computation. 2019 Sep;29(5):693-721. https://doi.org/10.1093/logcom/exz011

Author

Cohen, Liron ; Rowe, Reuben ; Zohar, Yoni. / Towards automated reasoning in Herbrand structures. In: Journal of Logic and Computation. 2019 ; Vol. 29, No. 5. pp. 693-721.

BibTeX

@article{5f9d6a93577b4d0a8df4beb2be4c9b27,
title = "Towards automated reasoning in Herbrand structures",
abstract = "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 proof-theoretic 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.",
author = "Liron Cohen and Reuben Rowe and Yoni Zohar",
year = "2019",
month = sep,
doi = "10.1093/logcom/exz011",
language = "English",
volume = "29",
pages = "693--721",
journal = "Journal of Logic and Computation",
issn = "0955-792X",
publisher = "Oxford University Press",
number = "5",

}

RIS

TY - JOUR

T1 - Towards automated reasoning in Herbrand structures

AU - Cohen, Liron

AU - Rowe, Reuben

AU - Zohar, Yoni

PY - 2019/9

Y1 - 2019/9

N2 - 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 proof-theoretic 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.

AB - 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 proof-theoretic 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.

U2 - 10.1093/logcom/exz011

DO - 10.1093/logcom/exz011

M3 - Article

VL - 29

SP - 693

EP - 721

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

SN - 0955-792X

IS - 5

ER -