Journal Article
No Thumbnail Available
License

CC-BYCC-BY - Attribution

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

Author
Golińska-Pilarek, Joanna
Huuskonen, Taneli
Zawidzki, Michał
Publication date
2021
Abstract (EN)

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.

Keywords EN
Sentential Calculus with Identity
non-Fregean logics
labelled tableaux
decision procedure
termination
computational complexity
PBN discipline
philosophy
Pages from-to
41-57
Date release in open access
2021-07-05
Open access license
Attribution