Artykuł w czasopiśmie
Brak miniatury
Licencja
CC-BYCC-BY - Uznanie autorstwa
 

Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity

Uproszczony widok
dc.abstract.enSentential Calculus with Identity ( SCI ) is an extension of classical propositional logic, featuring a new connective of identity between formulas. In SCI two formulas are said to be identical if they share the same denotation. In the semantics of the logic, truth values are distinguished from denotations, hence the identity connective is strictly stronger than classical equivalence. In this paper we present a sound, complete, and terminating algorithm deciding the satisfiability of SCI -formulas, based on labelled tableaux. To the best of our knowledge, it is the first implemented decision procedure for SCI which runs in NP, i.e., is complexity-optimal. The obtained complexity bound is a result of dividing derivation rules in the algorithm into two sets: decomposition and equality rules, whose interplay yields derivation trees with branches of polynomial length with respect to the size of the investigated formula. We describe an implementation of the procedure and compare its performance with implementations of other calculi for SCI (for which, however, the termination results were not established). We show possible refinements of our algorithm and discuss the possibility of extending it to other non-Fregean logics.
dc.affiliationUniwersytet Warszawski
dc.conference.datefinish2021-07-15
dc.conference.datestart2021-07-12
dc.conference.placeVirtual Event
dc.conference.seriesInternational Conference on Automated Deduction
dc.conference.seriesInternational Conference on Automated Deduction
dc.conference.seriesshortcutCADE
dc.conference.shortcutCADE 2021
dc.conference.weblinkhttps://www.cs.cmu.edu/~mheule/CADE28/
dc.contributor.authorGolińska-Pilarek, Joanna
dc.contributor.authorHuuskonen, Taneli
dc.contributor.authorZawidzki, Michał
dc.date.accessioned2024-01-26T09:30:23Z
dc.date.available2024-01-26T09:30:23Z
dc.date.copyright2021-07-05
dc.date.issued2021
dc.description.accesstimeBEFORE_PUBLICATION
dc.description.financePublikacja bezkosztowa
dc.description.versionFINAL_PUBLISHED
dc.identifier.doi10.1007/978-3-030-79876-5_3
dc.identifier.urihttps://repozytorium.uw.edu.pl//handle/item/121492
dc.identifier.weblinkhttps://link.springer.com/chapter/10.1007/978-3-030-79876-5_3
dc.languageeng
dc.pbn.affiliationphilosophy
dc.relation.pages41-57
dc.rightsCC-BY
dc.sciencecloudnosend
dc.subject.enSentential Calculus with Identity
dc.subject.ennon-Fregean logics
dc.subject.enlabelled tableaux
dc.subject.endecision procedure
dc.subject.entermination
dc.subject.encomputational complexity
dc.titleTableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity
dc.typeJournalArticle
dspace.entity.typePublication