Generic Modal Cut Elimination Applied to Conditional Logics

We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal...

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2011-03, Vol.7, Issue 1
Main Authors: Pattinson, Dirk, Schröder, Lutz
Format: Article
Language:English
Subjects:
computer science - logic in computer science
f.4.1, i.2.3
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c278t-9cdab2aa284e7e65d4ad7e48359e71c0ae98b606d6e3b4db7f0454223b14dd7c3
cites cdi_FETCH-LOGICAL-c278t-9cdab2aa284e7e65d4ad7e48359e71c0ae98b606d6e3b4db7f0454223b14dd7c3
container_end_page
container_issue
container_start_page
container_title Logical methods in computer science
container_volume 7, Issue 1
creator Pattinson, Dirk
Schröder, Lutz
description We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal modal logic. We give extensive example instantiations of our framework to various conditional logics. For these, we obtain fully internalised calculi which are substantially simpler than those known in the literature, along with leaner proofs of cut elimination and complexity. In one case, conditional logic with modus ponens and conditional excluded middle, cut elimination and complexity were explicitly stated as open in the literature.
doi_str_mv 10.2168/LMCS-7(1:4)2011
format article
fullrecord <record><control><sourceid>doaj_cross</sourceid><recordid>TN_cdi_doaj_primary_oai_doaj_org_article_69b489e64d5844f5b7508569f7aedcb5</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><doaj_id>oai_doaj_org_article_69b489e64d5844f5b7508569f7aedcb5</doaj_id><sourcerecordid>oai_doaj_org_article_69b489e64d5844f5b7508569f7aedcb5</sourcerecordid><originalsourceid>FETCH-LOGICAL-c278t-9cdab2aa284e7e65d4ad7e48359e71c0ae98b606d6e3b4db7f0454223b14dd7c3</originalsourceid><addsrcrecordid>eNpNkEtLw0AUhQdRsNSu3Wapi9h5P3RVQq2FFBfqephXypQ0UyZx4b83sSLezbkcDt_iA-AWwQeMuFzWu-qtFHfokd5jiNAFmCHJYcmUoJf__muw6PsDHI8QJDGfgadN6EKOrtglb9qi-hyKdRuPsTNDTF2xOp3aGHwxpKJKnY9TOc7qtI-uvwFXjWn7sPjNOfh4Xr9XL2X9utlWq7p0WMihVM4bi43BkgYROPPUeBGoJEwFgRw0QUnLIfc8EEu9FQ2kjGJMLKLeC0fmYHvm-mQO-pTj0eQvnUzUP0XKe23yEF0bNFeWShU49UxS2jArGJSMq0aY4J1lI2t5Zrmc-j6H5o-HoJ5U6kmlFhppqieV5BtaC2YT</addsrcrecordid><sourcetype>Open Website</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype></control><display><type>article</type><title>Generic Modal Cut Elimination Applied to Conditional Logics</title><source>EZB Electronic Journals Library</source><creator>Pattinson, Dirk ; Schröder, Lutz</creator><creatorcontrib>Pattinson, Dirk ; Schröder, Lutz</creatorcontrib><description>We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal modal logic. We give extensive example instantiations of our framework to various conditional logics. For these, we obtain fully internalised calculi which are substantially simpler than those known in the literature, along with leaner proofs of cut elimination and complexity. In one case, conditional logic with modus ponens and conditional excluded middle, cut elimination and complexity were explicitly stated as open in the literature.</description><identifier>ISSN: 1860-5974</identifier><identifier>EISSN: 1860-5974</identifier><identifier>DOI: 10.2168/LMCS-7(1:4)2011</identifier><language>eng</language><publisher>Logical Methods in Computer Science e.V</publisher><subject>computer science - logic in computer science ; f.4.1, i.2.3</subject><ispartof>Logical methods in computer science, 2011-03, Vol.7, Issue 1</ispartof><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c278t-9cdab2aa284e7e65d4ad7e48359e71c0ae98b606d6e3b4db7f0454223b14dd7c3</citedby><cites>FETCH-LOGICAL-c278t-9cdab2aa284e7e65d4ad7e48359e71c0ae98b606d6e3b4db7f0454223b14dd7c3</cites><orcidid>0000-0002-3146-5906</orcidid></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,780,784,27924,27925</link.rule.ids></links><search><creatorcontrib>Pattinson, Dirk</creatorcontrib><creatorcontrib>Schröder, Lutz</creatorcontrib><title>Generic Modal Cut Elimination Applied to Conditional Logics</title><title>Logical methods in computer science</title><description>We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal modal logic. We give extensive example instantiations of our framework to various conditional logics. For these, we obtain fully internalised calculi which are substantially simpler than those known in the literature, along with leaner proofs of cut elimination and complexity. In one case, conditional logic with modus ponens and conditional excluded middle, cut elimination and complexity were explicitly stated as open in the literature.</description><subject>computer science - logic in computer science</subject><subject>f.4.1, i.2.3</subject><issn>1860-5974</issn><issn>1860-5974</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2011</creationdate><recordtype>article</recordtype><sourceid>DOA</sourceid><recordid>eNpNkEtLw0AUhQdRsNSu3Wapi9h5P3RVQq2FFBfqephXypQ0UyZx4b83sSLezbkcDt_iA-AWwQeMuFzWu-qtFHfokd5jiNAFmCHJYcmUoJf__muw6PsDHI8QJDGfgadN6EKOrtglb9qi-hyKdRuPsTNDTF2xOp3aGHwxpKJKnY9TOc7qtI-uvwFXjWn7sPjNOfh4Xr9XL2X9utlWq7p0WMihVM4bi43BkgYROPPUeBGoJEwFgRw0QUnLIfc8EEu9FQ2kjGJMLKLeC0fmYHvm-mQO-pTj0eQvnUzUP0XKe23yEF0bNFeWShU49UxS2jArGJSMq0aY4J1lI2t5Zrmc-j6H5o-HoJ5U6kmlFhppqieV5BtaC2YT</recordid><startdate>20110317</startdate><enddate>20110317</enddate><creator>Pattinson, Dirk</creator><creator>Schröder, Lutz</creator><general>Logical Methods in Computer Science e.V</general><scope>AAYXX</scope><scope>CITATION</scope><scope>DOA</scope><orcidid>https://orcid.org/0000-0002-3146-5906</orcidid></search><sort><creationdate>20110317</creationdate><title>Generic Modal Cut Elimination Applied to Conditional Logics</title><author>Pattinson, Dirk ; Schröder, Lutz</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c278t-9cdab2aa284e7e65d4ad7e48359e71c0ae98b606d6e3b4db7f0454223b14dd7c3</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2011</creationdate><topic>computer science - logic in computer science</topic><topic>f.4.1, i.2.3</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Pattinson, Dirk</creatorcontrib><creatorcontrib>Schröder, Lutz</creatorcontrib><collection>CrossRef</collection><collection>Directory of Open Access Journals</collection><jtitle>Logical methods in computer science</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Pattinson, Dirk</au><au>Schröder, Lutz</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Generic Modal Cut Elimination Applied to Conditional Logics</atitle><jtitle>Logical methods in computer science</jtitle><date>2011-03-17</date><risdate>2011</risdate><volume>7, Issue 1</volume><issn>1860-5974</issn><eissn>1860-5974</eissn><abstract>We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal modal logic. We give extensive example instantiations of our framework to various conditional logics. For these, we obtain fully internalised calculi which are substantially simpler than those known in the literature, along with leaner proofs of cut elimination and complexity. In one case, conditional logic with modus ponens and conditional excluded middle, cut elimination and complexity were explicitly stated as open in the literature.</abstract><pub>Logical Methods in Computer Science e.V</pub><doi>10.2168/LMCS-7(1:4)2011</doi><orcidid>https://orcid.org/0000-0002-3146-5906</orcidid><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 1860-5974
ispartof Logical methods in computer science, 2011-03, Vol.7, Issue 1
issn 1860-5974
1860-5974
language eng
recordid cdi_doaj_primary_oai_doaj_org_article_69b489e64d5844f5b7508569f7aedcb5
source EZB Electronic Journals Library
subjects computer science - logic in computer science
f.4.1, i.2.3
title Generic Modal Cut Elimination Applied to Conditional Logics
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-27T17%3A14%3A17IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-doaj_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Generic%20Modal%20Cut%20Elimination%20Applied%20to%20Conditional%20Logics&rft.jtitle=Logical%20methods%20in%20computer%20science&rft.au=Pattinson,%20Dirk&rft.date=2011-03-17&rft.volume=7,%20Issue%201&rft.issn=1860-5974&rft.eissn=1860-5974&rft_id=info:doi/10.2168/LMCS-7(1:4)2011&rft_dat=%3Cdoaj_cross%3Eoai_doaj_org_article_69b489e64d5844f5b7508569f7aedcb5%3C/doaj_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c278t-9cdab2aa284e7e65d4ad7e48359e71c0ae98b606d6e3b4db7f0454223b14dd7c3%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rfr_iscdi=true