ARRUDA, Alexandre Matos. Um sistema infinitário para a lógica de menor ponto fixo. 2007. 91 f. : Dissertação (mestrado) - Universidade Federal do Ceará, Departamento de Computação, Fortaleza-CE, 2007. / Submitted by guaracy araujo (guaraa3355@gmail.com) on 2016-05-20T15:28:27Z No. of bitstreams: 1 2007_dis_amarruda.pdf: 427889 bytes, checksum: b0a54f14f17ff89b515a4101e02f5b58 (MD5) / Approved for entry into archive by guaracy araujo (guaraa3355@gmail.com) on 2016-05-20T15:29:23Z (GMT) No. of bitstreams: 1 2007_dis_amarruda.pdf: 427889 bytes, checksum: b0a54f14f17ff89b515a4101e02f5b58 (MD5) / Made available in DSpace on 2016-05-20T15:29:23Z (GMT). No. of bitstreams: 1 2007_dis_amarruda.pdf: 427889 bytes, checksum: b0a54f14f17ff89b515a4101e02f5b58 (MD5) Previous issue date: 2007 / The notion of the least fixed-point of an operator is widely applied in computer science as, for instance, in the context of query languages for relational databases. Some extensions of FOL with _xed-point operators on finite structures, as the least fixed-point logic (LFP), were proposed to deal with problem problems related to the expressivity of FOL. LFP captures the complexity class PTIME over the class of _nite ordered structures. The descriptive characterization of computational classes is a central issue within _nite model theory (FMT). Trakhtenbrot's theorem, considered the starting point of FMT, states that validity over finite models is not recursively enumerable, that is, completeness fails over finite models. This result is based on an underlying assumption that any deductive system is of finite nature. However, we can relax such assumption as done in the scope of proof theory for arithmetic. Proof theory has roots in the Hilbert's programme. Proof theoretical consequences are, for instance, related to normalization theorems, consistency, decidability, and complexity results. The proof theory for arithmetic is also motivated by Godel incompleteness theorems. It aims to o_er an example of a true mathematically meaningful principle not derivable in first-order arithmetic. One way of presenting this proof is based on a definition of a proof system with an infinitary rule, the w-rule, that establishes the consistency of first-order arithmetic through a proof-theoretical perspective. Motivated by this proof, here we will propose an in_nitary proof system for LFP that will allow us to investigate proof theoretical properties. With such in_nitary deductive system, we aim to present a proof theory for a logic traditionally defined within the scope of FMT. It opens up an alternative way of proving results already obtained within FMT and also new results through a proof theoretical perspective. Moreover, we will propose a normalization procedure with some restrictions on the rules, such this deductive system can be used in a theorem prover to compute queries on relational databases. / A noção de menor ponto-fixo de um operador é amplamente aplicada na ciência da computação como, por exemplo, no contexto das linguagens de consulta para bancos de dados relacionais. Algumas extensões da Lógica de Primeira-Ordem (FOL)1 com operadores de ponto-fixo em estruturas finitas, como a lógica de menor ponto-fixo (LFP)2, foram propostas para lidar com problemas relacionados á expressividade de FOL. A LFP captura as classes de complexidade PTIME sobre a classe das estruturas finitas ordenadas. A caracterização descritiva de classes computacionais é uma abordagem central em Teoria do Modelos Finitos (FMT)3. O teorema de Trakhtenbrot, considerado o ponto de partida para FMT, estabelece que a validade sobre modelos finitos não é recursivamente enumerável, isto é, a completude falha sobre modelos finitos. Este resultado é baseado na hipótese de que qualquer sistema dedutivo é de natureza finita. Entretanto, nos podemos relaxar tal hipótese como foi feito no escopo da teoria da prova para aritmética. A teoria da prova tem raízes no programa de Hilbert. Conseqüências teóricas da noção de prova são, por exemplo, relacionadas a teoremas de normalização, consistência, decidibilidade, e resultados de complexidade. A teoria da prova para aritmética também é motivada pelos teoremas de incompletude de Gödel, cujo alvo foi fornecer um exemplo de um princípio matemático verdadeiro e significativo que não é derivável na aritmética de primeira-ordem. Um meio de apresentar esta prova é baseado na definição de um sistema de prova com uma regra infinitária, a w-rule, que estabiliza a consistência da aritmética de primeira-ordem através de uma perspectiva de teoria da prova. Motivados por esta prova, iremos propor aqui um sistema infinitário de prova para LFP que nos permitirá investigar propriedades em teoria da prova. Com tal sistema dedutivo infinito, pretendemos apresentar uma teoria da prova para uma lógica tradicionalmente definida no escopo de FMT. Permanece aberto um caminho alternativo de provar resultados já obtidos com FMT e também novos resultados do ponto de vista da teoria da prova. Além disso, iremos propor um procedimento de normalização com restrições para este sistema dedutivo, que pode ser usado em um provador de teoremas para computar consultas em banco de dados relacionais

