Resolution for Constrained Pseudo-Propositional Logic
This work provides a theoretical extension for logic systems, but it is incremental as it builds on existing propositional logic foundations.
The paper tackles the problem of extending propositional resolution to constrained pseudo-propositional logic (CPPL), which allows infinite sets of clauses, and shows that the generalized resolution system is sound and complete, implying that propositional resolution remains sound and complete even for formulas with infinite clause sets.
This work, shows how propositional resolution can be generalized to obtain a resolution proof system for constrained pseudo-propositional logic (CPPL), which is an extension resulted from inserting the natural numbers with few constraints symbols into the alphabet of propositional logic and adjusting the underling language accordingly. Unlike the construction of CNF formulas which are restricted to a finite set of clauses, the extended CPPL does not require the corresponding set to be finite. Although this restriction is made dispensable, this work presents a constructive proof showing that the generalized resolution for CPPL is sound and complete. As a marginal result, this implies that propositional resolution is also sound and complete for formulas with even infinite set of clauses.