Search

The Fifth International Conference on Automatic Differentiation held from August 11 to 15, 2008 in Bonn, Germany, is the most recent one in a series that began in Breckenridge, USA, in 1991 and continued in Santa Fe, USA, in 1996, Nice, France, in 2000 and Chicago, USA, in 2004. The 31 papers included in these proceedings re?ect the state of the art in automatic differentiation (AD) with respect to theory, applications, and tool development. Overall, 53 authors from institutions in 9 countries contributed, demonstrating the worldwide acceptance of AD technology in computational science. Recently it was shown that the problem underlying AD is indeed NP-hard, f- mally proving the inherently challenging nature of this technology. So, most likely, no deterministic “silver bullet” polynomial algorithm can be devised that delivers optimum performance for general codes. In this context, the exploitation of doma- speci?c structural information is a driving issue in advancing practical AD tool and algorithm development. This trend is prominently re?ected in many of the pub- cations in this volume, not only in a better understanding of the interplay of AD and certain mathematical paradigms, but in particular in the use of hierarchical AD approaches that judiciously employ general AD techniques in application-speci?c - gorithmic harnesses. In this context, the understanding of structures such as sparsity of derivatives, or generalizations of this concept like scarcity, plays a critical role, in particular for higher derivative computations.

Design reuse techniques have become the subject of books, conferences, and podium discussions over the last few years. However, most discussions focus on higher-level abstraction like RTL descriptions, which can be synthesized. Design reuse is often seen as an add-on to normal design activity, or a special design task that is not an integrated part of the existing design flow. This may all be true for the ASIC world, but not for high-speed, high-performance microprocessors. In the field of high-speed microprocessors, design reuse is an integrated part of the design flow. The method of choice in this demanding field was, and is always, physical design reuse at the layout level. In the past, the practical implementations of this method were linear shrinks and the lambda approach. With the scaling of process technology down to 0.18 micron and below, this approach lost steam and became inefficient. The only viable solution is a method, which is now called Automatic Layout Modification (ALM). It combines compaction, mask manipulation, and correction with powerful capabilities. Automatic Layout Modification, Including design reuse of the Alpha CPU in 0.13 micron SOI technology is a welcome effort to improving some of the practices in chip design today.

Worldwide there is a universal need for second language language learning. It is obvious that the computer can be a great help for this, especially when equipped with methods for automatically assessing the learner's pronunciation. While assessment of segmental pronunciation quality (i.,e. whether phones and words are pronounced correctly or not) is already available in commercial software packages, prosody (i.e. rhythm, word accent, etc.) is largely ignored---although it highly impacts intelligibility and listening effort. The present thesis contributes to closing this gap by developing and analyzing methods for automatically assessing the prosody of non-native speakers. We study the detection of word accent errors and the general assessment of the appropriateness of a speaker's rhythm. We propose a flexible, generic approach that is (a) very successful on these tasks, (b) competitive to other state-of-the-art result, and at the same time (c) flexible and easily adapted to new tasks.

Non-uniform random variate generation is an established research area in the intersection of mathematics, statistics and computer science. Although random variate generation with popular standard distributions have become part of every course on discrete event simulation and on Monte Carlo methods, the recent concept of universal (also called automatic or black-box) random variate generation can only be found dispersed in literature. This new concept has great practical advantages that are little known to most simulation practitioners. Being unique in its overall organization the book covers not only the mathematical and statistical theory, but also deals with the implementation of such methods. All algorithms introduced in the book are designed for practical use in simulation and have been coded and made available by the authors. Examples of possible applications of the presented algorithms (including option pricing, VaR and Bayesian statistics) are presented at the end of the book.

The evaluation of a logical formula can be viewed as a game played by two opponents, one trying to show that the formula is true and the other trying to prove it is false. This correspondence has been known for a very long time and has inspired numerous research directions. In this book, the author extends this connection between logic and games to the class of automatic structures, where relations are recognized by synchronous finite automata.In model-checking games for automatic structures, two coalitions play against each other with a particular kind of hierarchical imperfect information. The investigation of such games leads to the introduction of a game quantifier on automatic structures, which connects alternating automata with the classical model-theoretic notion of a game quantifier. This study is then extended, determining the memory needed for strategies in infinitary games on the one hand, and characterizing regularity-preserving Lindström quantifiers on the other. Counting quantifiers are investigated in depth: it is shown that all countable omega-automatic structures are in fact finite-word automatic and that the infinity and uncountability set quantifiers are definable in MSO over countable linear orders and over labeled binary trees.This book is based on the PhD thesis of Lukasz Kaiser, which was awarded with the E.W. Beth award for outstanding dissertations in the fields of logic, language, and information in 2009. The work constitutes an innovative study in the area of algorithmic model theory, demonstrating the deep interplay between logic and computability in automatic structures. It displays very high technical and presentational quality and originality, advances significantly the field of algorithmic model theory and raises interesting new questions, thus emerging as a fruitful and inspiring source for future research.

