„Sortenlogik“ – Versionsunterschied

Versionsgeschichte interaktiv durchsuchen

[gesichtete Version]

← Zum vorherigen Versionsunterschied Zum nächsten Versionsunterschied →

Inhalt gelöscht Inhalt hinzugefügt

Inline

Version vom 8. März 2018, 21:21 Uhr

Sortenlogik entspringt der Intention, das (mengentheoretische) Universum (Grundmenge, Allklasse, bis hin zu einem Grothendieck-Universum) nicht als eine homogee Ansammlung von (mathematischen) Objekten^[1] zu betrachten, sondern diese auf verschiedene Klassen oder Typen aufzuteilen, die in diesem Zusammenhang Sorten genannt werden (ähnlich wie die Datentypen in vielen Programmiersprachen und Datenbanksystemen). Jedem Term einer logischen Formel^[2] wird eine Sorte zugeordnet. Unifikation von Termen ist nur dann zugelassen, wenn beide Terme von der gleichen Sorte sind; Substitution^[3] und Argumentübergabe^[4] können ebenfalls nur unter Berücksichtigung diese Sorten erfolgen. Falsche Sortenzuordnungen werden also bereits als Syntaxfehler ausgewiesen.

Es gibt prinzipiell verschiedene Möglichkeiten, diese Absicht zu realisieren. Den meisten Fällen gemeinsam ist

es gibt eine Menge von Sorten, $S$ ^[5]
es gibt eine Verallgemeinerung des Begriffs Signatur, um die mit den Sorten verbundene Zusatzinformation handzuhaben.

Im gesamten Universum als Zusammenfassung aller Objekte iner Struktur werden dann in die Wertebereiche zu den verschiedenen Sorten abgegrenzt.

Aus dem Blickwinkel der Prädikatenlogik (ohne Sorten) sind solche Sorten einstellige Prädikate, falsche Sortenzuweisungen erscheinendann nicht als Syntaxfehler, sondern nach Zuweisung einer Semantik als falsch. Die Sortenlogik stellt dagegen für diese Prädikate eine Spezialbehandlung der eben erwähnten Form zur Verfügung. Da viele Deduktionschritte hierbei wegen der Sortenunverträglichkeit nicht in Betracht gezogen werden brauchen, verringert sich der Suchaufwand nach einem Beweis in der Praxis beträchtlich.

Beispiel

Ein Beispiel bieten Taxons (Gruppen) biologischer Organismen, unter anderem ${\textit {Pflanze}}$ und ${\textit {Tier}}$ . Während eine Funktion ${\textit {Mutter}}:{\textit {Tier}}\longrightarrow {\textit {Tier}}$ sinnvoll ist, würde das für eine ähnliche Funktion ${\textit {Mutter}}:{\textit {Pflanze}}\longrightarrow {\textit {Pflanze}}$ im Allgemeinen nicht gelten. Sortenlogik erlaubt Terme der Art ${\textit {Mutter}}($ ${\textit {Rex}}$ $)$ , verwirft aber ${\textit {Mutter}}($ ${\textit {Schaeferbuche}}$ $)$ als syntakische Fehlkonstruktion.

Formale Definition

Die formale Definition der Sortenlogik wird in einem Artikel von Caleiro und Gonçalves^[6] als Verallgemeinerung der Prädikatenlogik auf den vielsortigen Fall beschrieben, und kann gut als ein Einstieg in die Materie dienen.

Ordnungssortierte Logik

Während in der viesortigen Logik die paarweise Disjunktheit der Werteberiche zu den verschiedenenSorten vorausgesetzt wird, erlaubt die ordnungssortierte Logik (englisch: Order Sorted Logic), dass eine Sorte $s_{1}$ als eine Untersorte einer anderen Sorte $s_{2}$ erklärt wird, in Zeichen $s_{1}\subseteq s_{2}$ , $s_{1}\preceq s_{2}$ oder ähnlich. Im obigen Beispiel wäre etwa

{\textit {Hund}}\ \preceq \ {\textit {Fleischfresser}}

,

{\textit {Hund}}\ \preceq \ {\textit {Wirbeltier}}

,

{\textit {Raubtier}}\ \preceq \ {\textit {Tier}}

,

{\textit {Wirbeltier}}\ \preceq \ {\textit {Tier}}

,

{\textit {Tier}}\ \preceq \ {\textit {Organismus}}

,

{\textit {Buche}}\ \preceq \ {\textit {Pflanze}}

,

