Regelterm vs Termbeschreibung von Herleitungen

LRS
Erstie
Erstie
Beiträge: 11
Registriert: 3. Jul 2016 19:52

Regelterm vs Termbeschreibung von Herleitungen

Beitrag von LRS » 3. Mär 2017 08:26

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
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 124
Registriert: 11. Sep 2015 10:57

Re: Regelterm vs Termbeschreibung von Herleitungen

Beitrag von Markus Tasch » 3. Mär 2017 19:03

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.
Markus Tasch, M.Sc.
Modeling and Analysis of Information Systems
Department of Computer Science, TU Darmstadt
http://www.mais.informatik.tu-darmstadt.de

Antworten

Zurück zu „Archiv“