Skolemform ist ein Begriff der Prädikatenlogik und bezeichnet eine prädikatenlogische Formel, die sich in einer Normalform nach Albert Thoralf Skolem befindet. Algorithmen zur Prüfung der Erfüllbarkeit nutzen oft die Skolemform. Dies ist nützlich, da jede Formelmenge X genau dann erfüllbar ist, wenn ihre Skolemform erfüllbar ist. Des Weiteren ist die Skolemform ein hilfreicher Zwischenschritt, wenn man eine Formel in Klausel-Normalform umformen will. Sie wird auch als Zwischenergebnis benötigt, wenn man ein Herbrand-Universum erzeugen will. In der Skolemform sind keine Existenzquantoren (

Property Value
dbo:abstract
  • Skolemform ist ein Begriff der Prädikatenlogik und bezeichnet eine prädikatenlogische Formel, die sich in einer Normalform nach Albert Thoralf Skolem befindet. Algorithmen zur Prüfung der Erfüllbarkeit nutzen oft die Skolemform. Dies ist nützlich, da jede Formelmenge X genau dann erfüllbar ist, wenn ihre Skolemform erfüllbar ist. Des Weiteren ist die Skolemform ein hilfreicher Zwischenschritt, wenn man eine Formel in Klausel-Normalform umformen will. Sie wird auch als Zwischenergebnis benötigt, wenn man ein Herbrand-Universum erzeugen will. In der Skolemform sind keine Existenzquantoren () mehr enthalten. Variablen, die an Existenzquantoren gebunden waren, werden durch neue Funktionssymbole ersetzt. Als Argumente bekommen die neuen Funktionssymbole die Variablen der Allquantoren (), die vor dem entfernten Existenzquantor standen. (de)
  • Skolemform ist ein Begriff der Prädikatenlogik und bezeichnet eine prädikatenlogische Formel, die sich in einer Normalform nach Albert Thoralf Skolem befindet. Algorithmen zur Prüfung der Erfüllbarkeit nutzen oft die Skolemform. Dies ist nützlich, da jede Formelmenge X genau dann erfüllbar ist, wenn ihre Skolemform erfüllbar ist. Des Weiteren ist die Skolemform ein hilfreicher Zwischenschritt, wenn man eine Formel in Klausel-Normalform umformen will. Sie wird auch als Zwischenergebnis benötigt, wenn man ein Herbrand-Universum erzeugen will. In der Skolemform sind keine Existenzquantoren () mehr enthalten. Variablen, die an Existenzquantoren gebunden waren, werden durch neue Funktionssymbole ersetzt. Als Argumente bekommen die neuen Funktionssymbole die Variablen der Allquantoren (), die vor dem entfernten Existenzquantor standen. (de)
dbo:wikiPageID
  • 252407 (xsd:integer)
dbo:wikiPageRevisionID
  • 153550208 (xsd:integer)
dct:subject
rdfs:comment
  • Skolemform ist ein Begriff der Prädikatenlogik und bezeichnet eine prädikatenlogische Formel, die sich in einer Normalform nach Albert Thoralf Skolem befindet. Algorithmen zur Prüfung der Erfüllbarkeit nutzen oft die Skolemform. Dies ist nützlich, da jede Formelmenge X genau dann erfüllbar ist, wenn ihre Skolemform erfüllbar ist. Des Weiteren ist die Skolemform ein hilfreicher Zwischenschritt, wenn man eine Formel in Klausel-Normalform umformen will. Sie wird auch als Zwischenergebnis benötigt, wenn man ein Herbrand-Universum erzeugen will. In der Skolemform sind keine Existenzquantoren ( (de)
  • Skolemform ist ein Begriff der Prädikatenlogik und bezeichnet eine prädikatenlogische Formel, die sich in einer Normalform nach Albert Thoralf Skolem befindet. Algorithmen zur Prüfung der Erfüllbarkeit nutzen oft die Skolemform. Dies ist nützlich, da jede Formelmenge X genau dann erfüllbar ist, wenn ihre Skolemform erfüllbar ist. Des Weiteren ist die Skolemform ein hilfreicher Zwischenschritt, wenn man eine Formel in Klausel-Normalform umformen will. Sie wird auch als Zwischenergebnis benötigt, wenn man ein Herbrand-Universum erzeugen will. In der Skolemform sind keine Existenzquantoren ( (de)
rdfs:label
  • Skolemform (de)
  • Skolemform (de)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageRedirects of
is foaf:primaryTopic of