next up previous contents
Nächste Seite: GOLOG Aufwärts: Das Situationskalkül Vorherige Seite: Eine Lösung des Rahmenproblems   Inhalt


Fundamentale Axiome

  1. \( \forall P.P(S_{o})\wedge [\forall s\forall a.(P(s)\supset P(do(a,s)))]\supset \forall s.P(s); \)
  2. \( do(a,s)=do(a',s')\supset a=a' \) \( \wedge s=s' \)
  3. \( \neg (s\sqsubset S_{o}) \)
  4. \( s\sqsubset do(a,s')\equiv s\sqsubseteq s' \), mit \( s\sqsubseteq s' \) steht für \( (s\sqsubset s')\vee (s=s') \)
  5. \( s\prec s'\equiv s\sqsubset s'\wedge \forall a,s^{*}.s\sqsubset do(a,s^{*})\sqsubseteq s'\supset Poss(a,s^{*}) \)
Die erste Aussage ist ein induktives Axiom zweiter Ordnung, das nur solche Situationen zuläßt, die durch Anwendung von \( do \) Termen aus \( S_{0} \) entstehen können. Es wird also eine Baumstruktur mit den Situationen \( s_{i} \) als Knoten und den Aktionen \( a_{j} \) als Übergänge definiert. Das zweite Axiom sichert die Eindeutigkeit des Übergangs von \( s_{i} \) nach \( s_{i+1} \) durch die Aktion \( a \). \( \sqsubseteq \) definiert eine geordnete Relation über Situationen. Das dritte Axiom beschreibt also, daß es keine Vorgängersituation vor der Situation \( S_{0} \) gibt. \( s\sqsubseteq s' \) ist erfüllt, wenn \( s' \) aus \( s \) durch eine endliche Anzahl von Aktionen erreicht werden kann. Zum Schluß gilt \( s\prec s' \), wenn eine legale Sequenz (\( executable(s) \)) von Aktionen existiert, die von \( s \) nach \( s' \) führt.



2001-01-04