Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Commemorating the 50th anniversary of the first time a mathematical theorem was proven by a computer system, Freek Wiedijk initiated the present book in 2004 by inviting formalizations of a proof of the irrationality of the square root of two from scientists using various theorem proving systems. The 17 systems included in this volume are among the most relevant ones for the formalization of mathematics. The systems are showcased by presentation of the formalized proof and a description in the form of answers to a standard questionnaire. The 17 systems presented are HOL, Mizar, PVS, Coq, Otter/Ivy, Isabelle/Isar, Alfa/Agda, ACL2, PhoX, IMPS, Metamath, Theorema, Leog, Nuprl, Omega, B method, and Minlog.

Proof theory --- Algebra --- Algèbre --- Data processing. --- Computer programs. --- Logiciels --- Computer programs --- Computer Science --- Mechanical Engineering - General --- Engineering & Applied Sciences --- Mathematics --- Mechanical Engineering --- Physical Sciences & Mathematics --- Information Technology --- Artificial Intelligence --- Computer science. --- Software engineering. --- Mathematical logic. --- Artificial intelligence. --- Computer Science. --- Artificial Intelligence (incl. Robotics). --- Software Engineering. --- Mathematical Logic and Formal Languages. --- AI (Artificial intelligence) --- Artificial thinking --- Electronic brains --- Intellectronics --- Intelligence, Artificial --- Intelligent machines --- Machine intelligence --- Thinking, Artificial --- Bionics --- Cognitive science --- Digital computer simulation --- Electronic data processing --- Logic machines --- Machine theory --- Self-organizing systems --- Simulation methods --- Fifth generation computers --- Neural computers --- Algebra of logic --- Logic, Universal --- Mathematical logic --- Symbolic and mathematical logic --- Symbolic logic --- Algebra, Abstract --- Metamathematics --- Set theory --- Syllogism --- Computer software engineering --- Engineering --- Informatics --- Science --- Artificial Intelligence. --- Proof theory - Data processing --- Algebra - Computer programs

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

These proceedings contain a refereed selection of papers presented at the Second Annual Workshop of the Types Working Group (Computer-Assisted Reasoning based on Type Theory, EUIST project 29001), which was held April 24–28, 2002 in Hotel Erica, Berg en Dal (close to Nijmegen), The Netherlands. The workshop was attended by about 90 researchers. On April 27, there was a special afternoon celebrating the 60th birthday of Per Martin-L¨of, one of the founding fathers of the Types community. The afternoon consisted of the following three invited talks: “Constructive Validity Revisited” by Dana Scott, “From the Rules of Logic to the Logic of Rules” by Jean-Yves Girard, and “The Varieties of Type Theories” by Peter Aczel. The contents of these contributions were not laid down in these proceedings, but the videos of the talks and the slides used by the speakers are available at http://www. cs. kun. nl/fnds/MartinLoefDay/LoefTalks. htm The previous workshop of the Types Working Group under EUIST project 29001 was held in 2000 in Durham, UK. The workshops Types 2000 and Types 2002 followed a series of meetings organized in the period 1993 – 1999 whithin previous Types projects (ESPRIT BRA 6435 and ESPRIT Working Group 21900). The proceedings of these earlier Types workshops were also published in the LNCS series, as volumes 806, 996, 1158, 1512, 1657, 1956 and 2277. ESPRIT BRA 6453 was a continuation of ESPRIT Action 3245, Logical Frameworks: - sign, Implementation and Experiments.

Automatic theorem proving --- Computer programming --- Computer Science --- Engineering & Applied Sciences --- Computer science. --- Science. --- Software engineering. --- Programming languages (Electronic computers). --- Computers. --- Computer logic. --- Mathematical logic. --- Computer Science. --- Software Engineering/Programming and Operating Systems. --- Science, general. --- Theory of Computation. --- Logics and Meanings of Programs. --- Programming Languages, Compilers, Interpreters. --- Mathematical Logic and Formal Languages. --- Information theory. --- Logic design. --- Science, Humanities and Social Sciences, multidisciplinary. --- Informatics --- Science --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Machine theory --- Switching theory --- Communication theory --- Communication --- Cybernetics --- Computer software engineering --- Engineering --- Algebra of logic --- Logic, Universal --- Mathematical logic --- Symbolic and mathematical logic --- Symbolic logic --- Mathematics --- Algebra, Abstract --- Metamathematics --- Set theory --- Syllogism --- Computer languages --- Computer program languages --- Computer programming languages --- Machine language --- Electronic data processing --- Languages, Artificial --- Computer science logic --- Logic, Symbolic and mathematical --- Automatic computers --- Automatic data processors --- Computer hardware --- Computing machines (Computers) --- Electronic brains --- Electronic calculating-machines --- Electronic computers --- Hardware, Computer --- Computer systems --- Calculators --- Cyberspace --- Programming languages (Electronic computers) --- Logic, Symbolic and mathematical.

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Mathematical logic --- Logic --- Computer science --- Programming --- Artificial intelligence. Robotics. Simulation. Graphics --- Computer. Automation --- ontwerpen --- programmeren (informatica) --- programmeertalen --- wiskunde --- software engineering --- robots

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

This book constitutes the joint refereed proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2008, the 15th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2008, and the 7th International Conference on Mathematical Knowledge Management, MKM 2008, held in Birmingham, UK, in July/August as CICM 2008, the Conferences on Intelligent Computer Mathematics. The 14 revised full papers for AISC 2008, 10 revised full papers for Calculemus 2008, and 18 revised full papers for MKM 2008, plus 5 invited talks, were carefully reviewed and selected from a total of 81 submissions for a joint presentation in the book. The papers cover different aspects of traditional branches in CS such as computer algebra, theorem proving, and artificial intelligence in general, as well as newly emerging ones such as user interfaces, knowledge management, and theory exploration, thus facilitating the development of integrated mechanized mathematical assistants that will be routinely used by mathematicians, computer scientists, and engineers in their every-day business.

Mathematical logic --- Computer architecture. Operating systems --- Information systems --- Artificial intelligence. Robotics. Simulation. Graphics --- Computer. Automation --- algebra --- ICT (informatie- en communicatietechnieken) --- informatica --- informatiesystemen --- database management --- KI (kunstmatige intelligentie) --- computernetwerken --- robots --- numerieke analyse

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Mathematical logic --- Computer architecture. Operating systems --- Information systems --- Artificial intelligence. Robotics. Simulation. Graphics --- Computer. Automation --- algebra --- ICT (informatie- en communicatietechnieken) --- informatica --- informatiesystemen --- database management --- KI (kunstmatige intelligentie) --- computernetwerken --- robots --- numerieke analyse --- AI (artificiële intelligentie)