{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,28]],"date-time":"2025-06-28T11:26:39Z","timestamp":1751109999516,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Sentential Calculus with Identity (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {SCI}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>SCI<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>) is an extension of classical propositional logic, featuring a new connective of identity between formulas. In <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {SCI}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>SCI<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> 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 <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {SCI}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>SCI<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-formulas, based on labelled tableaux. To the best of our knowledge, it is the first implemented decision procedure for <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {SCI}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>SCI<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> which runs in <jats:sc>NP<\/jats:sc>, i.e., is complexity-optimal. The obtained complexity bound is a result of dividing derivation rules in the algorithm into two sets: <jats:italic>decomposition<\/jats:italic> and <jats:italic>equality<\/jats:italic> 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 <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathsf {SCI}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mi>SCI<\/mml:mi>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> (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.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_3","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"41-57","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8546-2615","authenticated-orcid":false,"given":"Joanna","family":"Goli\u0144ska-Pilarek","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7882-8236","authenticated-orcid":false,"given":"Taneli","family":"Huuskonen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2909-5923","authenticated-orcid":false,"given":"Micha\u0142","family":"Zawidzki","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Bloom, S.L., Suszko, R.: Semantics for the sentential calculus with identity. Studia Logica 28(1), 77\u201381 (1971). https:\/\/doi.org\/10.1007\/BF02124265","DOI":"10.1007\/BF02124265"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Bloom, S.L., Suszko, R.: Investigations into the sentential calculus with identity. Notre Dame Journal of Formal Logic 13(3), 289\u2013308 (1972). https:\/\/doi.org\/10.1305\/ndjfl\/1093890617","DOI":"10.1305\/ndjfl\/1093890617"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Chlebowski, Szymon: Sequent Calculi for $${\\sf SCI}$$. Studia Logica 106(3), 541\u2013563 (2017). https:\/\/doi.org\/10.1007\/s11225-017-9754-8","DOI":"10.1007\/s11225-017-9754-8"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Chlebowski, S., Leszczy\u0144ska-Jasion, D.: An investigation into intuitionistic logic with identity. Bulletin of the Section of Logic 48(4), 259\u2013283 (2019). https:\/\/doi.org\/10.18778\/0138-0680.48.4.02","DOI":"10.18778\/0138-0680.48.4.02"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Goli\u0144ska-Pilarek, J.: Rasiowa-sikorski proof system for the non-Fregean sentential logic $${\\sf SCI}$$. Journal of Applied Non-Classical Logics 17(4), 511\u2013519 (2007). https:\/\/doi.org\/10.3166\/jancl.17.511-519","DOI":"10.3166\/jancl.17.511-519"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Goli\u0144ska-Pilarek, J.: On the Minimal Non-Fregean Grzegorczyk Logic. Studia Logica 104(2), 209\u2013234 (2016). https:\/\/doi.org\/10.1007\/s11225-015-9635-y","DOI":"10.1007\/s11225-015-9635-y"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Goli\u0144ska-Pilarek, J., Huuskonen, T.: Number of extensions of non-Fregean logics. Journal of Philosophical Logic 34(2), 193\u2013206 (2005). https:\/\/doi.org\/10.1007\/s10992-004-6366-3","DOI":"10.1007\/s10992-004-6366-3"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Goli\u0144ska-Pilarek, J., Huuskonen, T.: Non-Fregean propositional logic with quantifiers. Notre Dame Journal of Formal Logic 57(2), 249\u2013279 (2016). https:\/\/doi.org\/10.1215\/00294527-3470547","DOI":"10.1215\/00294527-3470547"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Goli\u0144ska-Pilarek, J., Huuskonen, T.: A mystery of Grzegorczyk\u2019s logic of descriptions. In: Garrido, A., Wybraniec-Skardowska, U. (eds.) The Lvov-Warsaw School. Past and Present, pp. 731\u2013745. Studies in Universal Logic, Springer Nature (2018). https:\/\/doi.org\/10.1007\/978-3-319-65430-0_51","DOI":"10.1007\/978-3-319-65430-0_51"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Goli\u0144ska-Pilarek, J., Welle, M.: Deduction in non-Fregean propositional logic $${\\sf SCI}$$. Axioms 8, 115 (2019). https:\/\/doi.org\/10.3390\/axioms8040115","DOI":"10.3390\/axioms8040115"},{"key":"3_CR11","unstructured":"Goli\u0144ska-Pilarek, J., Zawidzki, M.: Tableau-based decision procedure for the logic SCI. In: Gigante, N., Mari, F., Orlandini, A. (eds.) Proceedings of the 1st Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, co-located with the 18th International Conference of the Italian Association for Artificial Intelligence, OVERLAY@AI*IA 2019, Rende, Italy, November 19-20, 2019. CEUR Workshop Proceedings, vol. 2509, pp. 23-28 (2019)"},{"key":"3_CR12","unstructured":"Goli\u0144ska-Pilarek, J., Huuskonen, T., Zawidzki, M.: Tableau-based decision procedure for non-fregean logic of sentential identity (2021), arXiv: 2104.14697"},{"key":"3_CR13","unstructured":"Ishii, T.: Propositional calculus with identity. Bulletin of the Section of Logic 27(3), 96\u2013104 (1998)"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Lewitzka, S.: $$\\epsilon _I$$: : An intuitionistic logic without Fregean Axiom and with predicates for truth and falsity. Notre Dame Journal of Formal Logic 50(3), 275\u2013301 (2009). https:\/\/doi.org\/10.1215\/00294527-2009-012","DOI":"10.1215\/00294527-2009-012"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Lewitzka, S.: $$\\epsilon _K$$: a non-Fregean logic of explicit knowledge. Studia Logica 97(2), 233\u2013264 (2011). https:\/\/doi.org\/10.1007\/s11225-011-9304-8","DOI":"10.1007\/s11225-011-9304-8"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Lewitzka, S.: Denotational semantics for modal systems S3 S5 extended by axioms for propositional quantifiers and identity. Studia Logica 103(3), 507\u2013544 (2015). https:\/\/doi.org\/10.1007\/s11225-014-9577-9","DOI":"10.1007\/s11225-014-9577-9"},{"key":"3_CR17","unstructured":"\u0141ukowski, P.: Intuitionistic sentential calculus with classical identity. Bulletin of the Section of Logic 19(4), 147\u2013150 (1990)"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Michaels, A.: A uniform proof procedure for SCI tautologies. Studia Logica 33(3), 299\u2013310 (1974). https:\/\/doi.org\/10.1007\/BF02123284","DOI":"10.1007\/BF02123284"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Or\u0142owska, E., Goli\u0144ska-Pilarek, J.: Dual Tableaux: Foundations, Methodology, Case Studies, Trends in Logic, vol. 33. Springer, Dordrecht (2011). https:\/\/doi.org\/10.1007\/978-94-007-0005-5","DOI":"10.1007\/978-94-007-0005-5"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Schmidt, R.A., Tishkovsky, D.: Automated synthesis of tableau calculi. Logical Methods in Computer Science 7(2) (2011). https:\/\/doi.org\/10.2168\/LMCS-7(2:6)2011","DOI":"10.2168\/LMCS-7(2:6)2011"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Suszko, R.: Abolition of the Fregean axiom. In: Parikh, R. (ed.) Logic Colloquium. Lecture Notes in Mathematics, vol. 453, pp. 169\u2013239 (1975). https:\/\/doi.org\/10.1007%2FBFb0064874","DOI":"10.1007\/BFb0064874"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Wasilewska, A.: A sequence formalization for SCI. Studia Logica 35(3), 213\u2013217 (1976). https:\/\/doi.org\/10.1007\/BF02282483","DOI":"10.1007\/BF02282483"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Wasilewska, A.: DFC-algorithms for Suszko logic and one-to-one Gentzen type formalizations. Studia Logica 43(4), 395\u2013404 (1984). https:\/\/doi.org\/10.1007\/BF00370509","DOI":"10.1007\/BF00370509"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:21:32Z","timestamp":1625649692000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"76","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}