A NEW DECIDABLE HORN FRAGMENT OF PREDICATE CALCULUS

    loading  Checking for direct PDF access through Ovid

Abstract

We describe an extension of the class ∀∃ of Horn formulas in predicate calculus. We prove the decidability of this class. We describe complexity characteristics such that fixing them splits this extended class into polynomially decidable subclasses. Fixing the maximum arity of predicates splits our class into subclasses belonging to NP. Bibliography: 11 titles.

Related Topics

    loading  Loading Related Articles