System on TPTP

Last updated

System on TPTP is an online interface to several automated theorem proving systems and other automated reasoning tools. It allows users to run the systems either on problems from the latest releases from the TPTP problem library or on user-supplied problems in the TPTP syntax.

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 system is maintained by Geoff Sutcliffe at the University of Miami. In November 2010, it featured more than 50 systems, including both theorem provers and model finders. [1] System on TPTP can either run user-selected systems, or pick systems automatically based on problem features, and run them in parallel. [2]

Geoff Sutcliffe Australian computer scientist

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.

University of Miami private university in Coral Gables, Florida, United States

The University of Miami is a private research university in Coral Gables, Florida. As of 2018, the university enrolls 17,331 students in 12 separate colleges/schools, including the Leonard M. Miller School of Medicine in Miami's Health District, a law school on the main campus, and the Rosenstiel School of Marine and Atmospheric Science focused on the study of oceanography and atmospheric sciences on Virginia Key, with research facilities at the Richmond Facility in southern Miami-Dade County.


Related Research Articles

ACL2 software system consisting of a programming language, an extensible theory in a first-order logic, and an automated theorem prover

ACL2 is a software system consisting of a programming language, an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for the purpose of software and hardware verification. The input language and implementation of ACL2 are written in Common Lisp. ACL2 is free and open-source software.

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.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.


Paradox is a finite-domain model finder for pure first-order logic (FOL) with equality developed by Koen Lindström Claessen and Niklas Sörensson at the Chalmers University of Technology. It can a participate as part of an automated theorem proving system. The software is primarily written in the Haskell programming language. It is released under the terms of the GNU General Public License and is free.

Proof assistant 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.

A computer-assisted proof is a mathematical proof that has been at least partially generated by computer.

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.

Mutilated chessboard problem puzzle of pairing adjacent squares of a chessboard from which two squares have been removed

The mutilated chessboard problem is a tiling puzzle proposed by philosopher Max Black in his book Critical Thinking (1946). It was later discussed by Solomon W. Golomb (1954), Gamow & Stern (1958) and by Martin Gardner in his Scientific American column "Mathematical Games". The problem is as follows:

Suppose a standard 8×8 chessboard has two diagonally opposite corners removed, leaving 62 squares. Is it possible to place 31 dominoes of size 2×1 so as to cover all of these squares?

In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is proved to be impossible to construct an algorithm that always leads to a correct yes-or-no answer. The halting problem is an example: it can be proven that there is no algorithm that correctly determines whether arbitrary programs eventually halt when run.

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

SPASS is an automated theorem prover for first-order logic with equality developed at the Max Planck Institute for Computer Science and using the superposition calculus. The name originally stood for Synergetic Prover Augmenting Superposition with Sorts. The theorem proving system is released under the FreeBSD license.

TPTP is an abbreviation and may refer to

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.

In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever.

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 Test & Performance Tools Platform (TPTP) is an Eclipse tool used to profile plug-ins of the IDE that may run on different platforms. TPTP is tightly integrated into Eclipse so that it can make the profiling from within the IDE. It is used to find and isolate performance problems. Such problems can be performance bottlenecks, object leaks, or system resource limits. It can be used with both simple and complex applications, like stand-alone applications, plug-ins, or multi-machine enterprise applications.

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.

References

  1. ↑ Sutcliffe, Geoff. "System on TPTP" . Retrieved 4 November 2010.
  2. ↑ Sutcliffe, Geoff; D. Seyfang (1999). "Smart selective competition parallelism ATP". Proceedings of the Twelfth International Florida Artificial Intelligence Research Society Conference: 341–345.


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.