Prefix Classes of Krom Formulas with Identity

  • S. O. Aandraa ,
  • E. Boerger ,
  • Yuri Gurevich

| , Vol 22: pp. 43-49

Two small classes of first order formulae without function symbols but with identity, in prenex conjunctive normal form wit hall disjunctions binary, are shown to have a recursively unsolvable decision problem, whereas for another such class an algorithm is developed which solves the decision problem of that class. This solves the prefix problem for such classes of formulae except for the Godel-Kalmar-Schutte case.