Report
Tableau-based decision procedure for non-Fregean logic of sentential identity
| العنوان: | Tableau-based decision procedure for non-Fregean logic of sentential identity |
|---|---|
| المؤلفون: | Pilarek, Joanna Golińska, Huuskonen, Taneli, Zawidzki, Michał |
| سنة النشر: | 2021 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Logic in Computer Science, 03B22, 03B35 (Primary) 03B20, 03A05 (Secondary), F.4.3, I.2.3, I.2.4, D.3.1 |
| الوصف: | Sentential 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. Comment: This is a full version of a conference paper that will appear in the proceedings of the 28th International Conference on Automated Deduction (CADE) |
| نوع الوثيقة: | Working Paper |
| DOI: | 10.1007/978-3-030-79876-5_3 |
| URL الوصول: | http://arxiv.org/abs/2104.14697 |
| رقم الانضمام: | edsarx.2104.14697 |
| قاعدة البيانات: | arXiv |
| ResultId |
1 |
|---|---|
| Header |
edsarx arXiv edsarx.2104.14697 1014 3 Report report 1013.71435546875 |
| PLink |
https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&scope=site&db=edsarx&AN=edsarx.2104.14697&custid=s6537998&authtype=sso |
| FullText |
Array
(
[Availability] => 0
)
Array ( [0] => Array ( [Url] => http://arxiv.org/abs/2104.14697 [Name] => EDS - Arxiv [Category] => fullText [Text] => View record in Arxiv [MouseOverText] => View record in Arxiv ) ) |
| Items |
Array
(
[Name] => Title
[Label] => Title
[Group] => Ti
[Data] => Tableau-based decision procedure for non-Fregean logic of sentential identity
)
Array ( [Name] => Author [Label] => Authors [Group] => Au [Data] => <searchLink fieldCode="AR" term="%22Pilarek%2C+Joanna+Golińska%22">Pilarek, Joanna Golińska</searchLink><br /><searchLink fieldCode="AR" term="%22Huuskonen%2C+Taneli%22">Huuskonen, Taneli</searchLink><br /><searchLink fieldCode="AR" term="%22Zawidzki%2C+Michał%22">Zawidzki, Michał</searchLink> ) Array ( [Name] => DatePubCY [Label] => Publication Year [Group] => Date [Data] => 2021 ) Array ( [Name] => Subset [Label] => Collection [Group] => HoldingsInfo [Data] => Computer Science ) Array ( [Name] => Subject [Label] => Subject Terms [Group] => Su [Data] => <searchLink fieldCode="DE" term="%22Computer+Science+-+Logic+in+Computer+Science%22">Computer Science - Logic in Computer Science</searchLink><br /><searchLink fieldCode="DE" term="%2203B22%2C+03B35+%28Primary%29+03B20%2C+03A05+%28Secondary%29%22">03B22, 03B35 (Primary) 03B20, 03A05 (Secondary)</searchLink><br /><searchLink fieldCode="DE" term="%22F%2E4%2E3%22">F.4.3</searchLink><br /><searchLink fieldCode="DE" term="%22I%2E2%2E3%22">I.2.3</searchLink><br /><searchLink fieldCode="DE" term="%22I%2E2%2E4%22">I.2.4</searchLink><br /><searchLink fieldCode="DE" term="%22D%2E3%2E1%22">D.3.1</searchLink> ) Array ( [Name] => Abstract [Label] => Description [Group] => Ab [Data] => Sentential 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.<br />Comment: This is a full version of a conference paper that will appear in the proceedings of the 28th International Conference on Automated Deduction (CADE) ) Array ( [Name] => TypeDocument [Label] => Document Type [Group] => TypDoc [Data] => Working Paper ) Array ( [Name] => DOI [Label] => DOI [Group] => ID [Data] => 10.1007/978-3-030-79876-5_3 ) Array ( [Name] => URL [Label] => Access URL [Group] => URL [Data] => <link linkTarget="URL" linkTerm="http://arxiv.org/abs/2104.14697" linkWindow="_blank">http://arxiv.org/abs/2104.14697</link> ) Array ( [Name] => AN [Label] => Accession Number [Group] => ID [Data] => edsarx.2104.14697 ) |
| RecordInfo |
Array
(
[BibEntity] => Array
(
[Identifiers] => Array
(
[0] => Array
(
[Type] => doi
[Value] => 10.1007/978-3-030-79876-5_3
)
)
[Subjects] => Array
(
[0] => Array
(
[SubjectFull] => Computer Science - Logic in Computer Science
[Type] => general
)
[1] => Array
(
[SubjectFull] => 03B22, 03B35 (Primary) 03B20, 03A05 (Secondary)
[Type] => general
)
[2] => Array
(
[SubjectFull] => F.4.3
[Type] => general
)
[3] => Array
(
[SubjectFull] => I.2.3
[Type] => general
)
[4] => Array
(
[SubjectFull] => I.2.4
[Type] => general
)
[5] => Array
(
[SubjectFull] => D.3.1
[Type] => general
)
)
[Titles] => Array
(
[0] => Array
(
[TitleFull] => Tableau-based decision procedure for non-Fregean logic of sentential identity
[Type] => main
)
)
)
[BibRelationships] => Array
(
[HasContributorRelationships] => Array
(
[0] => Array
(
[PersonEntity] => Array
(
[Name] => Array
(
[NameFull] => Pilarek, Joanna Golińska
)
)
)
[1] => Array
(
[PersonEntity] => Array
(
[Name] => Array
(
[NameFull] => Huuskonen, Taneli
)
)
)
[2] => Array
(
[PersonEntity] => Array
(
[Name] => Array
(
[NameFull] => Zawidzki, Michał
)
)
)
)
[IsPartOfRelationships] => Array
(
[0] => Array
(
[BibEntity] => Array
(
[Dates] => Array
(
[0] => Array
(
[D] => 29
[M] => 04
[Type] => published
[Y] => 2021
)
)
)
)
)
)
)
|
| IllustrationInfo |