A Reduction Class Containing Formulas with one Monadic Predicate and one Binary Function Symbol

Hughes, Charles E.

J. Symbolic Logic, Tome 41 (1976) no. 1, p. 45-49 / Harvested from Project Euclid

Résumé

A new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form $\forall x\forall yC$. The matrix $C$ is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore $C$ contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.

Publié le : 1976-03-14
Classification:

@article{1183739715,
     author = {Hughes, Charles E.},
     title = {A Reduction Class Containing Formulas with one Monadic Predicate and one Binary Function Symbol},
     journal = {J. Symbolic Logic},
     volume = {41},
     number = {1},
     year = {1976},
     pages = { 45-49},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183739715}
}

Hughes, Charles E. A Reduction Class Containing Formulas with one Monadic Predicate and one Binary Function Symbol. J. Symbolic Logic, Tome 41 (1976) no. 1, pp.  45-49. http://gdmltest.u-ga.fr/item/1183739715/