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 an American 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.
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 the organizers of the Conference on Automated Deduction (CADE), 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.
The CADE ATP System Competition (CASC) is an annual competition of fully automated theorem provers for classical logic
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.
Robert Lee Constable is an American computer scientist. He is a professor of computer science and first and former dean of the Faculty of Computing and Information Science at Cornell University. He is known for his work on connecting computer programs and mathematical proofs, especially the Nuprl system. Prior to Nuprl, he worked on the PL/CV formal system and verifier. Alonzo Church supervised Constable's junior thesis while he was studying in Princeton. Constable received his PhD in 1968 under Stephen Kleene and has supervised over 40 students.
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, then once again in both fields since 2022. It is endowed with 15000, later with 20000 euros, and named in honor of the French logician Jacques Herbrand (1908-1931).