CAPES / Nesse trabalho identificamos os objetivos e as orientações nos Parâmetros Curriculares Nacionais, do terceiro e quarto ciclos, sobre o estudo da Geometria. Pesquisamos sobre a Biografia de Tales de Mileto, onde fazemos um relato, da região e história, da época em que ele viveu, contamos alguns de seus feitos, e enumeramos os teoremas cujas demonstrações lhe são atribuídas. Analisamos seis livros didáticos do 9º ano do ensino fundamental, que integram o Plano Nacional do Livro Didático 2014, observamos a forma como a Geometria é trabalhada, e quais as demonstrações e atividades apresentadas em relação ao Teorema de Tales. Usamos e recomendamos o software Geogebra para o estudo da Geometria. Propomos atividades diversificadas, para serem utilizadas em sala de aula, quando o Teorema de Tales for trabalhado. Sugerimos uma demonstração para o Teorema de Tales, onde utilizamos a definição de área do triângulo, e as propriedades do paralelogramo. / In this work we identify the goals and guidelines the National Curriculum Guidelines, the third and fourth cycles, on the study of geometry. We searched on the Biography of Thales of Miletus, where we do a story, and history of the region, the era in which he lived, we count some of their deeds, and enumerate the theorems whose statements are allocated. We analyzed six textbooks in 9th grade of elementary school, comprising the National Plan of Didactic Book 2014, observed how the geometry is crafted, and what activities and statements made with respect to the Thales’ Theorem. We use and recommend the Geogebra software for the study of geometry. We propose diversified activities for use in the classroom when the Thales’ Theorem is working. We suggest a demonstration of Thales’ Theorem, where we use the definition of the triangle area, and properties of the parallelogram.

Made available in DSpace on 2015-04-11T14:03:20Z (GMT). No. of bitstreams: 1 HERBERT OLIVEIRA.pdf: 512075 bytes, checksum: acc5d05442df938abdfa025f9db23367 (MD5) Previous issue date: 2011-02-04 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The use of computer-based systems in several domains has increased significantly over the last years, one of the main challenges in software development of these systems is to ensure the correctness and reliability of these. So that software verification now plays an important role in ensuring the overall product quality, aimed mainly the characteristics of predictability and reliability. In the context of software verification, with respect to the use of model checking technique, Bounded Model Checkers have already been applied to discover subtle errors in actual systems projects, contributing effectively in this verification process. The value of the counterexample and safety properties generated by Bounded Model Checkers to create test case and to debug these systems is widely recognized. When a Bounded Model Checking (BMC) finds an error it produces a counterexample. Thus, the value of counterexamples to debug software systems is widely recognized in the state-of-the-practice. However, BMCs often produce counterexamples that are either large or difficult to be understood and manipulated mainly because of both the software size and the values chosen by the respective solver. In this work we aim to demonstrate and analyze the use of formal methods (through using the model checking technique) in the process of developing programs in C language, exploring the features already provided by the model checking as the counterexample and the identification and verification of safety properties. In view of this we present two approaches: (i) we describe a method to integrate the bounded model checker ESBMC with the CUnit framework. This method aims to extract the safety properties generated by ESBMC to generate automatically test cases using the rich set of assertions provided by the CUnit framework and (ii) a method aims to automate the collection and manipulation of counterexamples in order to instantiate the analised C program for proving the root cause of the identified error. Such methods may be seen as a complementary technique for the verification performed by BMCs. We show the effectiveness of our proposed method over publicly available benchmarks of C programs. / A utilização de sistemas baseados em computador em diversos domínios aumentou significativamente nos últimos anos. Um dos principais desafios no desenvolvimento de software de sistemas críticos é a garantia da sua correção e confiabilidade. Desta forma, a verificação de software exerce um papel importante para assegurar a qualidade geral do produto, visando principalmente características como previsibilidade e confiabilidade. No contexto de verificação de software, os Bounded Model Checkers estão sendo utilizados para descobrir erros sutis em projetos de sistemas de software atuais, contribuindo eficazmente neste processo de verificação. O valor dos contra-exemplos e propriedades de segurança gerados pelo Bounded Model Checkers para criar casos de testes e para a depuração de sistemas é amplamente reconhecido. Quando um Bounded Model Checking (BMC) encontra um erro ele produz um contra-exemplo. Assim, o valor dos contra-exemplos para depuração de software é amplamente reconhecido no estado da prática. Entretanto, os BMCs frequentemente produzem contra-exemplos que são grandes ou difíceis de entender ou manipular, principalmente devido ao tamanho do software e valores escolhidos pelo solucionador de satisfabilidade. Neste trabalho visamos demonstrar e analisar o uso de método formal (através da técnica model checking) no processo de desenvolvimento de programas na linguagem C, explorando as características já providas pelo model checking como o contra-exemplo e a identificação e verificação de propriedades de segurança. Em face disto apresentamos duas abordagens: (i) descrevemos um método para integrar o Bounded Model Checker ESBMC como o framework de teste unitário CUnit, este método visa extrair as propriedades geradas pelo ESBMC para gerar automaticamente casos de teste usando o rico conjunto de assertivas providas pelo framework CUnit e (ii) um método que visa automatizar a coleta e manipulação dos contra-exemplos, de modo a instanciar o programa C analisado, para comprovar a causa raiz do erro identificado. Tais métodos podem ser vistos como um método complementar para a verificação efetuada pelos BMCs. Demonstramos a eficácia dos métodos propostos sobre benchmarks públicos de código C.

