Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. / Cohen, Liron; Rowe, Reuben.

27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Vol. 119 Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2018. p. 17:1-17:16 (Leibniz International Proceedings in Informatics (LIPIcs)).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published

Standard

Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. / Cohen, Liron; Rowe, Reuben.

27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Vol. 119 Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2018. p. 17:1-17:16 (Leibniz International Proceedings in Informatics (LIPIcs)).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

Cohen, L & Rowe, R 2018, Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. in 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). vol. 119, Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, pp. 17:1-17:16. https://doi.org/10.4230/LIPIcs.CSL.2018.17

APA

Cohen, L., & Rowe, R. (2018). Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) (Vol. 119, pp. 17:1-17:16). (Leibniz International Proceedings in Informatics (LIPIcs)). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.CSL.2018.17

Vancouver

Cohen L, Rowe R. Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Vol. 119. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. 2018. p. 17:1-17:16. (Leibniz International Proceedings in Informatics (LIPIcs)). https://doi.org/10.4230/LIPIcs.CSL.2018.17

Author

Cohen, Liron ; Rowe, Reuben. / Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Vol. 119 Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2018. pp. 17:1-17:16 (Leibniz International Proceedings in Informatics (LIPIcs)).

BibTeX

@inproceedings{b35a97e5471e41e1bd14770ef0ca7c15,
title = "Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent",
abstract = "Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. In this paper we present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-order logic with inductive definitions, our infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria. Consequently, the restriction to regular infinitary (i.e. cyclic) proofs provides the basis for an effective system for automating inductive reasoning.",
author = "Liron Cohen and Reuben Rowe",
year = "2018",
month = sep,
day = "4",
doi = "10.4230/LIPIcs.CSL.2018.17",
language = "English",
volume = "119",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
pages = "17:1--17:16",
booktitle = "27th EACSL Annual Conference on Computer Science Logic (CSL 2018)",

}

RIS

TY - GEN

T1 - Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent

AU - Cohen, Liron

AU - Rowe, Reuben

PY - 2018/9/4

Y1 - 2018/9/4

N2 - Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. In this paper we present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-order logic with inductive definitions, our infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria. Consequently, the restriction to regular infinitary (i.e. cyclic) proofs provides the basis for an effective system for automating inductive reasoning.

AB - Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. In this paper we present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-order logic with inductive definitions, our infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria. Consequently, the restriction to regular infinitary (i.e. cyclic) proofs provides the basis for an effective system for automating inductive reasoning.

U2 - 10.4230/LIPIcs.CSL.2018.17

DO - 10.4230/LIPIcs.CSL.2018.17

M3 - Conference contribution

VL - 119

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 17:1-17:16

BT - 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

PB - Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

ER -