Conference on Automated Deduction

Last updated

The Conference on Automated Deduction (CADE) is the premier academic conference on automated deduction and related fields. [1] The first CADE was organized in 1974 at the Argonne National Laboratory near Chicago. Most CADE meetings have been held in Europe and the United States. However, conferences have been held all over the world. Since 1996, CADE has been held yearly. In 2001, CADE was, for the first time, merged into the International Joint Conference on Automated Reasoning (IJCAR). [2] This has been repeated biannually since 2004. [3]

In 1996, CADE Inc. was formed as a non-profit sub-corporation of the Association for Automated Reasoning to organize the formerly individually organized conferences.

NrProceedingsDateYearLocationEditor(s)
LNAI
011975
021976
031977
041979
0500871980 Les Arcs, France Wolfgang Bibel, Robert Kowalski
0601381982New York, USA Donald W. Loveland
070170May 14–161984Napa, California, USA Robert Shostak
080230Jul 27 – Aug 11986Oxford, EnglandJörg H. Siekmann
090310May 23–261988Argonne, Illinois, USAE. Lusk, Ross A. Overbeek
1004491990Kaiserslautern, Germany Mark Stickel
110607Jun 15–181992Saratoga Springs, USAD. Kapur
120814Jun 26 – Jul 11994Nancy, France Alan Bundy
131104Jul 30 – Aug 31996New Brunswick, NJ, USA Michael A. McRobbie, J.K. Slaney
141249Jul 13–171997Townsville, North Queensland, Australia William McCune
151421Jul 5–101998Lindau, GermanyClaude Kirchner, Hélène Kirchner
161632Jul 7–101999Trento, Italy Harald Ganzinger
171831Jun 17–202000Pittsburgh, PA, USA David A. McAllester
182392Jul 27–302002Copenhagen, Denmark Andrei Voronkov
192741Jul 28 – Aug 22003Miami Beach, FL, USA Franz Baader
203632Jul 22–272005Tallinn, EstoniaRobert Nieuwenhuis
214603Jul 17–202007Bremen, Germany Frank Pfenning
225663Aug 2–72009Montreal, CanadaRenate A. Schmidt
236803Jul 31 – Aug 52011 Wrocław, Poland Nikolaj Bjørner, Viorica Sofronie-Stokkermans
247898Jun 9–142013 Lake Placid, New York, USAMaria Paola Bonacina
259195Aug 1–72015 Berlin, GermanyAmy Felty, Aart Middeldorp
2610395Aug 6–112017 Gothenburg, SwedenLeonardo de Moura
2710900Jul 14–172018 Oxford, United KingdomDidier Galmiche, Stephan Schulz, Roberto Sebastiani
2811716Aug 23–302019 Natal, BrazilPascal Fontaine
2912166–7Jun 29 – Jul 62020 Paris, FranceNicolas Peltier, Viorica Sofronie-Stokkermans
30Jul 11–162021 Pittsburgh, USA (virtual)

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

E is a high performance theorem prover for full first-order logic with equality. It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem proving competitions. E is developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich, now at Baden-Württemberg Cooperative State University Stuttgart.

The Herbrand Award for Distinguished Contributions to Automated Reasoning is an award given by the Conference on Automated Deduction (CADE), Inc., to honour persons or groups for important contributions to the field of automated deduction. The award is named after the French scientist Jacques Herbrand and given at most once per CADE or International Joint Conference on Automated Reasoning (IJCAR). It comes with a prize of US$1,000. Anyone can be nominated, the award is awarded after a vote among CADE trustees and former recipients, usually with input from the CADE/IJCAR programme committee.

Automated reasoning is an area of computer science and metalogic dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.

The Association for Automated Reasoning (AAR) is a non-profit corporation that serves as an association of researchers working on automated theorem proving, automated reasoning, and related fields. It organizes the CADE and IJCAR conferences and publishes a roughly quarterly newsletter.

The International Joint Conference on Automated Reasoning (IJCAR) is a series of conferences on the topics of automated reasoning, automated deduction, and related fields. It is organized semi-regularly as a merger of other meetings. IJCAR replaces those independent conferences in the years it takes place. The conference is organized by CADE Inc., and CADE has always been one of the conferences partaking in IJCAR.

Alan Bundy

Alan Richard Bundy is a professor at the School of Informatics at the University of Edinburgh, known for his contributions to automated reasoning, especially to proof planning, the use of meta-level reasoning to guide proof search.

The Federated Logic Conference (FLoC) is an international conglomeration of several mathematical logic and computer science related academic conferences that deal with the intersection of the two fields. FLoC traditionally includes:

The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) is an annual international academic conference that deals with all aspects of automated reasoning with analytic tableaux. Periodically, it joins with CADE and TPHOLs into the International Joint Conference on Automated Reasoning (IJCAR).

Drew McDermott is a former Professor of Computer Science at Yale University.

SNARK, , is a theorem prover for multi-sorted first-order logic intended for applications in artificial intelligence and software engineering, developed at SRI International.

Michael Kohlhase

Michael Kohlhase is a German computer scientist and professor at University of Erlangen–Nuremberg, where he is head of the KWARC research group.

There are a number of competitions and prizes to promote research in artificial intelligence.

The International Workshop on First-Order Theorem Proving (FTP) is a scientific meeting of researchers interested in automated theorem proving for first-order logic and related fields. FTP workshops are less formal than many conferences, but more formal than most workshops. While FTP proceedings are published informally, most FTP workshops have resulted in a special issue of a recognized peer-reviewed academic journal.

Geoff Sutcliffe

Geoff Sutcliffe is a US-based computer scientist working in the field of automated reasoning. He was born in the former British colony of Northern Rhodesia , grew up in South Africa, and earned his PhD in Australia. Sutcliffe currently works at the University of Miami, and is of both British and Australian nationality.

The CADE ATP System Competition (CASC) is a yearly competition of fully automated theorem provers for classical logic CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated Reasoning organized by the Association for Automated Reasoning. It has inspired similar competition in related fields, in particular the successful SMT-COMP competition for Satisfiability Modulo Theories, the SAT Competition for propositional reasoners, and the modal logic reasoning competition.

Lawrence T. Wos was an American mathematician, a researcher in the Mathematics and Computer Science Division of Argonne National Laboratory.

Interactive Theorem Proving (ITP) is an annual international academic conference on the topic of automated theorem proving, proof assistants and related topics, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics.

Mark E. Stickel was a computer scientist working in the fields of automated theorem proving and artificial intelligence. He worked at SRI International for over 30 years, and was Principal Scientist at the Artificial Intelligence Center.

Andrei Voronkov

Andrei Anatolievič Voronkov is a Professor of Formal methods in the Department of Computer Science at the University of Manchester.

References

  1. ↑ Lu, James J.; Erik Rosenthal (2004). "Logic-Based Reasoning for Intelligent Systems". In Alan B. Tucker (ed.). Computer Science Handbook (Second ed.). CRC Press. p. 61-24.
  2. ↑ Goré, Rajeev; Alexander Leitsch; Tobias Nipkow (2001). "Foreword". Automated Reasoning - First International Joint Conference, IJCAR 2001, Siena, Italy. Springer.
  3. ↑ "The International Conference on Automated Deduction - conferences". CADE, Inc. Retrieved 4 May 2013.CS1 maint: discouraged parameter (link)


This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.