Extension Rule for Non-Clausal Propositional Calculus

Article type: Research Article

Authors: Majorinc, Kazimir

Affiliations: Faculty of Natural Sciences and Mathematics, University of Zagreb, Zagreb, Croatia. [email protected]

Abstract: Van Gelder has described a few reasons for satisfiability testing without transformation of formulas into CNF and has developed an algorithm for this problem. We have introduced two possible improvements. First, we have used directed acyclic graphs for the representation of formula, instead of representation in the form of a tree or a string of characters. Second, we have allowed a limited introduction of new variables, again without transformation to CNF. In terms of a proof system, Van Gelder’s algorithm does not p-simulate system described here. Some generalizations of notions of propositional formula, satisfiability, etc. are introduced.

Keywords: non-clausal propositional satisfiability, Van Gelder's algorithm, splitting rule

DOI: 10.3233/FI-1997-31201

Journal: Fundamenta Informaticae, vol. 31, no. 2, pp. 107-116, 1997