In this book, the design of two new planar patterns for camera calibration of intrinsic parameters is addressed and a line-based method for distortion correction is suggested. The dynamic calibration of structured light systems, which consist of a camera and a projector is also treated. Also, the 3D Euclidean reconstruction by using the image-to-world transformation is investigated. Lastly, linear calibration algorithms for the catadioptric camera are considered, and the homographic matrix and fundamental matrix are extensively studied. In these methods, analytic solutions are provided for the computational efficiency and redundancy in the data can be easily incorporated to improve reliability of the estimations. This volume will therefore prove valuable and practical tool for researchers and practioners working in image processing and computer vision and related subjects.

Automatic Quantum Computer Programming provides an introduction to quantum computing for non-physicists, as well as an introduction to genetic programming for non-computer-scientists. The book explores several ways in which genetic programming can support automatic quantum computer programming and presents detailed descriptions of specific techniques, along with several examples of their human-competitive performance on specific problems. Source code for the author's QGAME quantum computer simulator is included as an appendix, and pointers to additional online resources furnish the reader with an array of tools for automatic quantum computer programming.

Speech recognition technology is being increasingly employed in human-machine interfaces. A remaining problem however is the robustness of this technology to non-native accents, which still cause considerable difficulties for current systems.In this book, methods to overcome this problem are described. A speaker adaptation algorithm that is capable of adapting to the current speaker with just a few words of speaker-specific data based on the MLLR principle is developed and combined with confidence measures that focus on phone durations as well as on acoustic features. Furthermore, a specific pronunciation modelling technique that allows the automatic derivation of non-native pronunciations without using non-native data is described and combined with the previous techniques to produce a robust adaptation to non-native accents in an automatic speech recognition system.

ntil now there has been no state-of-the-art collection of themost important writings in automatic text summarization. This bookpresents the key developments in the field in an integrated frameworkand suggests future research areas.With the rapid growth of the World Wide Web and electronic information services, information is becoming available on-line at an incredible rate. One result is the oft-decried information overload. No one has time to read everything, yet we often have to make critical decisions based on what we are able to assimilate. The technology of automatic text summarization is becoming indispensable for dealing with this problem. Text summarization is the process of distilling the most important information from a source to produce an abridged version for a particular user or task. Until now there has been no state-of-the-art collection of the most important writings in automatic text summarization. This book presents the key developments in the field in an integrated framework and suggests future research areas. The book is organized into six sections: Classical Approaches, Corpus-Based Approaches, Exploiting Discourse Structure, Knowledge-Rich Approaches, Evaluation Methods, and New Summarization Problem Areas.ContributorsD. A. Adams, C. Aone, R. Barzilay, E. Bloedorn, B. Boguraev, R. Brandow, C. Buckley, F. Chen, M. J. Chrzanowski, H. P. Edmundson, M. Elhadad, T. Firmin, R. P. Futrelle, J. Gorlinsky, U. Hahn, E. Hovy, D. Jang, K. Sparck Jones, G. M. Kasper, C. Kennedy, K. Kukich, J. Kupiec, B. Larsen, W. G. Lehnert, C. Lin, H. P. Luhn, I. Mani, D. Marcu, M. Maybury, K. McKeown, A. Merlino, M. Mitra, K. Mitze, M. Moens, A. H. Morris, S. H. Myaeng, M. E. Okurowski, J. Pedersen, J. J. Pollock, D. R. Radev, G. J. Rath, L. F. Rau, U. Reimer, A. Resnick, J. Robin, G. Salton, T. R. Savage, A. Singhal, G. Stein, T. Strzalkowski, S. Teufel, J. Wang, B. Wise, A. Zamora

A common approach in software engineering is to apply during the design phase a variety of structured techniques like top-down design, decomposition and abstraction, while only subsequently, in the implementation phase, is the design tested to ensure reliability. But this approach neglects that central aspects of software design and program development have a strong formal character which admits tool support for the construction of reliable and correct computer systems based on formal reasoning. This monograph provides much information both for theoreticians interested in algebraic theories, and for software engineers building practically relevant tools. The author presents the theoretical foundations needed for the verification of reactive, sequential infinite-state systems.

This book describes a fundamentally new theoretical framework for finding poor algorithms in an application program and replacing them with ones that parallelize the code.Parallel computation will become the norm in the coming decades. Unfortunately, advances in parallel hardware have far outpaced parallel applications of software. There are currently two approaches to applying parallelism to applications. One is to write completely new applications in new languages. But abandoning applications that work is unacceptable to most nonacademic users of high-performance computers. The other approach is to convert existing applications to a parallel form. This can be done manually or automatically. Even partial success in doing the job automatically has obvious economic advantages. This book describes a fundamentally new theoretical framework for finding poor algorithms in an application program and replacing them with ones that parallelize the code.

This two-volume set of LNAI 14739-14740 constitute the proceedings of the 12th International Joint Conference on Automated Reasoning, IJCAR 2024, held in Nancy, France, during July 3-6, 2024. The 39 full research papers and 6 short papers presented in this book were carefully reviewed and selected from 115 submissions. The papers focus on the following topics: theorem proving and tools; SAT, SMT and Quantifier Elimination; Intuitionistic Logics and Modal Logics; Calculi, Proof Theory and Decision Procedures; and Unification, Rewriting and Computational Models. This book is open access.

