Interactive simulations to physics teaching: a case study in brazilian high school

This paper presents the results of a study that investigated the use of simulators to improve physics teaching. The study population consisted of eight classes totaling 205 second year high school students from Brazilian public school. The research methodology adopted compares the average performance of students on tests conducted in the classroom to performance on tests conducted in the laboratory using computer simulators. The results obtained showed that students’ performance on tests improved after the use of simulators. It was found that the students had more homogeneous test results when using the simulator.

Measured and modeled interactive effects of potassium deficiency and water deficit on gross primary productivity and light-use efficiency in Eucalyptus grandis plantations

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Teacher-learning process based on an immersive and interactive environment

This paper explores the benefits of using immersive and interactive multiprojection environments (CAVE) to visualize molecules, and how it improves users’ understanding. We have proposed and implemented a tool for teachers to manipulate molecules and another to edit molecules and assist students at home. The contribution of the present research project are these tool that allows investigating structures, properties and dynamics of a molecular system which are extremely complex and comprises millions of atoms. The experience is enriched through multimedia information associated with parts of the model; for example, videos and text can be linked to specific molecule, demonstrating some detail. This solution is based on a teaching-learning process.

The interactive whiteboard in primary school: a case study of a brazilian district school

Interactive whiteboards (IWB) consist of a set of technological equipment organized in order to fulfill a specific task, enabling the development of didactic activities. Because they are associated to computers’ potentiality, interactive whiteboards can provide bigger interactivity between: teacher and students, students and content, and among students. This work’s main objective is to present some of the results yielded from a research related to the way students perceive interactive whiteboards in the classroom. In order to analyze the IWB usage dynamics, some educational applications in the field of mathematics were applied in the 3rd grade of elementary school. Aside from observation, video recordings were made and students were interviewed about the interactive whiteboard, in order to understand how these students observe and engage with the technological tool. IWB do not transform classroom’s reality by themselves, however, their physical presence and usage amount to external reinforcement can change student’s behavior positively.

ENHANCEMENT OF THE FAA’s ON-LINE WILDLIFE AIRCRAFT STRIKE DATABASE WITH AN INTERACTIVE GRAPHICS CAPABILITY

Embry-Riddle Aeronautical University (Prescott, AZ, USA) was awarded a grant from the William J. Hughes FAA Technical Center in October 1999 to develop and maintain a web site dealing with a wide variety of airport safety wildlife concerns. Initially, the web site enabled users to access related topics such as wildlife management (at/near airports), bird identification information, FAA wildlife management guidelines, education, pictures, current news, upcoming meetings and training, available jobs and discussion/forum sections. In April 2001, the web site was augmented with an on-line wildlife strike report (FAA Form 5200-7). Upon submittal on-line, “quick look” email notifications are sent to concerned government personnel. The distribution of these emails varies as to whether there was damage, human injuries/fatalities, and whether feather remains were collected and will be sent to the Smithsonian Institution for identification. In July 2002, a real-time on-line query system was incorporated to allow federal and local government agencies, airport and operator personnel, and USDA and airport wildlife biologists to access this database (which as of June 2005 contains 68,288 researched strike reports added to at a rate of approximately 500 strike reports/month) to formulate strategies to reduce the hazards wildlife present to aviation. To date (June 2005), over 15,000 on-line real-time queries were processed. In June 2004, ERAU was authorized to develop a graphical interface to this on-line query system. Current capabilities include mapping strikes (by species) on the US map, each of the contiguous 48 state maps (with AK and HI being added), and airport diagrams of the major metropolitan airports as well as the next 46 airports with the most reported strikes The latter capability depicts strikes by runway in plan as well as in elevation view. Currently under development is the ability to view time-sequenced strikes on the US map. This extensive graphical interface will give analysts the ability to view strike patterns with a wide variety of variables including species, seasons, migration patterns, etc. on US and state maps and airport diagrams.

Music at the Fair! The Trans- Mississippi and International Exposition. An Interactive Website

“Music at the Fair!” gives the daily musical programs for The Trans-Mississippi and International Exposition, held in Omaha, Nebraska, June 1 through October 31, 1898. The Trans-Mississippi and International Exposition brought an unprecedented array of local, national, and international musical acts to Omaha, NE in 1898. This served to designate Omaha, "the gateway to the west" as a musical hub, as well as to incite musical excitement in the region. Some of the more popular acts featured were the Theodore Thomas Orchestra, the U.S. Marine Band, and the Apollo Club of Chicago. Many more groups and their musical programs can be found within the pages of this site. The “Music at the Fair!” website was created by Grace Carey, and last revised on May 19, 2006.It is the result of a two- year research grant funded by an Undergraduate Creative Activities and Research Experiences (UCARE) grant through the University of Nebraska at Lincoln. It is an extension of an ongoing project on music at the TME by Music Professor Peter Lefferts. The primary sources of information for the site are the following newspapers from June – November 1898: The Omaha Daily Bee, the Omaha Evening Bee, and the Omaha World Herald, and the the official programs of the fair located in the archives at the Omaha Public Library. I would like to thank the helpful staff at the Nebraska State Historical Society and the downtown branch of the Omaha Public Library. Site Creator: Grace Carey Project Advisor: Peter Lefferts, Professor of Music History at the University of Nebraska, Lincoln The linked “Document” is a flat PDF version of the interactive website. To download the fully interactive html version, click on the “Related file” to download the zipped folder. When unzipped, click on the file named “index” to enter the website.

