Cohen, Liron, Rowe, Reuben (2018) Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. In: Leibniz International Proceedings in Informatics. Proceedings of the 27th EACSL Annual Conference on Computer Science Logic, CSL 2018. . LIPICS (doi:10.4230/LIPIcs.CSL.2018.16) (KAR id:67460)
PDF
Publisher pdf
Language: English
This work is licensed under a Creative Commons Attribution 4.0 International License.
|
|
Download (317kB)
Preview
|
Preview |
This file may not be suitable for users of assistive technology.
Request an accessible format
|
|
Official URL http://dx.doi.org/10.4230/LIPIcs.CSL.2018.16 |
Abstract
Transitive closure logic is a known extension of first-order logic obtained by introducing a
are a priori parametrized by a set of inductive definitions, the addition of the transitive closure
infinitary proof system for transitive closure logic which is an infinite descent-style counterpart
systems for first-order logic with inductive definitions, our infinitary system is complete for the
closure operator allows semantically meaningful complete restrictions to be defined using simple
the basis for an effective system for automating inductive reasoning.
Item Type: | Conference or workshop item (Proceeding) |
---|---|
DOI/Identification number: | 10.4230/LIPIcs.CSL.2018.16 |
Uncontrolled keywords: | Induction, Transitive Closure, Infinitary Proof Systems, Cyclic Proof Systems, Soundness, Completeness, Standard Semantics, Henkin Semantics |
Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Reuben Rowe |
Date Deposited: | 29 Jun 2018 13:45 UTC |
Last Modified: | 16 Feb 2021 13:55 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/67460 (The current URI for this page, for reference purposes) |
Rowe, Reuben: | ![]() |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):