Alejandro Solares-Rojas

We present the first implementation of the labeled KE-tableau system for Intuitionistic Propositional Logic recently introduced in (Solares-Rojas, Baldi and Rodriguez, 2026), considering the formulation that uses only constant labels. This implementation extends an existing prover for classical KE with a "canonical" decision procedure executing the intuitionistic version. Particularly, we identify and motivate three operational design decisions that the theoretical presentation in (Solares-Rojas, Baldi and Rodriguez, 2026) does not detail for an implementation: (i) how the branch-completion condition is evaluated, which in turn determines when a branch of the derivation tree yields a counter-model of the input; (ii) the point at which the branching rule is applied, for which we provide two alternative implementations and compare them; and (iii) how instance-identity is encoded, so that reapplying a rule at a newly available label is not mistaken for the repetition that the procedure forbids. Finally, we evaluate on the complete propositional part of the ILTP library (274 problems), on which the prover agrees with the declared status on every problem it decides.

El sistema de demostración KE es una variante de los tableaux analíticos pero es computacionalmente más eficiente que estos. Este sistema fue extendido a la lógica intuicionista proposicional recientemente. Además de su eficiencia y a diferencia de los resolvedores SAT, el sistema KE intuicionista no requiere transformaciones a formas normales y es modular en tanto que se puede extender, simple y naturalmente, a una familia amplia de lógicas que admiten semánticas relacionales. En este trabajo exploramos parte de esta modularidad, extendiendo KE a una familia de lógicas modales intuicionistas, las cuales tienen aplicaciones relevantes en razonamiento automatizado y verificación formal.

The tableau-like system KE is generalized to intuitionistic propositional logic by means of labeled signed formulas and constraints between labels, mimicking the relational semantics. To improve on proof-search and exploiting the meaning of negation, we further endow the system with free-variables. The resulting system enjoys the subformula property and terminates, either with a proof or a finite countermodel, without any extra mechanism. Proof and countermodel search is guided by generalizations of traditional reasoning patterns.

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.

FDE, LP and K3 are closely related to each other and admit of an intuitive informational interpretation. However, all these logics are co-NP complete, and so idealized models of how an agent can think. We address this issue by shifting to signed formulae, where the signs express imprecise values associated with two bipartitions of the corresponding set of standard values. We present proof systems whose operational rules are all linear and have only two structural branching rules that express a generalized Principle of Bivalence. Each of these systems leads to defining an infinite hierarchy of tractable approximations to the respective logic, in terms of the maximum number of allowed nested applications of the two branching rules. Further, each resulting hierarchy admits of an intuitive 5-valued non-deterministic semantics.

FDE is a logic that captures relevant entailment between implication-free formulae and admits of an intuitive informational interpretation as a 4-valued logic in which “a computer should think”. However, the logic is co-NP complete, and so an idealized model of how an agent can think. We address this issue by shifting to signed formulae where the signs express imprecise values associated with two distinct bipartitions of the set of standard 4 values. Thus, we present a proof system which consists of linear operational rules and only two branching structural rules, the latter expressing a generalized rule of bivalence. This system naturally leads to defining an infinite hierarchy of tractable depth-bounded approximations to FDE. Namely, approximations in which the number of nested applications of the two branching rules is bounded.