  Prolog is a well known declarative programming language based on
propositional Horn formulas. It is useful in various areas, including
artificial intelligence, automated theorem proving, mathematical logic and so
on. An active research area for many years is to extend Prolog to larger
classes of logic. Some important extensions of it includes the constraint logic
programming, and the object oriented logic programming. However, it cannot
solve problems having arbitrary quantified Horn formulas.
  To be precise, the facts, rules and queries in Prolog are not allowed to have
arbitrary quantified variables. The paper overcomes this major limitations of
Prolog by extending it for the quantified Boolean Horn formulas. We achieved
this by extending the SLD-resolution proof system for quantified Boolean Horn
formulas, followed by proposing an efficient model for implementation. The
paper shows that the proposed implementation also supports the first-order
predicate Horn logic with arbitrary quantified variables.
  The paper also introduces for the first time, a declarative programming for
the quantified Boolean Horn formulas.