We present a series of improvements to the Hybrid system, a formal theory implemented in Isabelle/HOL to support specifying and reasoning about formal systems using higher-order abstract syntax (HOAS). We modify Hybrid's type of terms, which is built definitionally in terms of de Bruijn indices, to exclude at the type level terms with `dangling' indices. We strengthen the injectivity property for Hybrid's variable-binding operator, and develop rules for compositional proof of its side condition, avoiding conversion from HOAS to de Bruijn indices. We prove representational adequacy of Hybrid (with these improvements) for a lambda-calculus-like subset of Isabelle/HOL syntax, at the level of set-theoretic semantics and without unfolding Hybrid's definition in terms of de Bruijn indices. In further work, we prove an induction principle that maintains some of the benefits of HOAS even for open terms. We also present a case study of the formalization in Hybrid of a small programming language, Mini-ML with mutable references, including its operational semantics and a type-safety property. This is the largest case study in Hybrid to date, and the first to formalize a language with mutable references. We compare four variants of this formalization based on the two-level approach adopted by Felty and Momigliano in other recent work on Hybrid, with various specification logics (SLs), including substructural logics, formalized in Isabelle/HOL and used in turn to encode judgments of the object language. We also compare these with a variant that does not use an intermediate SL layer. In the course of the case study, we explore and develop new proof techniques, particularly in connection with context invariants and induction on SL statements.

The aim of this diploma thesis is the research of building polygons for the testing of autonomous vehicles, from the point of view of road technology and also designing aspects. In the thesis are mentioned 9 most important world test polygons and their description of design parameters. There are described particular stages of automation from foreign organizations which are concerned with research and development in the automotive industry. In addition, there are described basic advanced driver assistance systems and connectivity between vehicles and infrastructure. Conclusion also contains the assessment of existing aerodrome test areas for autonomous vehicles.

While automated game playing systems like Deep Blue perform excellent within their domain, handling a different game or even a slight change of rules is impossible without intervention of the programmer. Considered a great challenge for Artificial Intelligence, General Game Playing is concerned with the development of techniques that enable computer programs to play arbitrary, possibly unknown n-player games given nothing but the game rules in a tailor-made description language. A key to success in this endeavour is the ability to reliably extract hidden game-specific features from a given game description automatically. An informed general game player can efficiently play a game by exploiting structural game properties to choose the currently most appropriate algorithm, to construct a suited heuristic, or to apply techniques that reduce the search space. In addition, an automated method for property extraction can provide valuable assistance for the discovery of specification bugs during game design by providing information about the mechanics of the currently specified game description. The recent extension of the description language to games with incomplete information and elements of chance further induces the need for the detection of game properties involving player knowledge in several stages of the game. In this thesis, we develop a formal proof method for the automatic acquisition of rich game-specific invariance properties. To this end, we first introduce a simple yet expressive property description language to address knowledge-free game properties which may involve arbitrary finite sequences of successive game states. We specify a semantic based on state transition systems over the Game Description Language, and develop a provably correct formal theory which allows to show the validity of game properties with respect to their semantic across all reachable game states. Our proof theory does not require to visit every single reachable state. Instead, it applies an induction principle on the game rules based on the generation of answer set programs, allowing to apply any off-the-shelf answer set solver to practically verify invariance properties even in complex games whose state space cannot totally be explored. To account for the recent extension of the description language to games with incomplete information and elements of chance, we correctly extend our induction method to properties involving player knowledge. With an extensive evaluation we show its practical applicability even in complex games.

