This HTML5 document contains 28 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n2https://kar.kent.ac.uk/id/eprint/
wdrshttp://www.w3.org/2007/05/powder-s#
n19http://purl.org/ontology/bibo/status/
dchttp://purl.org/dc/elements/1.1/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n6https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n8http://eprints.org/ontology/
n20https://kar.kent.ac.uk/id/eprint/73527#
bibohttp://purl.org/ontology/bibo/
n16https://kar.kent.ac.uk/id/publication/
n13https://kar.kent.ac.uk/73527/
n4https://kar.kent.ac.uk/id/org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n9https://kar.kent.ac.uk/id/document/
n10https://kar.kent.ac.uk/id/
n18doi:10.1093/logcom/
xsdhhttp://www.w3.org/2001/XMLSchema#
n11https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n7https://kar.kent.ac.uk/id/person/

Statements

Subject Item
n2:73527
rdf:type
n8:ArticleEPrint n8:EPrint bibo:AcademicArticle bibo:Article
rdfs:seeAlso
n13:
owl:sameAs
n18:exz011
n8:hasAccepted
n9:3174674
n8:hasDocument
n9:3174692 n9:3174674 n9:3174688 n9:3174689 n9:3174690 n9:3174691
dc:hasVersion
n9:3174674
dcterms:title
Towards Automated Reasoning in Herbrand Structures
wdrs:describedby
n6:export_kar_RDFN3.n3 n11:export_kar_RDFN3.n3
dcterms:date
2019-06-03
dcterms:creator
n7:ext-r.n.s.rowe@kent.ac.uk n7:ext-ab9ce8caa44f679bfc5d7564bd603fd8 n7:ext-1efe0342b9adf7423d4e80571b4b0091
bibo:status
n19:peerReviewed n19:published
dcterms:publisher
n4:ext-ffae441f908983694f410e3721f2491d
bibo: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.
dcterms:isPartOf
n10:repository n16:ext-0955792X
bibo:authorList
n20:authors