{\textit {Pflanze}}\ \preceq \ {\textit {Organismus}}

,

und so weiter.

Einzelnachweise und Anmerkungen

↑ Siehe auch Objekt in der Programmierung
↑ Siehe auch mathematische Formel
↑ Siehe auch Substitution in der Mathematik
↑ Siehe auch Argumente in de Informatik, Argumente in der Programmierung
↑ $S$ wird gedeutet als ein Alphabet von Sortenbezeichnern, siehe Alphabet (Informatik) und Alphabet (Mathematik)
↑ Carlos Caleiro, Ricardo Gonçalves: Proc. 18th int. conf. on Recent trends in algebraic development techniques (WADT). Springer, 2006, ISBN 978-3-540-71997-7, On the algebraization of many-sorted logics, S. 21–36 (utl.pt [PDF]).

Literatur

Wolfgang Bibel, Steffen Hölldobler, Torsten Schaub: Wissensrepräsentation und Inferenz. Eine grundlegende Einführung. Springer-Verlag, 2013, ISBN 3-322-86814-1, S. 99–100 (Google Books [abgerufen am 17. April 2016]).
A. Oberschelp: Untersuchungen zur mehrsortigen Quantorenlogik, Nummer 4. In: Mathematische Annalen. 145. Jahrgang, 1962, S. 297–333, doi:10.1007/bf01396685 (uni-goettingen.de).
Wang, Hao: Logic of many-sorted theories. In: Journal of Symbolic Logic. 17. Jahrgang, 1952, S. 105–116, doi:10.2307/2266241. , collected in the author's Computation, Logic, Philosophy. A Collection of Essays, Beijing: Science Press; Dordrecht: Kluwer Academic, 1990.
Gilmore, P.C.: An addition to "Logic of many-sorted theories". In: Compositio Mathematica. 13. Jahrgang, 1958, S. 277–281 (numdam.org [PDF]).
F. Jeffry Pelletier: Sortal Quantification and Restricted Quantification. In: Philosophical Studies. 23. Jahrgang, 1972, S. 400–404, doi:10.1007/bf00355532 (sfu.ca [PDF]).

Siehe auch

[1] Siehe auch Objekt in der Programmierung

[2] Siehe auch mathematische Formel

[3] Siehe auch Substitution in der Mathematik

[4] Siehe auch Argumente in de Informatik, Argumente in der Programmierung

[5] $S$ wird gedeutet als ein Alphabet von Sortenbezeichnern, siehe Alphabet (Informatik) und Alphabet (Mathematik)

[6] Carlos Caleiro, Ricardo Gonçalves: Proc. 18th int. conf. on Recent trends in algebraic development techniques (WADT). Springer, 2006, ISBN 978-3-540-71997-7, On the algebraization of many-sorted logics, S. 21–36 (utl.pt [PDF]).

[1]

[2]

[3]

[4]

[5]

[6]

