Ich bin ein bisschen verwirrt mit dem Zusammenhang von Regeltermen und die Induktion über Herleitung. Nach definition von Regeltermen darf sowohl bei der Konklusion als auch bei der Prämissen kein Metavariable auftauchen. Bei der Induktion über Herleitung dürfen die Termen Metavariablen enthalten. Ist den Zusammenhang, dass die Termen bei der Herleitung durch geeignite Substitution sich zu eine Regeltermen auswerten lassen?
vielen Dank im Voraus!