Autonomous Experimentation is poised to revolutionize scientific experiments at advanced experimental facilities. Whereas previously, human experimenters were burdened with the laborious task of overseeing each measurement, recent advances in mathematics, machine learning and algorithms have alleviated this burden by enabling automated and intelligent decision-making, minimizing the need for human interference. Illustrating theoretical foundations and incorporating practitioners'first-hand experiences, this book is a practical guide to successful Autonomous Experimentation.Despite the field's growing potential, there exists numerous myths and misconceptions surrounding Autonomous Experimentation. Combining insights from theorists, machine-learning engineers and applied scientists, this book aims to lay the foundation for future research and widespread adoption within the scientific community. This book is particularly useful for members of the scientific community looking to improve their research methods but also contains additional insights for students and industry professionals interested in the future of the field.

This book focuses in detail on data science and data analysis and emphasizes the importance of data engineering and data management in the design of big data applications. The author uses patterns discovered in a collection of big data applications to provide design principles for hypothesis generation, integrating big data processing and management, machine learning and data mining techniques. The book proposes and explains innovative principles for interpreting hypotheses by integrating micro-explanations (those based on the explanation of analytical models and individual decisions within them) with macro-explanations (those based on applied processes and model generation). Practical case studies are used to demonstrate how hypothesis-generation and -interpretation technologies work. These are based on “social infrastructure” applications like in-bound tourism, disaster management, lunar and planetary exploration, and treatment of infectious diseases. The novel methods and technologies proposed in Hypothesis Generation and Interpretation are supported by the incorporation of historical perspectives on science and an emphasis on the origin and development of the ideas behind their design principles and patterns. Academic investigators and practitioners working on the further development and application of hypothesis generation and interpretation in big data computing, with backgrounds in data science and engineering, or the study of problem solving and scientific methods or who employ those ideas in fields like machine learning will find this book of considerable interest.

Network Optimization in Intelligent Internet of Things Applications: Principles and Challenges sheds light on the optimization methods that form the basis of effective communication between networked devices. It is an excellent resource as it provides readers with a thorough understanding of the methods, ideas, and tactics essential to attaining seamless connectivity and improving performance.This book presents the fundamental ideas that govern network optimization, from maximizing throughput and lowering latency to handling a variety of communication protocols and minimizing energy use. It also addresses scalability issues, security flaws, and constantly changing IoT environments along with optimization techniques.This book uses cutting-edge research and real-world examples to give readers the knowledge and skills to address the complex problems associated with network optimization in intelligent IoT applications. It also examines machine learning-driven predictive analytics, robust security protocols, flexible routing algorithms, and the integration of edge computing - all crucial instruments for overcoming obstacles and attaining peak performance.This book provides a comprehensive understanding of the principles, challenges, and cutting-edge solutions in IoT network optimization for all kinds of readers, whether it is students, academicians, researchers, or industry professionals. This book unleashes the potential of networked smart devices, which can be unleashed in various sectors.

This book provides a comprehensive presentation of a recently introduced framework, named'probabilistic indexing'(PrIx), for searching text in large collections of document images and other related applications. It fosters the development of new search engines for effective information retrieval from manuscripts which, however, lack the electronic text (transcripts) that would typically be required for such search and retrieval tasks. The book is structured into 11 chapters and three appendices. The first two chapters briefly outline the necessary fundamentals and state of the art in pattern recognition, statistical decision theory, and handwritten text recognition. Chapter 3 presents approaches for indexing (as opposed to “spotting”) each region of a handwritten text image which is likely to contain a word. Next, Chapter 4 describes models adopted for handwritten text in images, namely hidden Markov models, convolutional and recurrent neural networks and language models, and provides full details of weighted finite-state transducer (WFST) concepts and methods, needed in further chapters of the book. Chapter 5 explains the set of techniques and algorithms developed to generate image probabilistic indexes which allow for fast search and retrieval of textual information in the indexed images. Chapter 6 then presents experimental evaluations of the proposed framework and algorithms on different traditional benchmark datasets and compares them with other approaches, while Chapter 7 reviews the most popular keyword-spotting approaches. Chapter 8 explains how PrIx can support classical free-text search tools, while Chapter 9 presents new methods that use PrIx not only for searching, but also to deal with text analytics and other related natural language processing and information extraction tasks. Chapter 10 shows how the proposed solutions can be used to effectively index very large collections of handwritten document images, before Chapter 11 eventually summarizes the book and suggests promising lines of future research. The appendices detail the necessary mathematical foundations for the work and presents details of the text image collections and datasets used in the experiments throughout the book. This book is written for researchers and (post-)graduate students in pattern recognition and information retrieval. It will also be of interest to people in areas like history, criminology, or psychology who need technical support to evaluate, understand or decode historical or contemporary handwritten text.

This open access book constitutes the proceedings of the 29th International Conference on Automated Deduction, CADE 29, which took place in Rome, Italy, during July 2023. The 28 full papers and 5 short papers presented were carefully reviewed and selected from 77 submissions. CADE is the major forum for the presentation of research in all aspects of automated deduction, including foundations, applications, implementations, and practical experience. The papers are organized in the following topics: Logical foundations; theory and principles; implementation and application; ATP and AI; and system descriptions.

