Regelterm vs Termbeschreibung von Herleitungen

[LRS]

Guten Tag,

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!

[Markus Tasch]

Die von dir beschriebene Einschränkung auf Regelterme ohne Metavariablen gibt es nur in der Definition der Menge \(RTerme(r\text{-}name)\) (Folie 5), die alle Regelterme, die durch Instanziieren einer Regel erzeugt werden können, beinhaltet.

In der Induktion über Herleitung greifen wir aber auf die Menge von Herleitungen innerhalb eines Kalküls zurück (siehe Folie 6-8). Diese dürfen Metavariablen enthalten. Ich hoffe das klärt deine Frage.