WikiMili The Free Encyclopedia

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.

**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.

**Automated reasoning** is an area of computer science, cognitive science, and mathematical logic 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 even philosophy.

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.

The website of the association is maintained by Valentin Montmirail and Geoff Sutcliffe in Jekyll (software).

**Geoff Sutcliffe** is a US-based computer scientist working in the field of automated reasoning. He is of both British and Australian nationality. He was born in the former British colony of Northern Rhodesia , grew up in South Africa, and earned his Ph.D. in Australia. He works at the University of Miami. He is the developer of the Thousands of Problems for Theorem Provers (TPTP) problem library, and of the TPTP language for formal specification of Automated theorem proving problems and solutions. Since 1996 he has been organizing the annual CADE ATP System Competition (CASC), associated with the Conference on Automated Deduction and International Joint Conference on Automated Reasoning. He has been a co-organizer of several Automated reasoning challenges, including The Modal Logic $100 Challenge, The MPTP $100 Challenges, and The SUMO $100 Challenges. Together with Stephan Schulz, Sutcliffe founded and has been organizing the ES* Workshop series, a venue for presentation and publishing of practically oriented Automated Reasoning research.

**Jekyll** is a simple, blog-aware, static site generator for personal, project, or organization sites. Written in Ruby by Tom Preston-Werner, GitHub's co-founder, it is distributed under the open source MIT license.

This computer science article is a stub. You can help Wikipedia by expanding it. |

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.

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.

**Inferences** are steps in reasoning, moving from premises to logical consequences; etymologically, the word *infer* means to "carry forward". Inference is theoretically traditionally divided into deduction and induction, a distinction that in Europe dates at least to Aristotle. Deduction is inference deriving logical conclusions from premises known or assumed to be true, with the laws of valid inference being studied in logic. Induction is inference from particular premises to a universal conclusion. A third type of inference is sometimes distinguished, notably by Charles Sanders Peirce, distinguishing abduction from induction, where abduction is inference to the best explanation.

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:

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.

**Robert Anthony Kowalski** is a logician and computer scientist, who has spent most of his career in the United Kingdom.

An **Advanced Train Control System** (**ATCS**) is a system of railroad equipment designed to ensure safety by monitoring locomotive and train locations, providing analysis and reporting, and automating track warrants and similar orders. ATCS specifications are published by the Association of American Railroads (AAR), and are designed to document the stated requirements of railroad operational and technical professionals concerning ATCS hardware and software.

**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.

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

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

**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.

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.

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.

**Andrei Aleksandrovič Voronkov** is a Professor of Formal methods in the School of Computer Science at the University of Manchester.