Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-I-96-2-010

Strong skolemization

Nonnengart, Andreas

MPI-I-96-2-010. December 1996, 16 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
Skolemization is a means to eliminate existential quantifiers within
predicate logic sentences and that
by replacing existentially quantified variables with Skolem function
applications.
The arguments of these Skolem functions are variables which are
quantified outside the sub-formula under consideration.
In this paper a Skolemization technique is introduced which abstracts
from some of the arguments of the Skolem functions.
It shows that the Skolemization result obtained this way is usually
more general than what can be achieved from standard (classical)
Skolemization.
This can be of quite some importance since such generalizations often
lead to a reduction of both search space and proof length.
Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-96-2-010.ps242 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1996-2-010
Hide details for BibTeXBibTeX
@TECHREPORT{Nonnengart96b,
  AUTHOR = {Nonnengart, Andreas},
  TITLE = {Strong skolemization},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-96-2-010},
  MONTH = {December},
  YEAR = {1996},
  ISSN = {0946-011X},
}