Cette thèse porte sur la vérification des règles ajoutées de l'Atelier B en utilisant une plate-forme appelée BCARe qui repose sur un plongement de la théorie sous-jacente à la méthode B (théorie de B) dans l'assistant à la preuve Coq. En particulier, nous proposons trois approches pour prouver la validité d'une règle, ce qui revient à prouver une formule exprimée dans la théorie de B. Ces trois approches ont été évaluées sur les règles de la base de règles de SIEMENS IC-MOL. La première approche dite autarcique est développée avec le langage de tactiques de Coq Ltac.  Elle repose sur une première étape qui consiste à déplier tous les opérateurs ensemblistes pour obtenir une formule de la logique du premier ordre. Puis nous appliquons une procédure de décision qui met en oeuvre une heuristique naïve en ce qui concerne les instanciations. La deuxième approche, dite sceptique,appelle le prouveur automatique de théorèmes Zenon après avoir effectué l'étape de normalisation précédente. Nous vérifions ensuite les preuves trouvées par Zenon dans le plongement profond de B en Coq.  La troisième approche évite l'étape de normalisation précédente grâce à une extension de Zenon utilisant des règles d'inférence spécifiques à la théorie de B. Ces règles sont obtenues grâce à la technique de superdéduction. Cette dernière approche est généralisée en une extension de Zenon à toute théorie grâce à un calcul dynamique des règles de superdéduction. Ce nouvel outil, appelé Super Zenon, peut par exemple prouver des problèmes issus de la bibliothèque de problèmes TPTP. / The purpose of this thesis is the verification of Atelier B added rules using the framework named BCARe which relies on a deep embedding of the B theory within the logic of the Coq proof assistant. We propose especially three approaches in order to prove the validity of a rule, which amounts to prove a formula expressed in the B theory. These three approaches have been assessed on the rules coming from the rule database maintained by Siemens IC-MOL.  To do so, the first approach, so-called autarkic approach, is developed thanks to the Coq tactic language, Ltac. It rests upon a first step which consists in unfolding the set operators so as to obtain a first order formula.  A decision procedure which implements an heuristic is applied afterwards to deal with instantiation.  We propose a second approach, so-called skeptic approach, which uses the automated first order theorem prover Zenon, after the previous normalization step has been applied.  Then we verify the Zenon proofs in the deep embedding of B in Coq. A third approach consists in using anextension of Zenon to the B method thanks to the superdeduction. Superdeduction allows us to add the axioms of the B theory by means of deduction rules in the proof mechanism of Zenon. This last approach is generalized in an extension of Zenon to every theory thanks to a dynamic calculus of the superdeduction rules. This new tool, named Super Zenon, is able to prove problems coming from the problem library TPTP, for example.

HolBA is a binary analysis library that can be used to formally verify binary programs using contracts. It is developed in the interactive theorem prover HOL4 to achieve a high degree of trust in verification, the result of verification is a machine-checked proof demonstrating its correctness. This thesis presents two proof-producing procedures. The first resolve indirect jumps in BIR, the binary intermediate language used in HolBA, given their possible targets. The second transfers contracts proved on resolved BIR programs without indirect jumps to the original ones containing indirect jumps. This allows the existing weakest precondition generator to automatically prove contracts on loop-free BIR fragments containing indirect jumps. The implemented proof-producing procedures were evaluated on a small binary program and generated synthetic BIR programs. It was found that the first proof-producing procedure is not very efficient, which could pose a problem when verifying large binary programs. Future work could include improving the efficiency of the first proof-producing procedure and integrate it with an external tool that automatically finds possible targets of indirect jumps. / HolBA är ett bibliotek för binär analys som kan användas för att formellt verifiera binära program med kontrakt. Det är utvecklat i den interaktiva teorembevisaren HOL4 för att åstadkomma en hög grad av tillit till verifiering, resultatet av verifiering är ett maskin-kontrollerat bevis som demonstrerar dess korrekthet. Detta arbete presenterar två bevis-producerande procedurer. Den första bestämmer indirekta hopp i BIR, den binära mellanliggande representationen som används i HolBA, givet deras möjliga mål. Den andra överför kontrakt bevisade för bestämda BIR program utan indirekta hopp till originalen med indirekta hopp. Detta möjliggör den existerande svagaste förutsättning generatorn att automatiskt bevisa kontrakt för sling-fria BIR fragment som innehåller indirekta hopp. De implementerade bevis-producerande procedurerna utvärderades med ett litet binärt program och med genererade syntetiska BIR program. Det visades att den första bevis-producerande proceduren inte är särskilt effektiv, vilket skulle kunna vara ett problem vid verifiering av stora binära program. Framtida arbete skulle kunna inkludera att förbättra effektiviteten för den första bevis-producerande proceduren och att integrera den med ett externt verktyg som automatiskt kan hitta de möjliga målen för indirekta hopp.

