Cultural advice

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

Aboriginal and Torres Strait Islander peoples are advised that ANU Library collections may include images, names, voices, and other representations of deceased persons.

Material in the collection may contain terms, language or views that reflect the period in which the item was created and may be considered inappropriate today.

Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents

Simple item page
dc.contributor.authorGore, Rajeev
dc.contributor.authorLellmann, Bjorn
dc.contributor.editorCerrito, S.
dc.contributor.editorPopescu, A .
dc.coverage.spatialLondon United Kingdom
dc.date.accessioned2023-11-29T02:46:55Z
dc.date.createdSeptember 3-5 2019
dc.date.issued2019-08-14
dc.date.updated2022-08-28T08:15:57Z
dc.description.abstractWe give a linear nested sequent calculus for the basic normal tense logic 𝖪𝗍 We show that the calculus enables backwards proof-search, counter-model construction and syntactic cut-elimination. Linear nested sequents thus provide the minimal amount of nesting necessary to provide an adequate proof-theory for modal logics containing converse. As a bonus, this yields a cut-free calculus for symmetric modal logic KB.en_AU
dc.format.mimetypeapplication/pdfen_AU
dc.identifier.citationGoré, R., Lellmann, B. (2019). Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents. In: Cerrito, S., Popescu, A. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2019. Lecture Notes in Computer Science(), vol 11714. Springer, Cham. https://doi.org/10.1007/978-3-030-29026-9_11en_AU
dc.identifier.isbn978-3-030-29026-9en_AU
dc.identifier.issn0302-9743en_AU
dc.identifier.urihttp://hdl.handle.net/1885/307522
dc.language.isoen_AUen_AU
dc.publisherSpringer, Chamen_AU
dc.relation.ispartofseries28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2019en_AU
dc.rights© 2019 Springer Nature Switzerland AGen_AU
dc.sourceAutomated Reasoning with Analytic Tableaux and Related Methodsen_AU
dc.titleSyntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequentsen_AU
dc.typeConference paperen_AU
local.bibliographicCitation.lastpage202en_AU
local.bibliographicCitation.startpage185en_AU
local.contributor.affiliationGore, Rajeev, College of Engineering and Computer Science, ANUen_AU
local.contributor.affiliationLellmann, Bjorn, Technical University of Viennaen_AU
local.contributor.authoruidGore, Rajeev, u9409448en_AU
local.description.embargo2099-12-31
local.description.notesImported from ARIESen_AU
local.description.refereedYes
local.identifier.absfor461303 - Computational logic and formal languagesen_AU
local.identifier.ariespublicationa383154xPUB11846en_AU
local.identifier.doi10.1007/978-3-030-29026-9_11en_AU
local.identifier.essn1611-3349en_AU
local.identifier.scopusID2-s2.0-85077118412
local.identifier.thomsonIDWOS:000711904000011
local.publisher.urlhttps://link.springer.com/en_AU
local.type.statusPublished Versionen_AU

Downloads

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
978-3-030-29026-9.pdf
Size:
435.09 KB
Format:
Adobe Portable Document Format
Description:
Download

Collections

ANU Research Publications

DSpace software copyright © 2002-2026 LYRASIS