FundaÃÃo Cearense de Apoio ao Desenvolvimento Cientifico e TecnolÃgico / A noÃÃo de menor ponto-fixo de um operador à amplamente aplicada na ciÃncia da computaÃÃo como, por exemplo, no contexto das linguagens de consulta para bancos de dados relacionais. Algumas extensÃes da LÃgica de Primeira-Ordem (FOL)1 com operadores de ponto-fixo em estruturas finitas, como a lÃgica de menor ponto-fixo (LFP)2, foram propostas para lidar com problemas relacionados à expressividade de FOL. A LFP captura as classes de complexidade PTIME sobre a classe das estruturas finitas ordenadas. A caracterizaÃÃo descritiva de classes computacionais à uma abordagem central em Teoria do Modelos Finitos (FMT)3. O teorema de Trakhtenbrot, considerado o ponto de partida para FMT, estabelece que a validade sobre modelos finitos nÃo à recursivamente enumerÃvel, isto Ã, a completude falha sobre modelos finitos. Este resultado à baseado na hipÃtese de que qualquer sistema dedutivo à de natureza finita. Entretanto, nos podemos relaxar tal hipÃtese como foi feito no escopo da teoria da prova para aritmÃtica. A teoria da prova tem raÃzes no programa de Hilbert. ConseqÃÃncias teÃricas da noÃÃo de prova sÃo, por exemplo, relacionadas a teoremas de normalizaÃÃo, consistÃncia, decidibilidade, e resultados de complexidade. A teoria da prova para aritmÃtica tambÃm à motivada pelos teoremas de incompletude de GÃdel, cujo alvo foi fornecer um exemplo de um princÃpio matemÃtico verdadeiro e significativo que nÃo à derivÃvel na aritmÃtica de primeira-ordem. Um meio de apresentar esta prova à baseado na definiÃÃo de um sistema de prova com uma regra infinitÃria, a w-rule, que estabiliza a consistÃncia da aritmÃtica de primeira-ordem atravÃs de uma perspectiva de teoria da prova. Motivados por esta prova, iremos propor aqui um sistema infinitÃrio de prova para LFP que nos permitirà investigar propriedades em teoria da prova. Com tal sistema dedutivo infinito, pretendemos apresentar uma teoria da prova para uma lÃgica tradicionalmente definida no escopo de FMT. Permanece aberto um caminho alternativo de provar resultados jà obtidos com FMT e tambÃm novos resultados do ponto de vista da teoria da prova. AlÃm disso, iremos propor um procedimento de normalizaÃÃo com restriÃÃes para este sistema dedutivo, que pode ser usado em um provador de teoremas para computar consultas em banco de dados relacionais / The notion of the least fixed-point of an operator is widely applied in computer science as, for instance, in the context of query languages for relational databases. Some extensions of FOL with _xed-point operators on finite structures, as the least fixed-point logic (LFP), were proposed to deal with problem problems related to the expressivity of FOL. LFP captures the complexity class PTIME over the class of _nite ordered structures. The descriptive characterization of computational classes is a central issue within _nite model theory (FMT). Trakhtenbrot's theorem, considered the starting point of FMT, states that validity over finite models is not recursively enumerable, that is, completeness fails over finite models. This result is based on an underlying assumption that any deductive system is of finite nature. However, we can relax such assumption as done in the scope of proof theory for arithmetic. Proof theory has roots in the Hilbert's programme. Proof theoretical consequences are, for instance, related to normalization theorems, consistency, decidability, and complexity results. The proof theory for arithmetic is also motivated by Godel incompleteness theorems. It aims to o_er an example of a true mathematically meaningful principle not derivable in first-order arithmetic. One way of presenting this proof is based on a definition of a proof system with an infinitary rule, the w-rule, that establishes the consistency of first-order arithmetic through a proof-theoretical perspective. Motivated by this proof, here we will propose an in_nitary proof system for LFP that will allow us to investigate proof theoretical properties. With such in_nitary deductive system, we aim to present a proof theory for a logic traditionally defined within the scope of FMT. It opens up an alternative way of proving results already obtained within FMT and also new results through a proof theoretical perspective. Moreover, we will propose a normalization procedure with some restrictions on the rules, such this deductive system can be used in a theorem prover to compute queries on relational databases.