@@ Zeile 1: / Zeile 1: @@
+'''Sortenlogik''' entspringt der Intention, das (mengentheoretische) Universum ([[Grundmenge]], [[Allklasse]], bis hin zu einem [[Grothendieck-Universum]]) nicht als eine homogee Ansammlung von [[Objekt (Philosophie)|(mathematischen) Objekten]]<ref>Siehe auch [[Objekt (Programmierung)|Objekt]] in der Programmierung</ref> zu betrachten, sondern diese auf verschiedene Klassen oder Typen aufzuteilen, die in diesem Zusammenhang ''Sorten'' genannt werden (ähnlich wie die [[Datentyp]]en in vielen [[Programmiersprachen]] und [[Datenbank|Datenbanksystemen]]).  Jedem [[Term]] einer [[logische Formel|logischen Formel]]<ref>Siehe auch [[mathematische Formel]]</ref> wird eine Sorte zugeordnet. [[Unifikation (Logik)|Unifikation]] von Termen ist nur dann zugelassen, wenn beide Terme von der gleichen Sorte sind; [[Substitution (Logik)|Substitution]]<ref>Siehe auch [[Substitution (Mathematik)|Substitution]] in der Mathematik</ref> und [[Funktion (Mathematik)#Sprechweisen|Argumentübergabe]]<ref>Siehe auch [[Parameter_(Informatik)#Argumente|Argumente]] in de Informatik, [[Funktion_(Programmierung)#Funktionale_Programmierung|Argumente]] in der Programmierung</ref> können ebenfalls nur unter Berücksichtigung diese Sorten erfolgen. Falsche Sortenzuordnungen werden also bereits als [[Syntaxfehler]] ausgewiesen.
-'''Sortenlogik''' ordnet jedem [[Term]] in einer Formel eine Klasse zu, die man in diesem Zusammenhang ''Sorte'' nennt, und die [[Unifikation (Logik)|Unifikation]] nur dann zulässt, wenn beide Terme von der gleichen Sorte sind.
+Es gibt prinzipiell verschiedene Möglichkeiten, diese Absicht zu realisieren. Den meisten Fällen gemeinsam ist
-Aus dem Blickwinkel der [[Prädikatenlogik]] (ohne Sorten) sind solche Sorten einstellige Prädikate. Die Sortenlogik stellt für diese [[Prädikat (Logik)|Prädikate]] eine Spezialbehandlung der eben erwähnten Form zur Verfügung. Da viele [[Deduktion]]schritte hierbei wegen der Sortenunverträglichkeit nicht in Betracht gezogen werden, verringert sich der Suchaufwand nach einem Beweis beträchtlich, wie die Praxis zeigt.
+* es gibt eine Menge von Sorten, <math>S</math><ref><math>S</math> wird gedeutet als ein Alphabet von Sortenbezeichnern, siehe [[Alphabet (Informatik)]] und [[Alphabet (Mathematik)]]</ref>
+* es gibt eine Verallgemeinerung des Begriffs [[Signatur (Modelltheorie)|Signatur]], um die mit den Sorten verbundene Zusatzinformation handzuhaben.
+Im gesamten Universum als Zusammenfassung aller Objekte iner Struktur werden dann in die Wertebereiche zu den verschiedenen Sorten abgegrenzt.
+Aus dem Blickwinkel der [[Prädikatenlogik]] (ohne Sorten) sind solche Sorten einstellige Prädikate, falsche Sortenzuweisungen erscheinendann nicht als Syntaxfehler, sondern nach Zuweisung einer [[Semantik#Semantik formaler Sprachen|Semantik]] als falsch. Die Sortenlogik stellt dagegen für diese [[Prädikat (Logik)|Prädikate]] eine Spezialbehandlung der eben erwähnten Form zur Verfügung. Da viele [[Deduktion]]schritte hierbei wegen der Sortenunverträglichkeit nicht in Betracht gezogen werden brauchen, verringert sich der Suchaufwand nach einem [[Beweis (Logik)|Beweis]] in der Praxis beträchtlich.
-== Siehe auch ==
-* [[Signatur (Modelltheorie)#Vielsortige Signaturen|Signatur in der Modelltheorie: Vielsortige Signaturen]]
+== Beispiel ==
-* [[Term#Terme in vielsortiger Logik|Terme in vielsortiger Logik]] und [[Term#Ausdrücke in der vielsortigen Logik|Ausdrücke in vielsortiger Logik]]
+Ein Beispiel bieten [[Taxon]]s (Gruppen) biologischer [[Organismus|Organismen]], unter anderem <math>\textit{Pflanze}</math> und <math>\textit{Tier}</math>. Während eine Funktion <math>\textit{Mutter}: \textit{Tier} \longrightarrow \textit{Tier}</math> sinnvoll ist, würde das für eine ähnliche Funktion <math>\textit{Mutter}: \textit{Pflanze} \longrightarrow \textit{Pflanze}</math> im Allgemeinen nicht gelten. Sortenlogik erlaubt Terme der Art {{nowrap|<math>\textit{Mutter}(</math>[[Kommissar Rex|<math>\textit{Rex}</math>]]<math>)</math>}}, verwirft aber {{nowrap|<math>\textit{Mutter}(</math>[[Schäferbuche|<math>\textit{Schaeferbuche}</math>]]<math>)</math>}} als syntakische Fehlkonstruktion.
+== Formale Definition ==
+Die formale Definition der Sortenlogik wird in einem Artikel von Caleiro und Gonçalves<ref>{{cite book| author=Carlos Caleiro, Ricardo Gonçalves| chapter=On the algebraization of many-sorted logics| title=Proc. 18th int. conf. on Recent trends in algebraic development techniques (WADT)| year=2006| volume=| pages=21–36| publisher=Springer| editor=| series=| isbn=978-3-540-71997-7| url=http://sqig.math.ist.utl.pt/pub/CaleiroC/06-CG-manysorted.pdf}}</ref> als Verallgemeinerung der Prädikatenlogik auf den vielsortigen Fall beschrieben, und kann gut als ein Einstieg in die Materie dienen.
+== Ordnungssortierte Logik ==
+Während in der ''viesortigen Logik'' die paarweise [[Disjunkt]]heit der Werteberiche zu den verschiedenenSorten vorausgesetzt wird, erlaubt die ''[[ordnungssortierte Logik]]''<!-- Zur Übersetzung des Begriffs siehe [https://www.fernuni-hagen.de/ps/team/friedrich.steimann.shtml] und Martin Rörig unter [https://www.fdsi.org/index.php?id=27] --> (englisch: [[:en:Order Sorted Logic|Order Sorted Logic]]), dass eine Sorte <math>s_1</math> als eine Untersorte einer anderen Sorte <math>s_2</math> erklärt wird, in Zeichen <math>s_1 \sube s_2</math>, &nbsp;<math>s_1 \preceq s_2</math> oder ähnlich. Im obigen Beispiel wäre etwa
+:<math>\textit{Hund}\ \preceq\ \textit{Fleischfresser}</math>,
+:<math>\textit{Hund}\ \preceq\ \textit{Wirbeltier}</math>,
+:<math>\textit{Raubtier}\ \preceq\ \textit{Tier}</math>,
+:<math>\textit{Wirbeltier}\ \preceq\ \textit{Tier}</math>,
+:<math>\textit{Tier}\ \preceq\ \textit{Organismus}</math>,
+:<math>\textit{Buche}\ \preceq\ \textit{Pflanze}</math>,
+:<math>\textit{Pflanze}\ \preceq\ \textit{Organismus}</math>,
+und so weiter.
+== Einzelnachweise und Anmerkungen ==
+<references />
 == Literatur ==
 * {{Literatur|Autor=Wolfgang Bibel, Steffen Hölldobler, Torsten Schaub|Verlag=Springer-Verlag|Titel=Wissensrepräsentation und Inferenz|TitelErg=Eine grundlegende Einführung|Jahr=2013|ISBN=3-3228681-4-1|Seiten=99–100|Online=[https://books.google.de/books?id=VcCbBgAAQBAJ&pg=PA99 Google Books]|Zugriff=2016-04-17}}
+* {{cite journal| author=A. Oberschelp| title=Untersuchungen zur mehrsortigen Quantorenlogik, Nummer 4| journal=Mathematische Annalen| year=1962| volume=145| pages=297–333| url=http://gdz.sub.uni-goettingen.de/index.php?id=11&L=4&PPN=GDZPPN002289989&L=1| doi=10.1007/bf01396685}}
+* {{cite journal| author=Wang, Hao| title=Logic of many-sorted theories| journal=Journal of Symbolic Logic| year=1952| volume=17| pages=105–116| doi=10.2307/2266241}}, collected in the author's ''Computation, Logic, Philosophy. A Collection of Essays'', Beijing: Science Press; Dordrecht: Kluwer Academic, 1990.
+* {{cite journal| author=Gilmore, P.C.| title=An addition to "Logic of many-sorted theories"| journal=Compositio Mathematica| year=1958| volume=13| pages=277–281| url=http://archive.numdam.org/article/CM_1956-1958__13__277_0.pdf}}
+* {{cite journal| author=F. Jeffry Pelletier| title=Sortal Quantification and Restricted Quantification| journal=Philosophical Studies| year=1972| volume=23| pages=400–404| url=https://www.sfu.ca/~jeffpell/papers/SortalRestrQuant.pdf| doi=10.1007/bf00355532}}
+== Siehe auch ==
+* [[Signatur (Modelltheorie)#Vielsortige Signaturen|Signatur in der Modelltheorie: Vielsortige Signaturen]]
+* [[Term#Terme in vielsortiger Logik|Terme in vielsortiger Logik]] und [[Term#Ausdrücke in der vielsortigen Logik|Ausdrücke in vielsortiger Logik]]
 [[Kategorie:Logik]]

„Sortenlogik“ – Versionsunterschied

Version vom 8. März 2018, 21:21 Uhr

Inhaltsverzeichnis

Beispiel

Formale Definition

Ordnungssortierte Logik

Einzelnachweise und Anmerkungen

Literatur

Siehe auch

Navigationsmenü

„Sortenlogik“ – Versionsunterschied

Version vom 8. März 2018, 21:21 Uhr

Beispiel

Formale Definition

Ordnungssortierte Logik

Einzelnachweise und Anmerkungen

Literatur

Siehe auch

Navigationsmenü

Suche