Choose an application

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

The First CADE in the Third Millennium This volume contains the papers presented at the Eighteenth International C- ference on Automated Deduction (CADE-18) held on July 27–30th, 2002, at the University of Copenhagen as part of the Federated Logic Conference (FLoC 2002). Despite a large number of deduction-related conferences springing into existence at the end of the last millennium, the CADE conferences continue to be the major forum for the presentation of new research in all aspects of automated deduction. CADE-18 was sponsored by the Association for Auto- ted Reasoning, CADE Inc., the Department of Computer Science at Chalmers University, the Gesellschaft fur ¨ Informatik, Safelogic AB, and the University of Koblenz-Landau. There were 70 submissions, including 60 regular papers and 10 system - scriptions. Each submission was reviewed by at least ?ve program committee members and an electronic program committee meeting was held via the Int- net. The committee decided to accept 27 regular papers and 9 system descr- tions. One paper switched its category after refereeing, thus the total number of system descriptions in this volume is 10. In addition to the refereed papers, this volume contains an extended abstract of the CADE invited talk by Ian Horrocks, the joint CADE/CAV invited talk by Sharad Malik, and the joint CADE-TABLEAUX invited talk by Matthias Baaz. One more invited lecture was given by Daniel Jackson.

Automatic theorem proving --- Logic, Symbolic and mathematical --- Computer Science --- Mechanical Engineering - General --- Engineering & Applied Sciences --- Mechanical Engineering --- Computer science. --- Programming languages (Electronic computers). --- Computer logic. --- Mathematical logic. --- Artificial intelligence. --- Computer Science. --- Artificial Intelligence (incl. Robotics). --- Mathematical Logic and Formal Languages. --- Logics and Meanings of Programs. --- Programming Languages, Compilers, Interpreters. --- Logic design. --- Artificial Intelligence. --- Informatics --- Science --- 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 --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Switching theory --- Computer languages --- Computer program languages --- Computer programming languages --- Machine language --- Languages, Artificial --- Computer science logic --- Algebra of logic --- Logic, Universal --- Mathematical logic --- Symbolic and mathematical logic --- Symbolic logic --- Mathematics --- Algebra, Abstract --- Metamathematics --- Set theory --- Syllogism --- Automatic theorem proving - Congresses --- Logic, Symbolic and mathematical - Congresses

Choose an application

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

For the past 25 years the CADE conference has been the major forum for the presentation of new results in automated deduction. This volume contains the papers and system descriptions selected for the 17th International Conference on Automated Deduction, CADE-17, held June 17-20, 2000,at Carnegie Mellon University, Pittsburgh, Pennsylvania (USA). Fifty-three research papers and twenty system descriptions were submitted by researchers from ?fteen countries. Each submission was reviewed by at least three reviewers. Twenty-four research papers and ?fteen system descriptions were accepted. The accepted papers cover a variety of topics related to t- orem proving and its applications such as proof carrying code, cryptographic protocol veri?cation, model checking, cooperating decision procedures, program veri?cation, and resolution theorem proving. The program also included three invited lectures: “High-level veri?cation using theorem proving and formalized mathematics” by John Harrison, “Sc- able Knowledge Representation and Reasoning Systems” by Henry Kautz, and “Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice” by Carl Seger. Abstracts or full papers of these talks are included in this volume.In addition to the accepted papers, system descriptions, andinvited talks, this volumecontains one page summaries of four tutorials and ?ve workshops held in conjunction with CADE-17.

Automatic theorem proving --- Logic, Symbolic and mathematical --- Computer science. --- Computers. --- Computer logic. --- Mathematical logic. --- Artificial intelligence. --- Computer Science. --- Artificial Intelligence (incl. Robotics). --- Theory of Computation. --- Mathematical Logic and Formal Languages. --- Logics and Meanings of Programs. --- Mathematical Logic and Foundations. --- Information theory. --- Logic design. --- Logic, Symbolic and mathematical. --- Artificial Intelligence. --- Algebra of logic --- Logic, Universal --- Mathematical logic --- Symbolic and mathematical logic --- Symbolic logic --- Mathematics --- Algebra, Abstract --- Metamathematics --- Set theory --- Syllogism --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Machine theory --- Switching theory --- Informatics --- Science --- Communication theory --- Communication --- Cybernetics --- 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 --- Self-organizing systems --- Simulation methods --- Fifth generation computers --- Neural computers --- Computer science logic --- Automatic computers --- Automatic data processors --- Computer hardware --- Computing machines (Computers) --- Electronic calculating-machines --- Electronic computers --- Hardware, Computer --- Computer systems --- Calculators --- Cyberspace --- Automatic theorem proving - Congresses --- Logic, Symbolic and mathematical - Congresses

Choose an application

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

Artificial intelligence. --- Mathematical logic. --- Computer logic. --- Software engineering. --- Artificial Intelligence. --- Mathematical Logic and Formal Languages. --- Logics and Meanings of Programs. --- Software Engineering.

Choose an application

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

Artificial intelligence. --- Mathematical logic. --- Computer logic. --- Software engineering. --- Artificial Intelligence. --- Mathematical Logic and Formal Languages. --- Logics and Meanings of Programs. --- Software Engineering.

Choose an application

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

Automatic theorem proving --- Logic, Symbolic and mathematical --- Congresses.