Non-well-founded proof system for Transitive Closure Logic

## Authors: Liron Cohen and Reuben Rowe

## Paper Information

Title: | Non-well-founded proof system for Transitive Closure Logic |

Authors: | Liron Cohen and Reuben Rowe |

Proceedings: | WiL Short Papers and Abstracts |

Editors: | Valeria de Paiva, Amy Felty and Ursula Martin |

Keywords: | Transitive closure logic, proof theory, infinitary and cyclic systems, induction |

Abstract: | ABSTRACT. Transitive closure logic is obtained by a modest addition to first-order logic that affords enormous expressive power. Most importantly, it provides a uniform way of capturing finitary inductive definitions. Thus, particular induction principles do not need to be added to the logic; instead, all induction schemes are available within a single, unified language. We here present a non-well-founded proof system for transitive closure logic which is complete for the standard semantics. This system captures implicit induction, and its soundness is underpinned by the principle of infinite descent. We also consider its subsystem of cyclic proofs. |

Pages: | 2 |

Talk: | Jul 08 15:15 (Session 40S) |

Paper: |