This open access book constitutes the proceedings of the proceedings of the 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023, held in Prague, Czech Republic, during September 18-21, 2023. The 20 full papers and 5 short papers included in this book together with 5 abstracts of invited talks were carefully reviewed and selected from 43 submissions. They present research on all aspects of the mechanization of reasoning with tableaux and related methods. The papers are organized in the following topical sections: tableau calculi; sequent calculi; theorem proving; non-wellfounded proofs; modal logics; linear logic and MV-algebras; separation logic; and first-order logics.

This book introduces embedded software engineering and management methods, proposing the relevant testing theory and techniques that promise the final realization of automated testing of embedded systems. The quality and reliability of embedded systems have become a great concern, faced with the rising demands for the complexity and scale of system hardware and software. The authors propose and expound on the testing theory and techniques of embedded software systems and relevant environment construction technologies, providing effective solutions for the automated testing of embedded systems. Through analyzing typical testing examples of the complex embedded software systems, the authors verify the effectiveness of the theories, technologies and methods proposed in the book. In combining the fundamental theory and technology and practical solutions, this book will appeal to researchers and students studying computer science, software engineering, and embedded systems, as well as professionals and practitioners engaged in the development, verification, and maintenance of embedded systems in the military and civilian fields.

This book uses automotive embedded systems as an example to introduce functional safety assurance and safety-aware cost optimization. The book explores functional safety assurance from the perspectives of verification, enhancement, and validation. The functional safety assurance methods implement a safe and efficient assurance system that integrates safety verification, enhancement, and validation. The assurance methods offered in this book could provide a reasonable and scientific theoretical basis for the subsequent formulation of automotive functional safety standards. The safety-aware cost optimization methods divide cost types according to the essential differences of various costs in system design and establish reasonable models based on different costs. The cost optimization methods provided in this book could give appropriate cost optimization solutions for the cost-sensitive automotive industry, thereby achieving effective cost management and control. Functional safety assurance methods and safety-aware cost optimization support each other and jointly build the architecture of functional safety design methodologies for automotive embedded systems. The work aspires to provide a relevant reference for students, researchers, engineers, and professionals working in this area or those interested in hardware cost optimization and development cost optimization design methods based on ensuring functional safety in general.

This volume, LNAI 13385, constitutes the refereed proceedings of the 11th International Joint Conference on Automated Reasoning, IJCAR 2022, held in Haifa, Israel, in August 2022. The 32 full research papers and 9 short papers presented together with two invited talks were carefully reviewed and selected from 85 submissions. The papers focus on the following topics: Satisfiability, SMT Solving,Arithmetic; Calculi and Orderings; Knowledge Representation and Jutsification; Choices, Invariance, Substitutions and Formalization; Modal Logics; Proofs System and Proofs Search; Evolution, Termination and Decision Prolems.This is an open access book.

Artificial Intelligence (AI) is undoubtedly playing an increasingly significant role in automobile technology. In fact, cars inhabit one of just a few domains where you will find many AI innovations packed into a single product.AI for Cars provides a brief guided tour through many different AI landscapes including robotics, image and speech processing, recommender systems and onto deep learning, all within the automobile world. From pedestrian detection to driver monitoring to recommendation engines, the book discusses the background, research and progress thousands of talented engineers and researchers have achieved thus far, and their plans to deploy this life-saving technology all over the world.

This open access book constitutes the proceeding of the 28th International Conference on Automated Deduction, CADE 28, held virtually in July 2021.The 29 full papers and 7 system descriptions presented together with 2 invited papers were carefully reviewed and selected from 76 submissions. CADE is the major forum for the presentation of research in all aspects of automated deduction, including foundations, applications, implementations, and practical experience. The papers are organized in the following topics: Logical foundations; theory and principles; implementation and application; ATP and AI; and system descriptions.

This book provides an overview of the basic concepts and components of UAVs, the various sensors used, architecture of autonomous UAVs, communication tools and devices to acquire real-time data from UAVs, the software needed to analyze the UAV data, required rules and regulations to fly UAVs, various application areas, and future areas of research which is needed to handle relevant challenges. FEATURES:Explores the utilization of UAVs in different application areas, such as construction, oil and gas, mining, agriculture, forestry, search and rescue, surveillance, transportation, disaster, logistics, health, journalism, and many moreCovers the theory, hardware, and software components of UAVsIncludes end of chapter review questions for better understanding of the subject matter.

