About: Infinitary and Cyclic Proof Systems for Transitive Closure Logic

Not logged in : Login

(Sponging disallowed)

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: Infinitary and Cyclic Proof Systems for Transitive Closure Logic Goto Sponge NotDistinct Permalink

An Entity of Type : bibo:Manuscript, within Data Space : demo.openlinksw.com associated with source document(s)

Attributes	Values
type	http://eprints.org/ontology/EPrint http://eprints.org/ontology/MonographEPrint Article Manuscript
seeAlso	HTML Summary of #65886 Infinitary and Cyclic Proof Systems for Transitive Closure Logic
http://eprints.org/ontology/hasDocument	Infinitary and Cyclic Proof Systems for Transitive Closure Logic (PDF) Infinitary and Cyclic Proof Systems for Transitive Closure Logic (Other) Infinitary and Cyclic Proof Systems for Transitive Closure Logic (Other) Infinitary and Cyclic Proof Systems for Transitive Closure Logic (Other) Infinitary and Cyclic Proof Systems for Transitive Closure Logic (Other) Infinitary and Cyclic Proof Systems for Transitive Closure Logic (Other)
Title	Infinitary and Cyclic Proof Systems for Transitive Closure Logic
described by	https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3 https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
Date	2018
Creator	Liron Cohen Reuben N. S. Rowe
status	published
Publisher	arXiv
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.
Is Part Of	https://kar.kent.ac.uk/id/repository
Subject	QA 9 Formal systems, logics
list of authors	https://kar.kent.ac.uk/id/eprint/65886#authors
is topic of	https://www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3 https://raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
is primary topic of	HTML Summary of #65886 Infinitary and Cyclic Proof Systems for Transitive Closure Logic

Faceted Search & Find service v1.17_git144 as of Jul 26 2024

Alternative Linked Data Documents: iSPARQL | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3331 as of Aug 25 2024, on Linux (x86_64-ubuntu_noble-linux-glibc2.38-64), Single-Server Edition (378 GB total memory, 49 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software