Resolution for Constrained Pseudo-Propositional Logic
Ahmad-Saher Azizi-Sultan
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.