Orientador : Fernando Jose Von Zuben / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica e de Computação / Made available in DSpace on 2018-08-04T02:17:19Z (GMT). No. of bitstreams: 1 Lima_ClodoaldoAparecidodeMoraes_D.pdf: 5444612 bytes, checksum: 0172ca4143c2737bf19a3b2076c06b44 (MD5) Previous issue date: 2004 / Resumo: Os algoritmos baseados em métodos de kernel destacam-se entre as diversas técnicas de aprendizado de máquina. Eles foram inicialmente empregados na implementação de máquinas de vetores-suporte (SVMs). A abordagem SVM representa um procedimento de aprendizado não-paramétrico para classificação e regressão de alto desempenho. No entanto, existem aspectos estruturais e paramétricos de projeto que podem conduzir a uma degradação de desempenho. Na ausência de uma metodologia sistemática e de baixo custo para a proposição de modelos computacionais otimamente especificados, os comitês de máquinas se apresentam como alternativas promissoras. Existem versões estáticas de comitês, na forma de ensembles de componentes, e versões dinâmicas, na forma de misturas de especialistas. Neste estudo, os componentes de um ensemble e os especialistas de uma mistura são tomados como SVMs. O objetivo é explorar conjuntamente potencialidades advindas de SVM e comitê de máquinas, adotando uma formulação unificada. Várias extensões e novas configurações de comitês de máquinas são propostas, com análises comparativas que indicam ganho significativo de desempenho frente a outras propostas de aprendizado de máquina comumente adotadas para classificação e regressão / Abstract: Algorithms based on kernel methods are prominent techniques among the available approaches for machine learning. They were initially applied to implement support vector machines (SVMs). The SVM approach represents a nonparametric learning procedure devoted to high performance classification and regression tasks. However, structural and parametric aspects of the design may guide to performance degradation. In the absence of a systematic and low-cost methodology for the proposition of optimally specified computational models, committee machines emerge as promising alternatives. There exist static versions of committees, in the form of ensembles of components, and dynamic versions, in the form of mixtures of experts. In the present investigation, the components of an ensemble and the experts of a mixture are taken as SVMs. The aim is to jointly explore the potentialities of both SVM and committee machine, by means of a unified formulation. Several extensions and new configurations of committee machines are proposed, with comparative analyses that indicate significant gain in performance before other proposals for machine learning commonly adopted for classification and regression / Doutorado / Engenharia de Computação / Doutor em Engenharia Elétrica

A definition of abstract logic is presented. This is used to explore and compare some abstract logics, such as logics with generalised quantifiers and infinitary logics, and their properties. Special focus is given to the properties of completeness, compactness, and the Löwenheim-Skolem property. A method of comparing different logics is presented and the concept of equivalent logics introduced. Lastly a proof is given for Lindström's theorem, which provides a characterization of elementary logic, also known as first-order logic, as the strongest logic for which both the compactness property and the Löwenheim-Skolem property, holds.

