O'Reilly logo

Handbook of Automated Reasoning by Andrei Voronkov, Alan J.A. Robinson

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

By Herbrand's theorem, every valid sequent containing weak quantifiers only defines a corresponding Herbrand sequent; thus, Herbrand complexity is well-defined. Still, H C si137_e can be defined in several ways—depending on our choice of a complexity measure for sequents (an alternative would be to define ‖S‖ as the number of symbol occurrences in the sequent S). As skolemization is a method of removing strong quantifiers, any sequent resulting from a valid one has a Herbrand complexity. The following theorem shows that different forms of skolemization may yield sequents with strongly different Herbrand complexity.

5.16. Theorem.

There exists ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required