The depthbounded approach seeks to provide realistic models of reasoners. Recognizing that most useful logics are idealizations in that they are either undecidable or likely to be intractable, the approach accounts for how they can be approximated in practice by resourcebounded agents. The approach has been applied to Classical Propositional Logic (CPL), yielding a hierarchy of tractable depthbounded approximations to that logic, which in turn has been based on a KE/KI system. This Thesis shows that the approach can be naturally extended to useful nonclassical logics such as FirstDegree Entailment (FDE), the Logic of Paradox (LP), Strong Kleene Logic (K3) and Intuitionistic Propositional Logic (IPL). To do this, we introduce a KE/KIstyle system for each of those logics such that: is formulated via signed formulae, consist of linear operational rules and branching structural rule(s), can be used as a directproof and a refutation method, and is interesting independently of the approach in that it has an exponential speedup on its tableau system counterpart. The latter given that we introduce a new class of examples which we prove to be hard for all tableau systems sharing the ∨/∧ rules with the classical one, but easy for their analogous KEstyle systems. Then we focus on showing that each of our KE/KIstyle systems naturally yields a hierarchy of tractable depthbounded approximations to the respective logic, in terms of the maximum number of allowed nested applications of the branching rule(s). The rule(s) express(es) a generalized rule of bivalence, is (are) essentially cut rule(s) and govern(s) the manipulation of virtual information, which is information that an agent does not hold but she temporarily assumes as if she held it. Intuitively, the more virtual information needs to be invoked via the branching rule(s), the harder the inference is for the agent. So, the nested application of the branching rule(s) provides a sensible measure of inferential depth. We also show that each hierarchy approximating FDE, LP, and K3, admits of a 5valued nondeterministic semantics; whereas, paving the way for a semantical characterization of the hierarchy approximating IPL, we provide a 3valued nondeterministic semantics for the full logic that fixes the meaning of the connectives without appealing to “structural” conditions. Moreover, we show a superpolynomial lower bound for the strongest possible version of clausal tableaux on the wellknown class of “truly fat” expressions (which are easy for KE), settling a problem left open in the literature. Further, we investigate a hierarchy of tractable depthbounded approximations to CPL based only on KE. Finally, we propose a refinement of the psimulation relation which is adequate to establish positive results about the superiority of a system over another with respect to proofsearch.
TRACTABLE DEPTHBOUNDED APPROXIMATIONS TO SOME PROPOSITIONAL LOGICS. TOWARDS MORE REALISTIC MODELS OF LOGICAL AGENTS / A.j. Solares Rojas ; supervisore: A. Zamansky, M. D'Agostino ; coordinatore: A. Pinotti. Dipartimento di Filosofia Piero Martinetti, 2022 Jul 15. 34. ciclo, Anno Accademico 2021.
TRACTABLE DEPTHBOUNDED APPROXIMATIONS TO SOME PROPOSITIONAL LOGICS. TOWARDS MORE REALISTIC MODELS OF LOGICAL AGENTS.
A.J. SOLARES ROJAS
2022
Abstract
The depthbounded approach seeks to provide realistic models of reasoners. Recognizing that most useful logics are idealizations in that they are either undecidable or likely to be intractable, the approach accounts for how they can be approximated in practice by resourcebounded agents. The approach has been applied to Classical Propositional Logic (CPL), yielding a hierarchy of tractable depthbounded approximations to that logic, which in turn has been based on a KE/KI system. This Thesis shows that the approach can be naturally extended to useful nonclassical logics such as FirstDegree Entailment (FDE), the Logic of Paradox (LP), Strong Kleene Logic (K3) and Intuitionistic Propositional Logic (IPL). To do this, we introduce a KE/KIstyle system for each of those logics such that: is formulated via signed formulae, consist of linear operational rules and branching structural rule(s), can be used as a directproof and a refutation method, and is interesting independently of the approach in that it has an exponential speedup on its tableau system counterpart. The latter given that we introduce a new class of examples which we prove to be hard for all tableau systems sharing the ∨/∧ rules with the classical one, but easy for their analogous KEstyle systems. Then we focus on showing that each of our KE/KIstyle systems naturally yields a hierarchy of tractable depthbounded approximations to the respective logic, in terms of the maximum number of allowed nested applications of the branching rule(s). The rule(s) express(es) a generalized rule of bivalence, is (are) essentially cut rule(s) and govern(s) the manipulation of virtual information, which is information that an agent does not hold but she temporarily assumes as if she held it. Intuitively, the more virtual information needs to be invoked via the branching rule(s), the harder the inference is for the agent. So, the nested application of the branching rule(s) provides a sensible measure of inferential depth. We also show that each hierarchy approximating FDE, LP, and K3, admits of a 5valued nondeterministic semantics; whereas, paving the way for a semantical characterization of the hierarchy approximating IPL, we provide a 3valued nondeterministic semantics for the full logic that fixes the meaning of the connectives without appealing to “structural” conditions. Moreover, we show a superpolynomial lower bound for the strongest possible version of clausal tableaux on the wellknown class of “truly fat” expressions (which are easy for KE), settling a problem left open in the literature. Further, we investigate a hierarchy of tractable depthbounded approximations to CPL based only on KE. Finally, we propose a refinement of the psimulation relation which is adequate to establish positive results about the superiority of a system over another with respect to proofsearch.File  Dimensione  Formato  

phd_unimi_R12279.pdf
accesso aperto
Tipologia:
Postprint, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
1.47 MB
Formato
Adobe PDF

1.47 MB  Adobe PDF  Visualizza/Apri 
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.