Interactive Processes among Babies at a Daycare Center

The paper presents a study regarding babies' interactive processes with peers, which aimed to apprehend some of their qualitative aspects, considering babies' peculiarities. An empirical work was conducted with video recording scenes and interviews, regarding the "Babies' Adaptation to a Daycare Center" project, which followed up 21 babies (4-13 months) at a daycare center. Data analysis was based on the Network of Meanings perspective. Five episodes are here presented regarding three focal subjects and their peers. Analysis indicates the occurrence of interactions; among them it can be highlighted the role of the glance, presence of triadic relations (even among babies younger than nine months old), abbreviation of communicative resources and empathy. Moreover, despite verbal language absence at this age, it was verified meaning processes. Some practical-theoretical implications are pointed out as well.

Interactive quadrangulation with reeb atlases and connectivity textures

Creating high-quality quad meshes from triangulated surfaces is a highly nontrivial task that necessitates consideration of various application specific metrics of quality. In our work, we follow the premise that automatic reconstruction techniques may not generate outputs meeting all the subjective quality expectations of the user. Instead, we put the user at the center of the process by providing a flexible, interactive approach to quadrangulation design. By combining scalar field topology and combinatorial connectivity techniques, we present a new framework, following a coarse to fine design philosophy, which allows for explicit control of the subjective quality criteria on the output quad mesh, at interactive rates. Our quadrangulation framework uses the new notion of Reeb atlas editing, to define with a small amount of interactions a coarse quadrangulation of the model, capturing the main features of the shape, with user prescribed extraordinary vertices and alignment. Fine grain tuning is easily achieved with the notion of connectivity texturing, which allows for additional extraordinary vertices specification and explicit feature alignment, to capture the high-frequency geometries. Experiments demonstrate the interactivity and flexibility of our approach, as well as its ability to generate quad meshes of arbitrary resolution with high-quality statistics, while meeting the user's own subjective requirements.

DNA-Interactive Properties of Crotamine, a Cell-Penetrating Polypeptide and a Potential Drug Carrier

Crotamine, a 42-residue polypeptide derived from the venom of the South American rattlesnake Crotalus durissus terrificus, has been shown to be a cell-penetrating protein that targets chromosomes, carries plasmid DNA into cells, and shows specificity for actively proliferating cells. Given this potential role as a nucleic acid-delivery vector, we have studied in detail the binding of crotamine to single- and double-stranded DNAs of different lengths and base compositions over a range of ionic conditions. Agarose gel electrophoresis and ultraviolet spectrophotometry analysis indicate that complexes of crotamine with long-chain DNAs readily aggregate and precipitate at low ionic strength. This aggregation, which may be important for cellular uptake of DNA, becomes less likely with shorter chain length. 25-mer oligonucleotides do not show any evidence of such aggregation, permitting the determination of affinities and size via fluorescence quenching experiments. The polypeptide binds non-cooperatively to DNA, covering about 5 nucleotide residues when it binds to single (ss) or (ds) double stranded molecules. The affinities of the protein for ss-vs. ds-DNA are comparable, and inversely proportional to salt levels. Analysis of the dependence of affinity on [NaCl] indicates that there are a maximum of,3 ionic interactions between the protein and DNA, with some of the binding affinity attributable to non-ionic interactions. Inspection of the three-dimensional structure of the protein suggests that residues 31 to 35, Arg-Trp-Arg-Trp-Lys, could serve as a potential DNA-binding site. A hexapeptide containing this sequence displayed a lower DNA binding affinity and salt dependence as compared to the full-length protein, likely indicative of a more suitable 3D structure and the presence of accessory binding sites in the native crotamine. Taken together, the data presented here describing crotamine-DNA interactions may lend support to the design of more effective nucleic acid drug delivery vehicles which take advantage of crotamine as a carrier with specificity for actively proliferating cells. Citation: Chen P-C, Hayashi MAF, Oliveira EB, Karpel RL (2012) DNA-Interactive Properties of Crotamine, a Cell-Penetrating Polypeptide and a Potential Drug Carrier. PLoS ONE 7(11): e48913. doi:10.1371/journal.pone.0048913

Growth hormone pharmacogenetics: the interactive effect of a microsatellite in the IGF1 promoter region with the GHR-exon 3 and-202 A/C IGFBP3 variants on treatment outcomes of children with severe GH deficiency