In 2020 Parusiński and Rond proved that every algebraic set X ⊂ R^n is homeomorphic to an algebraic set X’ ⊂ R^n which is described globally (and also locally) by polynomial equations whose coefficients are real algebraic numbers. In general, the following problem was widely open: Open Problem. Is every real algebraic set homeomorphic to a real algebraic set defined by polynomial equations with rational coefficients? The aim of my PhD thesis is to provide classes of real algebraic sets that positively answer to above Open Problem. In Chapter 1 I introduce a new theory of real and complex algebraic geometry over subfields recently developed by Fernando and Ghiloni. In particular, the main notion to outline is the so called R|Q-regularity of points of a Q-algebraic set X ⊂ R^n. This definition suggests a natural notion of a Q-nonsingular Q-algebraic set X ⊂ R^n. The study of Q-nonsingular Q-algebraic sets is the main topic of Chapter 2. Then, in Chapter 3 I introduce Q-algebraic approximation techniques a là Akbulut-King developed in collaboration with Ghiloni and the main consequences we proved, that are, versions ‘over Q’ of the classical and the relative Nash-Tognoli theorems. Last results can be found in in Chapters 3 & 4, respectively. In particular, we obtained a positive answer to above Open Problem in the case of compact nonsingular algebraic sets. Then, after extending ‘over Q’ the Akbulut-King blowing down lemma, we are in position to give a complete positive answer to above Open Problem also in the case of compact algebraic sets with isolated singularities in Chapter 4. After algebraic Alexandroff compactification, we obtained a positive answer also in the case of non-compact algebraic sets with isolated singularities. Other related topics are investigated in Chapter 4 such as the existence of Q-nonsingular Q-algebraic models of Nash manifolds over every real closed field and an answer to the Q-algebrization problem for germs of an isolated algebraic singularity. Appendices A & B contain results on Nash approximation and an evenness criterion for the degree of global smoothings of subanalytic sets, respectively.

Diese Arbeit untersucht ordnungsinvariante Formeln der Logik erster Stufe (FO) und einiger ihrer Erweiterungen, sowie andere eng verwandte Konzepte der endlichen Modelltheorie. Viele Resultate der endlichen Modelltheorie nehmen an, dass Strukturen mit einer Einbettung ihres Universums in ein Anfangsstück der natürlichen Zahlen ausgestattet sind. Dies erlaubt es, beliebige Relationen (z.B. die lineare Ordnung) und Operationen (z.B. Addition, Multiplikation) von den natürlichen Zahlen auf solche Strukturen zu übertragen. Die resultierenden Relationen auf den endlichen Strukturen werden als numerische Prädikate bezeichnet. Werden numerische Prädikate in Formeln verwendet, beschränkt man sich dabei häufig auf solche Formeln, deren Wahrheitswert auf endlichen Strukturen invariant unter Änderungen der Einbettung der Strukturen ist. Wenn das einzige verwendete numerische Prädikat eine lineare Ordnung ist, spricht man beispielsweise von ordnungsinvarianten Formeln. Die Resultate dieser Arbeit können in drei Teile unterteilt werden. Der erste Teil betrachtet die Lokalitätseigenschaften von FO-Formeln mit Modulo-Zählquantoren, die beliebige numerische Prädikate invariant nutzen. Der zweite Teil betrachtet FO-Sätze, die eine lineare Ordnung samt der zugehörigen Addition auf invariante Weise nutzen, auf endlichen Bäumen. Es wird gezeigt, dass diese dieselben regulären Baumsprachen definieren, wie FO-Sätze ohne numerische Prädikate mit bestimmten Kardinalitätsprädikaten. Für den Beweis wird eine algebraische Charakterisierung der in dieser Logik definierbaren Baumsprachen durch Operationen auf Bäumen entwickelt. Der dritte Teil der Arbeit beschäftigt sich mit der Ausdrucksstärke und der Prägnanz von FO und Erweiterungen von FO auf Klassen von Strukturen beschränkter Baumtiefe. / This thesis studies the concept of order-invariance of formulae of first-order logic (FO) and some of its extensions as well as other closely related concepts from finite model theory. Many results in finite model theory assume that structures are equipped with an embedding of their universe into an initial segment of the natural numbers. This allows to transfer arbitrary relations (e.g. linear order) and operations (e.g. addition, multiplication) on the natural numbers to structures. The arising relations on the structures are called numerical predicates. If formulae use these numerical predicates, it is often desirable to consider only such formulae whose truth value in finite structures is invariant under changes to the embeddings of the structures. If the numerical predicates include only a linear order, such formulae are called order-invariant. We study the effect of the invariant use of different kinds of numerical predicates on the expressive power of FO and extensions thereof. The results of this thesis can be divided into three parts. The first part considers the locality and non-locality properties of formulae of FO with modulo-counting quantifiers which may use arbitrary numerical predicates in an invariant way. The second part considers sentences of FO which may use a linear order and the corresponding addition in an invariant way and obtains a characterisation of the regular finite tree languages which can be defined by such sentences: these are the same tree languages which are definable by FO-sentences without numerical predicates with certain cardinality predicates. For the proof, we obtain a characterisation of the tree languages definable in this logic in terms of algebraic operations on trees. The third part compares the expressive power and the succinctness of different ex- tensions of FO on structures of bounded tree-depth.

