de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

Strong skolemization

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45132

Nonnengart,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)

1996-2-010
(beliebiger Volltext), 10KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Nonnengart, A.(1996). Strong skolemization (MPI-I-1996-2-010). Saarbrücken: Max-Planck-Institut für Informatik.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-9FD9-6
Zusammenfassung
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.