Insulin-like growth factor type 1 (IGF1) is a mediator of growth hormone (GH) action, and therefore, IGF1 is a candidate gene for recombinant human GH (rhGH) pharmacogenetics. Lower serum IGF1 levels were found in adults homozygous for 19 cytosine-adenosine (CA) repeats in the IGF1 promoter. The aim of this study was to evaluate the influence of (CA)n IGF1 polymorphism, alone or in combination with GH receptor (GHR)-exon 3 and -202 A/C insulin-like growth factor binding protein-3 (IGFBP3) polymorphisms, on the growth response to rhGH therapy in GH-deficient (GHD) patients. Eighty-four severe GHD patients were genotyped for (CA) n IGF1, -202 A/C IGFBP3 and GHR-exon 3 polymorphisms. Multiple linear regressions were performed to estimate the effect of each genotype, after adjustment for other influential factors. We assessed the influence of genotypes on the first year growth velocity (1st y GV) (n = 84) and adult height standard deviation score (SDS) adjusted for target-height SDS (AH-TH SDS) after rhGH therapy (n = 37). Homozygosity for the IGF1 19CA repeat allele was negatively correlated with 1st y GV (P = 0.03) and AH-TH SDS (P = 0.002) in multiple linear regression analysis. In conjunction with clinical factors, IGF1 and IGFBP3 genotypes explain 29% of the 1st y GV variability, whereas IGF1 and GHR polymorphisms explain 59% of final height-target-height SDS variability. We conclude that homozygosity for IGF1 (CA) 19 allele is associated with less favorable short-and long-term growth outcomes after rhGH treatment in patients with severe GHD. Furthermore, this polymorphism exhibits a non-additive interaction with -202 A/C IGFBP3 genotype on the 1st y GV and with GHR-exon 3 genotype on adult height. The Pharmacogenomics Journal (2012) 12, 439-445; doi:10.1038/tpj.2011.13; published online 5 April 2011

The Interactive Effect of GHR-Exon 3 and -202 A/C IGFBP3 Polymorphisms on rhGH Responsiveness and Treatment Outcomes in Patients with Turner Syndrome

Context: There is great interindividual variability in the response to recombinant human (rh) GH therapy in patients with Turner syndrome (TS). Ascertaining genetic factors can improve the accuracy of growth response predictions. Objective: The objective of the study was to assess the individual and combined influence of GHR-exon 3 and -202 A/C IGFBP3 polymorphisms on the short-and long-term outcomes of rhGH therapy in patients with TS. Design and Patients: GHR-exon 3 and -202 A/C IGFBP3 genotyping (rs2854744) was correlated with height data of 112 patients with TS who remained prepubertal during the first year of rhGH therapy and 65 patients who reached adult height after 5 +/- 2.5 yr of rhGH treatment. Main Outcome Measures: First-year growth velocity and adult height were measured. Results: Patients carrying at least one GHR-d3 or -202 A-IGFBP3 allele presented higher mean first-year growth velocity and achieved taller adult heights than those homozygous for GHR-fl or -202 C-IGFBP3 alleles, respectively. The combined analysis of GHR-exon 3 and -202 A/C IGFBP3 genotypes showed a clear nonadditive epistatic influence on adult height of patients with TS treated with rhGH (GHR-exon 3 alone, R-2 = 0.27; -202 A/C IGFBP3, R-2 = 0.24; the combined genotypes, R-2 = 0.37 at multiple linear regression). Together with clinical factors, these genotypes accounted for 61% of the variability in adult height of patients with TS after rhGH therapy. Conclusion: Homozygosity for the GHR-exon3 full-length allele and/or the -202C-IGFBP3 allele are associated with less favorable short-and long-term growth outcomes after rhGH treatment in patients with TS. (J Clin Endocrinol Metab 97: E671-E677, 2012)

Interactive application in spanish sign language for a public transport environment

[ES] En este trabajo se presenta el diseño de una herramienta multimedia que traduce a la lengua de signos españolas los mensajes de avisos que puede proporcionar un sistema de megafonía. El objetivo del trabajo es proporcionar una herramienta que mejore la inclusión social de las personas con discapacidades auditivas. Con este propósito, se han seleccionado el entorno y los mensajes de audio habituales en un aeropuerto para desarrollar este proyecto piloto. Por último, los audios se han traducido a lengua de signos españolas sintetizando un avatar usando la técnica de animación de rotoscopía a partir de la grabación en vídeo de un traductor. Los resultados finales han sido evaluados por personas sordas.

User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

Automatic initialization for facial analysis in interactive robotics

[EN]This paper focuses on four different initialization methods for determining the initial shape for the AAM algorithm and their particular performance in two different classification tasks with respect to either the facial expression DaFEx database and to the real world data obtained from a robot’s point of view.