About: Towards Automated Reasoning in Herbrand Structures

Not logged in : Login

(Sponging disallowed)

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

About: Towards Automated Reasoning in Herbrand Structures Goto Sponge NotDistinct Permalink

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

Attributes	Values
type	http://eprints.org/ontology/ArticleEPrint http://eprints.org/ontology/EPrint Article Academic Article
seeAlso	HTML Summary of #73527 Towards Automated Reasoning in Herbrand Structures
sameAs	Towards Automated Reasoning in Herbrand Structures
http://eprints.org/ontology/hasAccepted	Towards Automated Reasoning in Herbrand Structures (PDF)
http://eprints.org/ontology/hasDocument	Towards Automated Reasoning in Herbrand Structures (PDF) Towards Automated Reasoning in Herbrand Structures (Other) Towards Automated Reasoning in Herbrand Structures (Other) Towards Automated Reasoning in Herbrand Structures (Other) Towards Automated Reasoning in Herbrand Structures (Other) Towards Automated Reasoning in Herbrand Structures (Other)
dc:hasVersion	Towards Automated Reasoning in Herbrand Structures (PDF)
Title	Towards Automated Reasoning in Herbrand Structures
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	2019-06-03
Creator	Liron Cohen Yoni Zohar Reuben N. S. Rowe
status	peer reviewed published
Publisher	Oxford University Press
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 prooftheoretic 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.
Is Part Of	Journal of Logic and Computation https://kar.kent.ac.uk/id/repository
list of authors	https://kar.kent.ac.uk/id/eprint/73527#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 #73527 Towards Automated Reasoning in Herbrand Structures

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, 17 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software