Både elever och lärare på gymnasienivå har svårigheter med bevis och bevisföring. Dessutom har det visat sig att bevis och bevisföring spelar en begränsad roll i matematikundervisning. Hur lärare ser på bevisets roll i matematikundervisningen kan påverka tillvägagångssättet för bevisundervisning. Syftet med studien är att belysa hur lärare ser på bevis och bevisföring när det gäller matematikundervisning på gymnasienivå. I studien har nio matematiklärare intervjuats om deras syn på bevisets roll i undervisningen, och hur de arbetar i praktiken med bevis och bevisföring. Intervjudata har analyserats tematiskt, baserat på en teori inspirerad av Knuths (2002a; 2002b) forskning om lärarnas uppfattningar om bevis. Teorin listar sex funktioner som bevis kan ha i matematikundervisning. Det framgår av studien att de flesta lärarna prioriterar förklaring, kommunikation och utveckling av logiskt tänkande när det gäller bevisets roll i undervisning. Resultaten visar även att lärarna anser att bevisundervisning främjar utvecklingen av problemlösningsförmågan. Den strukturerade progressionen och användningen av logiska steg som präglar bevisföringsprocessen utgör grunden för problemlösning. Det kan därför ses som rimligt att införa fler bevisföringsmoment i matematikundervisning. / Both pupils and teachers at upper-secondary school level have difficulties with proof and proving. Furthermore, proof and proving have been shown to play a limited role in mathematics teaching. How teachers view the role of proof in mathematics teaching can affect their approach to teaching proof. The aim of the study was to examine how teachers view proof and proving in the context of mathematics teaching at upper-secondary school level. Nine teachers were interviewed about how they viewed the role of proof in teaching and how they worked in practice with proof and proving. The data was analysed thematically, based on a theory inspired by Knuth’s (2002a; 2002b) research into teachers’ conceptions of proof. The theory lists six functions that proof can have in mathematics teaching. The study shows that most of the teachers prioritise explanation, communication and development of logical thinking as the roles of proof in teaching. The results also show that teachers believe that the teaching of proof promotes the development of problem-solving skills. The proving process is characterized by structured progression and use of logical steps that form the basis for problem-solving. It is therefore reasonable to include more teaching of proof in mathematics education.

In classical propositional logic (CPL) logical reasoning is formalised as logical entailment and can be computed by means of tableau and resolution proof procedures. Unfortunately CPL is not expressive enough and using first order logic (FOL) does not solve the problem either since proof procedures for these logics are not decidable. Modal propositional logics (MPL) on the other hand are both decidable and more expressive than CPL. It therefore seems reasonable to apply tableau and resolution proof systems to MPL in order to compute logical entailment in MPL. Although some of the principles in CPL are present in MPL, there are complexities in MPL that are not present in CPL. Tableau and resolution proof systems which address these issues and others will be surveyed here. In particular the work of Abadi & Manna (1986), Chan (1987), del Cerro & Herzig (1988), Fitting (1983, 1990) and Gore (1995) will be reviewed. / Computing / M. Sc. (Computer Science)

In this dissertation a formalisation of nonmonotonic reasoning, namely Default logic, is discussed. A proof theory for default logic and a variant of Default logic - Prioritised Default logic - is presented. We also pursue an investigation into the relationship between default reasoning and making inferences in a neural network. The inference problem shifts from the logical problem in Default logic to the optimisation problem in neural networks, in which maximum consistency is aimed at The inference is realised as an adaptation process that identifies and resolves conflicts between existing knowledge about the relevant world and external information. Knowledge and data are transformed into constraint equations and the nodes in the network represent propositions and constraint equations. The violation of constraints is formulated in terms of an energy function. The Hopfield network is shown to be suitable for modelling optimisation problems and default reasoning. / Computer Science / M.Sc. (Computer Science)