Diese Arbeit leistet Beiträge zu drei Gebieten der deskriptiven Komplexitätstheorie. Zunächst adaptieren wir einen repräsentationsinvarianten Graphkanonisierungsalgorithmus mit einfach exponentieller Laufzeit von Corneil und Goldberg (1984) und folgern, dass die Logik "Choiceless Polynomial Time with Counting" auf Strukturen, deren Relationen höchstens Stelligkeit 2 haben, gerade die Polynomialzeit-Eigenschaften (PTIME) von Fragmenten logarithmischer Größe charakterisiert. Der zweite Beitrag untersucht die deskriptive Komplexität von PTIME-Berechnungen auf eingeschränkten Graphklassen. Wir stellen eine neuartige Normalform von Intervallgraphen vor, die sich in Fixpunktlogik mit Zählen (FP+C) definieren lässt, was bedeutet, dass FP+C auf dieser Graphklasse PTIME charakterisiert. Wir adaptieren außerdem unsere Methoden, um einen kanonischen Beschriftungsalgorithmus für Intervallgraphen zu erhalten, der sich mit logarithmischer Platzbeschränkung (LOGSPACE) berechnen lässt. Im dritten Teil der Arbeit beschäftigt uns die ungelöste Frage, ob es eine Logik gibt, die alle Polynomialzeit-Berechnungen charakterisiert. Wir führen eine Reihe von Ranglogiken ein, die die Fähigkeit besitzen, den Rang von Matrizen über Primkörpern zu berechnen. Wir zeigen, dass diese Ergänzung um lineare Algebra robuste Logiken hervor bringt, deren Ausdrucksstärke die von FP+C übertrifft. Außerdem beweisen wir, dass Ranglogiken strikt an Ausdrucksstärke gewinnen, wenn wir die Zahl an Variablen erhöhen, die die betrachteten Matrizen indizieren. Dann bauen wir eine Brücke zur klassischen Komplexitätstheorie, indem wir über geordneten Strukturen eine Reihe von Komplexitätsklassen zwischen LOGSPACE und PTIME durch Ranglogiken charakterisieren. Die Arbeit etabliert die stärkste der Ranglogiken als Kandidat für die Charakterisierung von PTIME und legt nahe, dass Ranglogiken genauer erforscht werden müssen, um weitere Fortschritte im Hinblick auf eine Logik für Polynomialzeit zu erzielen. / This thesis is making contributions to three strands of descriptive complexity theory. First, we adapt a representation-invariant, singly exponential-time graph canonization algorithm of Corneil and Goldberg (1984) and conclude that on structures whose relations are of arity at most 2, the logic "Choiceless Polynomial Time with Counting" precisely characterizes the polynomial-time (PTIME) properties of logarithmic-size fragments. The second contribution investigates the descriptive complexity of PTIME computations on restricted classes of graphs. We present a novel canonical form for the class of interval graphs which is definable in fixed-point logic with counting (FP+C), which shows that FP+C captures PTIME on this graph class. We also adapt our methods to obtain a canonical labeling algorithm for interval graphs which is computable in logarithmic space (LOGSPACE). The final part of this thesis takes aim at the open question whether there exists a logic which generally captures polynomial-time computations. We introduce a variety of rank logics with the ability to compute the ranks of matrices over (finite) prime fields. We argue that this introduction of linear algebra results in robust logics whose expressiveness surpasses that of FP+C. Additionally, we establish that rank logics strictly gain in expressiveness when increasing the number of variables that index the matrices we consider. Then we establish a direct connection to standard complexity theory by showing that in the presence of orders, a variety of complexity classes between LOGSPACE and PTIME can be characterized by suitable rank logics. Our exposition provides evidence that rank logics are a natural object to study and establishes the most expressive of our rank logics as a viable candidate for capturing PTIME, suggesting that rank logics need to be better understood if progress is to be made towards a logic for polynomial time.

