Hi, Ich versteh nicht ganz wie bei einer Ableitung in einem Kalkül die Folge F_1 bis F_n zustande kommt. Also F_n ist die Formel die man aus dem Kalkül ableiten will aber wie kommen die anderen zustande und deren Reihenfolge? Find da im Script nichts zu.
Die Definition ist auf Folie 6.17.
http://www.informatik.uni-hamburg.de/WSV/teaching/FGI1/universitaet/FGI1_06_logik.pdf

mfg

Eine Ableitung in einem Kalkül (= Sprache + Axiome + Inferenzregeln) aus einer Formelmenge M ist eine Folge von Formeln.
Jede Formel muss dabei entweder[*]direkt aus M übernommen sein
[*]durch eine beliebige Substitution der Symbole in einem der Axiome entstanden sein (wirklich beliebig - denk Dir irgendwas aus, was Du für A und B und so einsetzen willst, das muss nicht mal in der Zielformel drin vorkommen oder so)
[*]mit einer Inferenzregel aus bisher in der Ableitung stehenden Formeln abgeleitet worden seinDie Reihenfolge der Formeln in der Ableitung ist also nicht 100%ig festgelegt, nur dass bei Anwendung einer Inferenzregel alle benötigten Formeln bereits aufgeführt sein müssen.
Das Geheimnis ist jetzt, wie man sich die Formeln in der Ableitung so hinbastelt, dass man eine bestimmte Zielformel hinbekommt. Da braucht man wahrscheinlich Erfahrung und Intuition. Das lässt sich im Script nicht so vermitteln, leider.