The technology of mechanized program verification can play a supporting role in many kinds of research projects in computer science, and related tools for formal proof-checking are seeing increasing adoption in mathematics and engineering. This book provides an introduction to the Coq software for writing and checking mathematical proofs. It takes a practical engineering focus throughout, emphasizing techniques that will help users to build, understand, and maintain large Coq developments and minimize the cost of code change over time.

Many books explain what is known about the universe. This book investigates what cannot be known. Rather than exploring the amazing facts that science, mathematics, and reason have revealed to us, this work studies what science, mathematics, and reason tell us cannot be revealed. In The Outer Limits of Reason, Noson Yanofsky considers what cannot be predicted, described, or known, and what will never be understood. He discusses the limitations of computers, physics, logic, and our own thought processes.

In the 1930s a series of seminal works published by Alan Turing, Kurt GÃ¶del, Alonzo Church, and others established the theoretical basis for computability. This work, advancing precise characterizations of effective, algorithmic computability, was the culmination of intensive investigations into the foundations of mathematics. In the decades since, the theory of computability has moved to the center of discussions in philosophy, computer science, and cognitive science.

Have you ever wondered how your GPS can find the fastest way to your destination, selecting one route from seemingly countless possibilities in mere seconds? How your credit card account number is protected when you make a purchase over the Internet? The answer is algorithms. And how do these mathematical formulations translate themselves into your GPS, your laptop, or your smart phone? This book offers an engagingly written guide to the basics of computer algorithms.

In this groundbreaking study, first published in 1983 and unavailable for over a decade, Linda Dalrymple Henderson demonstrates that two concepts of space beyond immediate perception—the curved spaces of non-Euclidean geometry and, most important, a higher, fourth dimension of space—were central to the development of modern art. The possibility of a spatial fourth dimension suggested that our world might be merely a shadow or section of a higher dimensional existence.

The classical view of concepts in psychology was challenged in the 1970s when experimental evidence showed that concept categories are graded and thus cannot be represented adequately by classical sets. The possibility of using fuzzy set theory and fuzzy logic for representing and dealing with concepts was recognized initially but then virtually abandoned in the early 1980s. In this volume, leading researchers--both psychologists working on concepts and mathematicians working on fuzzy logic--reassess the usefulness of fuzzy logic for the psychology of concepts.

“Mathematics can be as effortless as humming a tune, if you know the tune,” writes Gareth Loy. In Musimathics, Loy teaches us the tune, providing a friendly and spirited tour of the mathematics of music--a commonsense, self-contained introduction for the nonspecialist reader. It is designed for musicians who find their art increasingly mediated by technology, and for anyone who is interested in the intersection of art and science.

Volume 2 of Musimathics continues the story of music engineering begun in volume 1, focusing on the digital and computational domain. Loy goes deeper into the mathematics of music and sound, beginning with digital audio, sampling, and binary numbers, as well as complex numbers and how they simplify representation of musical signals. Chapters cover the Fourier transform, convolution, filtering, resonance, the wave equation, acoustical systems, sound synthesis, the short-time Fourier transform, and the wavelet transform.

In problem solving, as in street fighting, rules are for fools: do whatever works—don't just stand there! Yet we often fear an unjustified leap even though it may land us on a correct result. Traditional mathematics teaching is largely about solving exactly stated problems exactly, yet life often hands us partly defined problems needing only moderately accurate solutions. This engaging book is an antidote to the rigor mortis brought on by too much mathematical rigor, teaching us how to guess answers without needing a proof or an exact calculation.