Computers that `program themselves'has long been an aim of computer scientists. Recently genetic programming (GP) has started to show its promise by automatically evolving programs. Indeed in a small number of problems GP has evolved programs whose performance is similar to or even slightly better than that of programs written by people. The main thrust of GP has been to automatically create functions. While these can be of great use they contain no memory and relatively little work has addressed automatic creation of program code including stored data. This issue is the main focus of Genetic Programming, and Data Structures: Genetic Programming + Data Structures = Automatic Programming!. This book is motivated by the observation from software engineering that data abstraction (e.g., via abstract data types) is essential in programs created by human programmers. This book shows that abstract data types can be similarly beneficial to the automatic production of programs using GP. Genetic Programming and Data Structures: Genetic Programming + Data Structures = Automatic Programming! shows how abstract data types (stacks, queues and lists) can be evolved using genetic programming, demonstrates how GP can evolve general programs which solve the nested brackets problem, recognises a Dyck context free language, and implements a simple four function calculator. In these cases, an appropriate data structure is beneficial compared to simple indexed memory. This book also includes a survey of GP, with a critical review of experiments with evolving memory, and reports investigations of real world electrical network maintenance scheduling problems that demonstrate that Genetic Algorithms can find low cost viable solutions to such problems. Genetic Programming and Data Structures: Genetic Programming + Data Structures = Automatic Programming! should be of direct interest to computer scientists doing research on genetic programming, genetic algorithms, data structures, and artificial intelligence. In addition, this book will be of interest to practitioners working in all of these areas and to those interested in automatic programming.

There are many myths and mistakes which make the topics of artificial intelligence complex and confusing. But the truth is that the foundations of AI are not rocket science. People do not need a PhD to understand how a basic neural network works. In fact, one does not even need computer skills to learn this.Cunning Machines: Your Pocket Guide to the World of Artificial Intelligence explains the main concepts: what does AI really mean, where do we find it, how do scientists try to evaluate it, what are its main limitations and what future we can expect with it? It also describes the most popular AI techniques in an easy-to-digest form: Artificial neural networks Genetic algorithms The Monte Carlo method Natural language processing Ontologies and their applications This book is for everyone. Still, it may be especially valuable to teachers who wish to enrich their classes with some interesting and popular topics, sales managers and business analysts who wish to better understand the IT world, and finally politicians and journalists who take part in debates on the latest technologies.Jędrzej Osiński earned a PhD in artificial intelligence, has worked on government grants and has published 14 scientific papers to date. He is also the co-author of two books. At the same time, he has over ten years of experience working in IT companies of different sizes, domains (the web, telecoms, banking, e-learning), organisation structures and locations (Poland, Ireland and the UK). He is also involved in various initiatives promoting AI, science and modern technologies including blog posts, invited talks and TV and radio appearances

This book aims to teach the core concepts that make Self-driving vehicles (SDVs) possible. It is aimed at people who want to get their teeth into self-driving vehicle technology, by providing genuine technical insights where other books just skim the surface. The book tackles everything from sensors and perception to functional safety and cybersecurity. It also passes on some practical know-how and discusses concrete SDV applications, along with a discussion of where this technology is heading. It will serve as a good starting point for software developers or professional engineers who are eager to pursue a career in this exciting field and want to learn more about the basics of SDV algorithms. Likewise, academic researchers, technology enthusiasts, and journalists will also find the book useful.Key Features: Offers a comprehensive technological walk-through of what really matters in SDV development: from hardware, software, to functional safety and cybersecurity Written by an active practitioner with extensive experience in series development and research in the fields of Advanced Driver Assistance Systems (ADAS) and Autonomous Driving Covers theoretical fundamentals of state-of-the-art SLAM, multi-sensor data fusion, and other SDV algorithms. Includes practical information and hands-on material with Robot Operating System (ROS) and Open Source Car Control (OSCC). Provides an overview of the strategies, trends, and applications which companies are pursuing in this field at present as well as other technical insights from the industry.

An essential introduction to the analysis and verification of control system softwareThe verification of control system software is critical to a host of technologies and industries, from aeronautics and medical technology to the cars we drive. The failure of controller software can cost people their lives. In this authoritative and accessible book, Pierre-Loïc Garoche provides control engineers and computer scientists with an indispensable introduction to the formal techniques for analyzing and verifying this important class of software.Too often, control engineers are unaware of the issues surrounding the verification of software, while computer scientists tend to be unfamiliar with the specificities of controller software. Garoche provides a unified approach that is geared to graduate students in both fields, covering formal verification methods as well as the design and verification of controllers. He presents a wealth of new verification techniques for performing exhaustive analysis of controller software. These include new means to compute nonlinear invariants, the use of convex optimization tools, and methods for dealing with numerical imprecisions such as floating point computations occurring in the analyzed software.As the autonomy of critical systems continues to increase—as evidenced by autonomous cars, drones, and satellites and landers—the numerical functions in these systems are growing ever more advanced. The techniques presented here are essential to support the formal analysis of the controller software being used in these new and emerging technologies.

The widespread use of bankchecks in daily life makes the development of check-reading systems of fundamental relevance to banks and other financial institutions. This will improve productivity and allow advanced customer services. Therefore, many industrial companies and academic research laboratories have recently been attracted to this field, which involves several aspects, like image acquisition and preprocessing, layout analysis, preprinted data identification and recognition, user-entered data extraction, recognition of handwritten characters and words, and signature verification.The contributions collected in this book present the state of the art in the field of complete systems for bankcheck recognition, and explore the most promising trends in key aspects of this research field.

Research on artificial life is critical to solving various dynamic obstacles individuals face on a daily basis. From electric wheelchairs to navigation, artificial life can play a role in improving both the simple and complex aspects of civilian life. The Handbook of Research on Investigations in Artificial Life Research and Development is a vital scholarly reference source that examines emergent research in handling real-world problems through the application of various computation technologies and techniques. Examining topics such as computational intelligence, multi-agent systems, and fuzzy logic, this publication is a valuable resource for academicians, scientists, researchers, and individuals interested in artificial intelligence developments.

This book constitutes the proceedings of the 24th International Conference on Automated Deduction, CADE-24, held in Lake Placid, NY, USA, in June 2013. The 31 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 71 initial submissions. CADE is the major forum for the presentation of research in all aspects of automated deduction, ranging from theoretical and methodological issues to the presentation of new theorem provers, solvers and systems.

Grammatical Evolution: Evolutionary Automatic Programming in an Arbitrary Language provides the first comprehensive introduction to Grammatical Evolution, a novel approach to Genetic Programming that adopts principles from molecular biology in a simple and useful manner, coupled with the use of grammars to specify legal structures in a search. Grammatical Evolution's rich modularity gives a unique flexibility, making it possible to use alternative search strategies - whether evolutionary, deterministic or some other approach - and to even radically change its behavior by merely changing the grammar supplied. This approach to Genetic Programming represents a powerful new weapon in the Machine Learning toolkit that can be applied to a diverse set of problem domains.

In the mathematical description of a physical or biological process, it is a common practice \0 assume that the future behavior of Ihe process considered depends only on the present slate, and therefore can be described by a finite sct of ordinary diffe­ rential equations. This is satisfactory for a large class of practical systems. However. the existence of lime-delay elements, such as material or infonnation transport, of­ tcn renders such description unsatisfactory in accounting for important behaviors of many practical systems. Indeed. due largely to the current lack of effective metho­ dology for analysis and control design for such systems, the lime-delay elements arc often either neglected or poorly approximated, which frequently results in analysis and simulation of insufficient accuracy, which in turns leads to poor performance of the systems designed. Indeed, it has been demonstrated in the area of automatic control that a relatively small delay may lead to instability or significantly deteriora­ ted perfonnances for the corresponding closed-loop systems.

This book constitutes the thoroughly refereed proceedings of the Third International Conference on Interactive Theorem Proving, ITP 2012, held in Princeton, NJ, USA, in August 2012. The 21 revised full papers presented together with 4 rough diamond papers, 3 invited talks, and one invited tutorial were carefully reviewed and selected from 40 submissions. Among the topics covered are formalization of mathematics; program abstraction and logics; data structures and synthesis; security; (non-)termination and automata; program verification; theorem prover development; reasoning about program execution; and prover infrastructure and modeling styles.

Intelligent Unmanned Ground Vehicles describes the technology developed and the results obtained by the Carnegie Mellon Robotics Institute in the course of the DARPA Unmanned Ground Vehicle (UGV) project. The goal of this work was to equip off-road vehicles with computer-controlled, unmanned driving capabilities. The book describes contributions in the area of mobility for UGVs including: tools for assembling complex autonomous mobility systems; on-road and off-road navigation; sensing techniques; and route planning algorithms. In addition to basic mobility technology, the book covers a number of integrated systems demonstrated in the field in realistic scenarios. The approaches presented in this book can be applied to a wide range of mobile robotics applications, from automated passenger cars to planetary exploration, and construction and agricultural machines. Intelligent Unmanned Ground Vehicles shows the progress that was achieved during this program, from brittle specially-built robots operating under highly constrained conditions, to groups of modified commercial vehicles operating in tough environments. One measure of progress is how much of this technology is being used in other applications. For example, much of the work in road-following, architectures and obstacle detection has been the basis for the Automated Highway Systems (AHS) prototypes currently under development. AHS will lead to commercial prototypes within a few years. The cross-country technology is also being used in the development of planetary rovers with a projected launch date within a few years. The architectural tools built under this program have been used in numerous applications, from an automated harvester to an autonomous excavator. The results reported in this work provide tools for further research development leading to practical, reliable and economical mobile robots.

The idea of mechanizing deductive reasoning can be traced all the way back to Leibniz, who proposed the development of a rational calculus for this purpose. But it was not until the appearance of Frege's 1879 Begriffsschrift-'not only the direct ancestor of contemporary systems of mathematical logic, but also the ancestor of all formal languages, including computer programming languages'([Dav83])-that the fundamental concepts of modern mathematical logic were developed. Whitehead and Russell showed in their Principia Mathematica that the entirety of classical mathematics can be developed within the framework of a formal calculus, and in 1930, Skolem, Herbrand, and Godel demonstrated that the first-order predicate calculus (which is such a calculus) is complete, i. e., that every valid formula in the language of the predicate calculus is derivable from its axioms. Skolem, Herbrand, and GOdel further proved that in order to mechanize reasoning within the predicate calculus, it suffices to Herbrand consider only interpretations of formulae over their associated universes. We will see that the upshot of this discovery is that the validity of a formula in the predicate calculus can be deduced from the structure of its constituents, so that a machine might perform the logical inferences required to determine its validity. With the advent of computers in the 1950s there developed an interest in automatic theorem proving.

Safety of Computer Control Systems 1985 (Safecomp'85): Achieving Safe Real Time Computer Systems presents the proceedings of the Fourth IFAC Workshop, held in Como, Italy, on October 1–3, 1985. This book discusses a wide range of topics ranging from direct process control through robotics to operator assistance. Organized into 28 chapters, this compilation of papers begins with an overview of the implementation of atomic actions by means of concurrent programming constructs. This text then examines the safety-related applications that usually demand the provision of redundant resources within the system. Other chapters consider the safe performance of an industrial robot system that relies on several factors. This book discusses as well the increasing demand for Computer Assisted Decision Making (CADM) both in engineering and service industries. The final chapter deals with the ways of reducing the effects of an error introduced during the design of a program. This book is a valuable resource for software engineers.

The problem of privacy-preserving data analysis has a long history spanning multiple disciplines. As electronic data about individuals becomes increasingly detailed, and as technology enables ever more powerful collection and curation of these data, the need increases for a robust, meaningful, and mathematically rigorous definition of privacy, together with a computationally rich class of algorithms that satisfy this definition. Differential Privacy is such a definition. The Algorithmic Foundations of Differential Privacy starts out by motivating and discussing the meaning of differential privacy, and proceeds to explore the fundamental techniques for achieving differential privacy, and the application of these techniques in creative combinations, using the query-release problem as an ongoing example. A key point is that, by rethinking the computational goal, one can often obtain far better results than would be achieved by methodically replacing each step of a non-private computation with a differentially private implementation. Despite some powerful computational results, there are still fundamental limitations. Virtually all the algorithms discussed herein maintain differential privacy against adversaries of arbitrary computational power — certain algorithms are computationally intensive, others are efficient. Computational complexity for the adversary and the algorithm are both discussed. The monograph then turns from fundamentals to applications other than query-release, discussing differentially private methods for mechanism design and machine learning. The vast majority of the literature on differentially private algorithms considers a single, static, database that is subject to many analyses. Differential privacy in other models, including distributed databases and computations on data streams, is discussed. The Algorithmic Foundations of Differential Privacy is meant as a thorough introduction to the problems and techniques of differential privacy, and is an invaluable reference for anyone with an interest in the topic.

Advanced space exploration is performed by unmanned missions with integrated autonomy in both flight and ground systems. Risk and feasibility are major factors supporting the use of unmanned craft and the use of automation and robotic technologies where possible. Autonomy in space helps to increase the amount of science data returned from missions, perform new science, and reduce mission costs.Elicitation and expression of autonomy requirements is one of the most significant challenges the autonomous spacecraft engineers need to overcome today. This book discusses the Autonomy Requirements Engineering (ARE) approach, intended to help software engineers properly elicit, express, verify, and validate autonomy requirements. Moreover, a comprehensive state-of-the-art of software engineering for aerospace is presented to outline the problems handled by ARE along with a proof-of-concept case study on the ESA's BepiColombo Mission demonstrating the ARE's ability to handle autonomy requirements.

This book constitutes the refereed proceedings of the 22nd International Conference on Automated Deduction, CADE-22, held in Montreal, Canada, in August 2009. The 27 revised full papers and 5 system descriptions presented were carefully reviewed and selected from 77 submissions. Furthermore, three invited lectures by distinguished experts in the area were included. The papers are organized in topical sections on combinations and extensions, minimal unsatisfiability and automated reasoning support, system descriptions, interpolation and predicate abstraction, resolution-based systems for non-classical logics, termination analysis and constraint solving, rewriting, termination and productivity, models, modal tableaux with global caching, arithmetic.

This volume contains the research papers presented at the International C- ference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009) held July 6-10, 2009 in Oslo, Norway. This conference was the 18th in a series of international meetings since 1992 (listed on page IX). It was collocated with FTP 2009, the Workshop on First-Order Theorem Proving. The Program Committee of TABLEAUX 2009 received 44 submissions from 24 countries. Each paper was reviewed by at least three referees, after which the reviews were sent to the authors for comment in a rebuttal phase. After a?nal intensive discussion on the borderline papers during the online meeting of the Program Committee, 21 research papers and 1 system description were accepted based on originality, technical soundness, presentation, and relevance. Additionally,three positionpaperswereaccepted,whicharepublished asate- nical report of the University of Oslo. We wish to sincerely thank all the authors who submitted their work for consideration. And we would like to thank the Program Committee members and other referees for their great e?ort and p- fessional work in the review and selection process. Their names are listed on the following pages.

Today, people use a large number of'systems'ranging in complexity from washing machines to international airline reservation systems. Computers are used in nearly all such systems: accuracy and security are becoming increasingly essential. The design of such computer systems should make use of development methods as systematic as those used in other engineering disciplines. A systematic development method must provide a way of writing specifications which are both precise and concise; it must also supply a way of relating design to specification. A concise specification can be achieved by restricting attention to what a system has to do: all considerations of implementation details are postponed. With computer systems, this is done by: 1) building an abstract model of the system -operations being specified by pre-and post-conditions; 2) defining languages by mapping program texts onto some collection of objects modelizing the concepts of the system to be dealt with, whose meaning is understood; 3) defining complex data objects in terms of abstractions known from mathematics. This last topic, the use of abstract data types, pervades all work on specifications and is necessary in order to apply ideas to systems of significant complexity. The use of mathematics based notations is the best way to achieve precision. 1.1 ABSTRACT DATA TYPES, PROOF TECHNIQUES From a practical point of view, a solution to these three problems consists to introduce abstract data types in the programming languages, and to consider formal proof methods.

The papers in this volume were presented at the First International Workshop on Larch, held at MIT Endicott House near Boston on 13-15 July 1992. Larch is a family of formal specification languages and tools, and this workshop was a forum for those who have designed the Larch languages, built tool support for them, particularly the Larch Prover, and used them to specify and reason about software and hardware systems. The Larch Project started in 1980, led by John Guttag at MIT and James Horning, then at Xerox/Palo Alto Research Center and now at Digital Equipment Corporation/Systems Research Center (DEC/SRC). Major applications have included VLSI circuit synthesis, medical device communications, compiler development and concurrent systems based on Lamport's TLA, as well as several applications to classical theorem proving and algebraic specification. Larch supports a two-tiered approach to specifying software and hardware modules. One tier of a specification is wrillen in the Larch Shared Language (LSL). An LSL specification describes mathematical abstractions such as sets, relations, and algebras; its semantics is defined in terms of first-order theories. The second tier is written in a Larch interface language, one designed for a specific programming language. An interface specification describes the effects of individual modules, e.g. state changes, resource allocation, and exceptions; its semantics is defined in terms of first-order predicates over two states, where state is defined in terms of the programming language's notion of state. Thus, LSL is programming language independent; a Larch interface language is programming language dependent.

This book constitutes the refereed proceedings of the 4th International Conference on Interactive Theorem Proving, ITP 2013, held in Rennes, France, in July 2013. The 26 regular full papers presented together with 7 rough diamond papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 66 submissions. The papers are organized in topical sections such as program verfication, security, formalization of mathematics and theorem prover development.

Coq is an interactive proof assistant for the development of mathematical theories and formally certified software. It is based on a theory called the calculus of inductive constructions, a variant of type theory. This book provides a pragmatic introduction to the development of proofs and certified programs using Coq. With its large collection of examples and exercises it is an invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-fault software.

System Modelling and Optimization covers research issues within systems theory, optimization, modelling, and computing. It includes contributions to structural mechanics, integer programming, nonlinear programming, interior point methods, dynamical systems, stability analysis, stochastic optimization, bilevel optimization, and semidefinite programming. Several survey papers written by leading experts in their fields complement new developments in theory and applications. This book contains most of the invited papers and a few carefully selected submitted papers that were presented at the 19th IFIP TC7 Conference on System Modelling and Optimization, which was held in Cambridge, England, from July 12 to 16, 1999, and sponsored by the International Federation for Information Processing (IFIP).

The History of the Book In August 1992 the author had the opportunity to give a course on resolution theorem proving at the Summer School for Logic, Language, and Information in Essex. The challenge of this course (a total of five two-hour lectures) con­ sisted in the selection of the topics to be presented. Clearly the first selection has already been made by calling the course'resolution theorem proving'instead of'automated deduction'. In the latter discipline a remarkable body of knowledge has been created during the last 35 years, which hardly can be presented exhaustively, deeply and uniformly at the same time. In this situ­ ation one has to make a choice between a survey and a detailed presentation with a more limited scope. The author decided for the second alternative, but does not suggest that the other is less valuable. Today resolution is only one among several calculi in computational logic and automated reasoning. How­ ever, this does not imply that resolution is no longer up to date or its potential exhausted. Indeed the loss of the'monopoly'is compensated by new appli­ cations and new points of view. It was the purpose of the course mentioned above to present such new developments of resolution theory. Thus besides the traditional topics of completeness of refinements and redundancy, aspects of termination (resolution decision procedures) and of complexity are treated on an equal basis.

There are many kinds of books on formal logic. Some have philosophers as their intended audience, some mathematicians, some computer scientists. Although there is a common core to all such books they will be very dif­ ferent in emphasis, methods, and even appearance. This book is intended for computer scientists. But even this is not precise. Within computer sci­ ence formal logic turns up in a number of areas, from program verification to logic programming to artificial intelligence. This book is intended for computer scientists interested in automated theorem proving in classical logic. To be more precise yet, it is essentially a theoretical treatment, not a how-to book, although how-to issues are not neglected. This does not mean, of course, that the book will be of no interest to philosophers or mathematicians. It does contain a thorough presentation of formal logic and many proof techniques, and as such it contains all the material one would expect to find in a course in formal logic covering completeness but not incompleteness issues. The first item to be addressed is, what are we talking about and why are we interested in it. We are primarily talking about truth as used in mathematical discourse, and our interest in it is, or should be, self-evident. Truth is a semantic concept, so we begin with models and their properties. These are used to define our subject.