本論文乃是藉由現代中醫科學研究，進一步指出中醫科學化的可能性及其問題。由於中醫理論十分駁雜，筆者將焦點主要集中於中醫脈診之上，藉由汪叔游和王唯工的研究，來討論中醫脈診科學化的可能性和問題。 本論文進行方式，主要可分為兩個步驟，首先針對傳統中醫理論地位的問題加以討論，其次乃是針對現代中醫實驗。 在第一步驟中，筆者提出一個理論作為科學理論所必須符合的最低標準，即是科學化三原則，分別是：可落實原則、主體際性原則以及系統化原則。藉由科學化三原則筆者嘗試論證傳統中醫並非是科學理論或是經驗有效的理論，最多僅能將中醫醫療實踐視為經驗有效的醫療診斷技術。 在第二步驟中，筆者藉由汪叔游和王唯工的實驗，來討論其經驗上和概念上的問題。藉由兩人的研究，筆者將進一步指出中醫科學化的過程中，必須經過理論的重新建構，而不是僅在於累積客觀的經驗資料就可證實中醫理論。

In der vorliegenden Arbeit wird eine Methodik zur Entwicklung mechanischer Simulationen der Interaktion Sportler-Sportgerät-Umwelt zur Untersuchung der Funktionalität von Sportgeräten konzipiert und vorgestellt. Die mechanische Simulation ist die gegenständliche Nachbildung spezieller Teilaspekte des Sportlers, z.B. der Körperform, der Trägheitseigenschaften, der Masse, der Interaktionskräfte zur Umwelt oder charakteristischer Bewegungsabläufe zum Zweck der Durchführung gezielter Experimente zur Untersuchung des dynamischen Systemverhaltens Sportler-Sportgerät-Umwelt. Dazu werden drei Fallbeispiele aus der Forschungstätigkeit der Arbeitsgruppe HLST an der Technischen Universität Chemnitz mit Methoden zur Verifikation von Simulationsmodellen – dem strukturierten Durchgehen, der Validierung im Dialog und dem Schreibtischtest – analysiert. Die Analyseergebnisse werden in eine Grobstruktur eingebettet, die aus relevanten Vorarbeiten zur Anwendung der Allgemeinen Modelltheorie abgeleitet ist. Die in den jeweiligen Fallbeispielen verwendeten Prozessschritte, Methoden und Werkzeuge werden dargestellt und die Entwicklungsergebnisse erörtert. Im Abschluss jedes Fallbeispiels wird der Entwicklungsprozess anhand von einheitlichen Kriterien bewertet. In einem abschließenden Schritt erfolgt die Zusammenführung der im Stand der Technik dargelegten Grundlagen und der in den drei Fallbeispielen gewonnenen Informationen zu einer strukturieren und kommentierten Methodik.:1 Einleitung 8 1.1 Definitionen 8 1.2 Einsatzgebiete der mechanischen Simulation 11 1.2.1 Überblick 11 1.2.2 Sicherheit gegen Versagen 12 1.2.3 Konformität 14 1.2.4 Funktionalität 15 1.3 Motivation und Zielsetzung 16 1.4 Aufbau der Arbeit 16 2 Theoretische Grundlagen 18 2.1 Experimentelle Methoden der Sportgeräteentwicklung 18 2.1.1 Einordnung nach Odenwald (2006) 18 2.1.2 Einordnung nach Witte (2013) 19 2.1.3 Einordnung nach Senner (2001) 20 2.1.4 Eigene Systematisierung 23 2.2 Allgemeine Modelltheorie 26 2.3 Existierende Ansätze für die Applikation der Allgemeinen Modelltheorie 29 2.3.1 Anwendung der AMT in der Chemie 29 2.3.2 Anwendung der AMT in der Biomechanik 30 2.3.3 Anwendung der AMT in Logistik und Produktion 32 2.3.4 Fazit 37 3 Präzisierung der Problemstellung 38 4 Methodik 39 5 Fallbeispiel Schwimmanzug – Strömungswiderstand 41 5.1 Vorbemerkungen 41 5.2 Aufgabenanalyse 42 5.2.1 Definition der zu untersuchenden Funktionalität des Sportgeräts 42 5.2.2 Analyse der zugrundeliegenden technischen Funktion des Sportgeräts 42 5.2.3 Analyse der Simulationswürdigkeit 43 5.2.4 Identifikation des Originals 47 5.3 Modellformulierung 48 5.3.1 Modellansatz 48 5.3.2 Modellsynthese 50 5.4 Modellimplementierung 53 5.4.1 Herstellung des Strömungskörpers 53 5.4.2 Simulation der Fortbewegung im Wasser 54 5.5 Modellanwendung 57 5.6 Modellüberprüfung 60 5.6.1 Abgleich zwischen den experimentellen Ergebnissen und dem theoretischen Modell 60 5.6.2 Vergleich mit dem Original 62 5.7 Fazit 67 6 Fallbeispiel Laufschuh – Stoßabsorption 69 6.1 Vorbemerkungen 69 6.2 Aufgabenanalyse 69 6.2.1 Definition der zu untersuchenden Funktionalität 69 6.2.2 Analyse der zugrundeliegenden technischen Funktion des Sportgeräts 71 6.2.3 Analyse der Simulationswürdigkeit 71 6.2.4 Definition des Originals 72 6.3 Modellformulierung 72 6.3.1 Modellansatz 72 6.3.2 Systemanalyse 72 6.3.3 Modellsynthese 77 6.4 Modellimplementierung 78 6.4.1 Krafterzeugung 78 6.4.2 Kraftübertragung 79 6.5 Modellanwendung 81 6.6 Modellüberprüfung 82 6.6.1 Soll-Istwert-Vergleich 82 6.6.2 Reliabilität 83 6.6.3 Korrelation zu Stoßbelastungsvariablen 85 6.6.4 Ereignisvaliditätstest: Sohlentemperatur 86 6.6.5 Ereignisvaliditätstest: Sohlendeformation 88 6.7 Fazit 91 7 Fallbeispiel Fußballschuh – Traktionseigenschaften 94 7.1 Vorbemerkungen 94 7.2 Aufgabenanalyse 94 7.2.1 Definition der zu untersuchenden Funktionalität 94 7.2.2 Analyse der zugrundeliegenden technischen Funktion des Sportgeräts 95 7.2.3 Analyse der Simulationswürdigkeit 96 7.2.4 Definition des Originals 97 7.3 Modellformulierung 98 7.3.1 Modellansatz 98 7.3.2 Systemanalyse 98 7.3.3 Modellsynthese 106 7.4 Modellimplementierung 107 7.5 Modellanwendung 110 7.6 Modellüberprüfung 114 7.6.1 Reliabilität 114 7.6.2 Sensitivitätsanalyse: Normalkraft 114 7.6.3 Sensitivitätsanalyse: Kraftanstieg horizontal 116 7.6.4 Vergleich mit der Realität 116 7.7 Fazit 117 8 Methodik zur Entwicklung mechanischer Simulationen der Interaktion Sportler-Sportgerät-Umwelt 119 8.1 Schematische Darstellung 119 8.2 Erläuterung der Vorgehensempfehlung 120 8.2.1 Klärung der Problemstellung 120 8.2.2 Modellbildung 122 8.2.3 Modellanwendung 124 9 Schlussbetrachtung 126 Literaturverzeichnis 128 Tabellenverzeichnis 133 Abbildungsverzeichnis 135 Danksagung 138 Selbstständigkeitserklärung 139 Lebenslauf 140 / In this dissertation a methodology is conceived that aims to structure the development process of test arrangements that mechanically simulate the interaction of athlete, sports equipment and environment. Mechanical simulation in this context is defined as the physical replication of specific properties of the athlete (e.g. the shape of the human body, body weight, joint kinematics, inertia, external forces in specific movements) in order to conduct experiments to investigate the dynamic behavior of the system athlete-equipment-environment. Therefore, three case studies of mechanical simulation models that have been developed at Technische Universität Chemnitz are analyzed by applying the validation and verification methods “structured walkthrough”, “face validity” and “desk checking”. The results of that analysis are embedded into a framework that is derived by literature review on applied model theory. For each of the three development processes the procedure model is identified and main tools and methods are discussed. Every case study is finally assessed by using standardized evaluation criterions. Finally, the main findings of the analysis of the case studies as well as knowledge obtained by reviewing the state of the art in model theory and simulation methods are used to build up a structured and commentated guideline.:1 Einleitung 8 1.1 Definitionen 8 1.2 Einsatzgebiete der mechanischen Simulation 11 1.2.1 Überblick 11 1.2.2 Sicherheit gegen Versagen 12 1.2.3 Konformität 14 1.2.4 Funktionalität 15 1.3 Motivation und Zielsetzung 16 1.4 Aufbau der Arbeit 16 2 Theoretische Grundlagen 18 2.1 Experimentelle Methoden der Sportgeräteentwicklung 18 2.1.1 Einordnung nach Odenwald (2006) 18 2.1.2 Einordnung nach Witte (2013) 19 2.1.3 Einordnung nach Senner (2001) 20 2.1.4 Eigene Systematisierung 23 2.2 Allgemeine Modelltheorie 26 2.3 Existierende Ansätze für die Applikation der Allgemeinen Modelltheorie 29 2.3.1 Anwendung der AMT in der Chemie 29 2.3.2 Anwendung der AMT in der Biomechanik 30 2.3.3 Anwendung der AMT in Logistik und Produktion 32 2.3.4 Fazit 37 3 Präzisierung der Problemstellung 38 4 Methodik 39 5 Fallbeispiel Schwimmanzug – Strömungswiderstand 41 5.1 Vorbemerkungen 41 5.2 Aufgabenanalyse 42 5.2.1 Definition der zu untersuchenden Funktionalität des Sportgeräts 42 5.2.2 Analyse der zugrundeliegenden technischen Funktion des Sportgeräts 42 5.2.3 Analyse der Simulationswürdigkeit 43 5.2.4 Identifikation des Originals 47 5.3 Modellformulierung 48 5.3.1 Modellansatz 48 5.3.2 Modellsynthese 50 5.4 Modellimplementierung 53 5.4.1 Herstellung des Strömungskörpers 53 5.4.2 Simulation der Fortbewegung im Wasser 54 5.5 Modellanwendung 57 5.6 Modellüberprüfung 60 5.6.1 Abgleich zwischen den experimentellen Ergebnissen und dem theoretischen Modell 60 5.6.2 Vergleich mit dem Original 62 5.7 Fazit 67 6 Fallbeispiel Laufschuh – Stoßabsorption 69 6.1 Vorbemerkungen 69 6.2 Aufgabenanalyse 69 6.2.1 Definition der zu untersuchenden Funktionalität 69 6.2.2 Analyse der zugrundeliegenden technischen Funktion des Sportgeräts 71 6.2.3 Analyse der Simulationswürdigkeit 71 6.2.4 Definition des Originals 72 6.3 Modellformulierung 72 6.3.1 Modellansatz 72 6.3.2 Systemanalyse 72 6.3.3 Modellsynthese 77 6.4 Modellimplementierung 78 6.4.1 Krafterzeugung 78 6.4.2 Kraftübertragung 79 6.5 Modellanwendung 81 6.6 Modellüberprüfung 82 6.6.1 Soll-Istwert-Vergleich 82 6.6.2 Reliabilität 83 6.6.3 Korrelation zu Stoßbelastungsvariablen 85 6.6.4 Ereignisvaliditätstest: Sohlentemperatur 86 6.6.5 Ereignisvaliditätstest: Sohlendeformation 88 6.7 Fazit 91 7 Fallbeispiel Fußballschuh – Traktionseigenschaften 94 7.1 Vorbemerkungen 94 7.2 Aufgabenanalyse 94 7.2.1 Definition der zu untersuchenden Funktionalität 94 7.2.2 Analyse der zugrundeliegenden technischen Funktion des Sportgeräts 95 7.2.3 Analyse der Simulationswürdigkeit 96 7.2.4 Definition des Originals 97 7.3 Modellformulierung 98 7.3.1 Modellansatz 98 7.3.2 Systemanalyse 98 7.3.3 Modellsynthese 106 7.4 Modellimplementierung 107 7.5 Modellanwendung 110 7.6 Modellüberprüfung 114 7.6.1 Reliabilität 114 7.6.2 Sensitivitätsanalyse: Normalkraft 114 7.6.3 Sensitivitätsanalyse: Kraftanstieg horizontal 116 7.6.4 Vergleich mit der Realität 116 7.7 Fazit 117 8 Methodik zur Entwicklung mechanischer Simulationen der Interaktion Sportler-Sportgerät-Umwelt 119 8.1 Schematische Darstellung 119 8.2 Erläuterung der Vorgehensempfehlung 120 8.2.1 Klärung der Problemstellung 120 8.2.2 Modellbildung 122 8.2.3 Modellanwendung 124 9 Schlussbetrachtung 126 Literaturverzeichnis 128 Tabellenverzeichnis 133 Abbildungsverzeichnis 135 Danksagung 138 Selbstständigkeitserklärung 139 Lebenslauf 140

No description available.