THFTPTP
An Infrastructure for Typed Higher-order Form Automated Theorem Proving
| Coordinatore |
Organization address
address: CAMPUS contact info |
| Nazionalità Coordinatore | Non specificata |
| Totale costo | 130˙109 € |
| EC contributo | 130˙109 € |
| Programma | FP7-PEOPLE
Specific programme "People" implementing the Seventh Framework Programme of the European Community for research, technological development and demonstration activities (2007 to 2013) |
| Code Call | FP7-PEOPLE-2007-4-2-IIF |
| Anno di inizio | 2008 |
| Periodo (anno-mese-giorno) | 2008-07-15 - 2009-09-14 |
Partecipanti
| # | ||||
|---|---|---|---|---|
| 1 |
UNIVERSITAET DES SAARLANDES
Organization address
address: CAMPUS contact info |
DE (SAARBRUECKEN) | coordinator | 0.00 |
Mappa
Word cloud
Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.
Obiettivo del progetto (Objective)
'There is a well established infrastructure that supports research and development of first-order Automated Theorem Proving (ATP) systems, stemming from the Thousands of Problems for Theorem Provers (TPTP) problem library. This infrastructure includes the TPTP itself, the TPTP language and SZS result ontology, the Thousands of Solutions from Theorem Provers (TSTP) solution library, various tools associated with the libraries, and the CADE ATP System Competition (CASC). This infrastructure has been central to the impressive progress that has been made in the development of high performance first-order ATP systems. Research and development of ATP for higher-order logic has been in progress for as long as that for first-order logic. However, the computational issues that must be faced are significantly harder than those in first-order ATP, and the state of the art in higher-order ATP is not as advanced as that of first-order ATP. While there are several effective interactive systems for reasoning in higher-order logic, there is limited automation. Critically, research and development has not been supported by a commonly accepted infrastructure that provides leverage for progress leading to effective and successful application. This proposed research will develop an infrastructure, corresponding to that in place for first-order ATP, for higher-order ATP in Church's simple type theory. The effect will be to support research, development, and deployment of higher-order ATP systems, so that they can be used as effective components of academic and industrial processes. The long-term goal, beyond this proposed research, is to provide an infrastructure that extends to other forms of higher-order logic that extend Church's simple type theory, e.g., intiutionistic type theory.'
Introduzione (Teaser)
A new European research initiative is creating software that will help prove the validity of theorems in a quick, efficient and accurate way.
Descrizione progetto (Article)
Automated theorem proving, also known as automated deduction, is a key subfield of automated reasoning. It is concerned with proving formally represented theorems in a wide range of domains, through the use of computers. Since 1993 development of effective automated theorem proving systems has been supported by the Thousands of Problems for Theorem Provers (TPTP) problem library and the Thousands of Solutions from Theorem Provers (TSTP) solution library.
The EU-funded project 'An Infrastructure for Typed Higher-order Form Automated Theorem Proving' (THFTPTP) was focused on research and development of automated theorem proving in classical higher-order logic. It designed a novel TPTP language to express problems and solutions in higher-order logic. The software involves a collection of higher-order test problems in TPTP and higher-order problem solutions in TSTP, as well as a result and output ontology for higher-order ATP. The project also provided tools for preparing, processing and analysing higher-order ATP problems and solutions.
The results of the project were disseminated through several papers at conferences and workshops, as well as through conferences themselves and presentations. Three grant proposals were strongly influenced by the project, ascertaining the viability of its arguments and results. The new THFTPTP infrastructure has been integrated with the TPTP project, which is available at http://www.tptp.org.
The THFTPTP project opened up several new research directions and initiatives that will facilitate the development of new principles. It has offered valuable transfer of knowledge and expertise to researchers and students at the project's host university and 11 other institutions across Europe.
In short, THFTPTP successfully developed the software products it set out to create and helped develop five fully automated ATP systems for higher-order logic in the THF format.