Übung 4

himbaer
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 28. Apr 2010 19:29
Kontaktdaten:

Übung 4

Beitrag von himbaer »

Ich habe mal eine Frage zum 4. Übungsblatt:
Bei der Aufgabe Problem 1 FOL Calculus die c) frage ich mich, warum es nach einer impR anwendung nicht möglich ist ExR anzuwenden? Wieso kann ich im Key System nun nicht das x substituieren?

Ich bekomme bei dem Versuch dann immer folgende Fehlermeldung:

Code: Alles auswählen

(program) variable or constant
	x_0
not declared 
Könnte mir jemand Erklären, warum das hier nicht möglich ist?

Dieses Problem tritt auch bei der Aufgabe e) auf. Hier würde ich jetzt eigentlich zuerst gerne den Existenzquantor rechts substituieren. Aber auch das ist im Key System nicht möglich????
meine Testsignatur :!:

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Übung 4

Beitrag von Nathan Wasser »

Du benötigst einen Term vom richtigen Typ. Es gibt aber nicht notwendigerweise einen solchen Term. Deshalb muss bei diesen Aufgaben eine Konstante in die Aufgabenstellung definiert werden.

himbaer
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 28. Apr 2010 19:29
Kontaktdaten:

Re: Übung 4

Beitrag von himbaer »

Wie definiere ich so eine Konstante?
meine Testsignatur :!:

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Übung 4

Beitrag von Nathan Wasser »

Das steht in der Lösung auf der Webseite. Eine Konstante wird als Funktion ohne Argumente definiert.

Antworten

Zurück zu „Archiv“