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.
J Strother Moore is a computer scientist. He is a co-developer of the Boyer–Moore string-search algorithm, Boyer–Moore majority vote algorithm, and the Boyer–Moore automated theorem prover, Nqthm. He made pioneering contributions to structure sharing including the piece table data structure and early logic programming. An example of the workings of the Boyer–Moore string search algorithm is given in Moore's website. Moore received his Bachelor of Science (BS) in mathematics at Massachusetts Institute of Technology in 1970 and his Doctor of Philosophy (Ph.D.) in computational logic at the University of Edinburgh in Scotland in 1973.
Bruno Buchberger is Professor of Computer Mathematics at Johannes Kepler University in Linz, Austria. In his 1965 Ph.D. thesis, he created the theory of Gröbner bases, and has developed this theory throughout his career. He named these objects after his advisor Wolfgang Gröbner. Since 1995, he has been active in the Theorema project at the University of Linz.
The Conference on Automated Deduction (CADE) is the premier academic conference on automated deduction and related fields. 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). This has been repeated biannually since 2004.
In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is 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.
Franz Baader is a German computer scientist at Dresden University of Technology.
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 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.
John Alan Robinson was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University.
There are a number of competitions and prizes to promote research in artificial intelligence.
William Walker McCune was an American computer scientist and logician working in the fields of automated reasoning, algebra, logic, and formal methods. He was best known for the development of the Otter, Prover9, and Mace4 automated reasoning systems, and the automated proof of the Robbins conjecture using the EQP theorem prover.
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 (1930–2020) was an American mathematician, a researcher in the Mathematics and Computer Science Division of Argonne National Laboratory.
Donald W. Loveland is a professor emeritus of computer science at Duke University who specializes in artificial intelligence. He is well known for the Davis–Putnam–Logemann–Loveland algorithm.
Melvin Fitting is a logician with special interests in philosophical logic and tableau proof systems. He was a professor at Lehman College and the Graduate Center of the City University of New York. from 1968 to 2013. At the Graduate Center he was in the departments of Computer Science, Philosophy, and Mathematics, and at Lehman College he was in the department of Mathematics and Computer Science. He is now Professor emeritus.
Tobias Nipkow is a German computer scientist.
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.
Charles Gregory Nelson was an American computer scientist.
Andrei Anatolievič Voronkov is a Professor of Formal methods in the Department of Computer Science at the University of Manchester.
The Jacques Herbrand Prize is an award given by the French Academy of Sciences to young researchers in the field of mathematics, physics, and their non-military applications. It was created in 1996, and first awarded in 1998. In 2001, it was renamed to Grand Prix Jacques Herbrand . Until 2002, the prize was given each year in both fields; since 2003, it is given alternatingly. It is endowed with 15000, later with 20000 euros, and named in honor of the French logician Jacques Herbrand (1908-1931).