Association for Automated Reasoning

Last updated

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 website of the association is maintained by Valentin Montmirail and Geoff Sutcliffe in Jekyll (software).

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.

Knowledge representation and reasoning is the field of artificial intelligence (AI) dedicated to representing information about the world in a form that a computer system can use to solve complex tasks such as diagnosing a medical condition or having a dialog in a natural language. Knowledge representation incorporates findings from psychology about how humans solve problems, and represent knowledge in order to design formalisms that will make complex systems easier to design and build. Knowledge representation and reasoning also incorporates findings from logic to automate various kinds of reasoning.

<span class="mw-page-title-main">Association of American Railroads</span> Industry trade group representing major North American freight railroads

The Association of American Railroads (AAR) is an industry trade group representing primarily the major freight railroads of North America. Amtrak and some regional commuter railroads are also members. Smaller freight railroads are typically represented by the American Short Line and Regional Railroad Association (ASLRRA), although some smaller railroads and railroad holding companies are also members of the AAR. The AAR also has two associate programs, and most associates are suppliers to the railroad industry.

AAR or Aar may refer to:

<span class="mw-page-title-main">American Academy of Religion</span> Learned society for scholars in religious studies

The American Academy of Religion (AAR) is the world's largest association of scholars in the field of religious studies and related topics. It is a nonprofit member association, serving as a professional and learned society for scholars involved in the academic study of religion. It has some 10,000 members worldwide, with the largest concentration being in the United States and Canada. AAR members are university and college professors, independent scholars, secondary teachers, clergy, seminarians, students, and interested lay-people.

<span class="mw-page-title-main">Proof assistant</span> Software tool to assist with the development of formal proofs by human-machine collaboration

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

<span class="mw-page-title-main">J Strother Moore</span> American computer scientist

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.

<span class="mw-page-title-main">Bruno Buchberger</span> Austrian mathematician (born 1942)

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.

Computational semantics is the study of how to automate the process of constructing and reasoning with meaning representations of natural language expressions. It consequently plays an important role in natural-language processing and computational linguistics.

<span class="mw-page-title-main">Outline of thought</span> Overview of and topical guide to thought

The following outline is provided as an overview of and topical guide to thought (thinking):

<span class="mw-page-title-main">Visual analytics</span>

Visual analytics is an outgrowth of the fields of information visualization and scientific visualization that focuses on analytical reasoning facilitated by interactive visual interfaces.

The CADE ATP System Competition (CASC) is an annual competition of fully automated theorem provers for classical logic

The Journal of Automated Reasoning was established in 1983 by Larry Wos, who was its editor in chief until 1992. It covers research and advances in automated reasoning, mechanical verification of theorems, and other deductions in classical and non-classical logic.

Qualitative Reasoning (QR) is an area of research within Artificial Intelligence (AI) that automates reasoning about continuous aspects of the physical world, such as space, time, and quantity, for the purpose of problem solving and planning using qualitative rather than quantitative information. Precise numerical values or quantities are avoided, and qualitative values are used instead (e.g., high, low, zero, rising, falling, etc.).

In information technology a reasoning system is a software system that generates conclusions from available knowledge using logical techniques such as deduction and induction. Reasoning systems play an important role in the implementation of artificial intelligence and knowledge-based systems.

The International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is an academic conference aiming at discussing cutting-edge results in the fields of automated reasoning, computational logic, programming languages and their applications.

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.

The All-America Rose Selections (AARS) is an award that was given annually, from 1940 to 2013, by the American rose industry to an outstanding new rose variety. The AARS selection was regarded as the most prestigious rose prize in the United States for 73 years. AARS was discontinued after 2013, and was replaced in 2016 by the new American Garden Rose Selections (AGRS) program.

References