Abstract

The depth-bounded 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 resource-bounded agents. The approach has been applied to Classical Propositional Logic (CPL), yielding a hierarchy of tractable depth-bounded 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 First-Degree Entailment (FDE), the Logic of Paradox (LP), Strong Kleene Logic (K3 ) and Intuitionistic Propositional Logic (IPL). To do this, we introduce a KE/KI-style 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 direct-proof and a refutation method, and is interesting independently of the approach in that it has an exponential speed-up 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 V/& rules with the classical one, but easy for their analogous KE-style systems. Then we focus on showing that each of our KE/KI-style systems naturally yields a hierarchy of tractable depth-bounded 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 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 5-valued non-deterministic semantics; whereas, paving the way for a semantical characterization of the hierarchy approximating IPL, we provide a 3-valued non-deterministic semantics for the full logic that fixes the meaning of the connectives without appealing to “structural” conditions. Moreover, we show a super-polynomial lower bound for the strongest possible version of clausal tableaux on the well-known 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 depth-bounded approximations to CPL based only on KE. Finally, we propose a refinement of the p-simulation relation which is adequate to establish positive results about the superiority of a system over another with respect to proof-search.