Malleable Theorem Proving Architectures
Project goals
Encouraged by the promising results of the recent years with the improvement of automatic theorem provers by the integration of (deep) machine learning components, this project aims to bring the technology to a new level by proposing and implementing new theorem proving architectures directly designed to benefit the most from the marriage of the deductive and inductive technologies. The ultimate aim of the project is to improve the performance of a state-of-the-art prover in terms of general-purpose proving skills (as measured on problems from the representative TPTP library) by at least 15 percent. A corresponding improvement in application areas such as automation in interactive theorem proving or program verification is expected to follow.
Keywords
automatic-theorem-provingsaturation-algorithmsmachine-learning
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
SGA0202400001
Main participants
České vysoké učení technické v Praze / Český institut informatiky, robotiky a kybernetiky
Contest type
VS - Public tender
Contract ID
24-12759S
Alternative language
Project name in Czech
Tvárné architektury pro automatické dokazování vět
Annotation in Czech
Motivován slibnými výsledky posleních let v oblasti zlepšování automatických dokazovačů vět integrováním komponent (hlubokého) strojového učení, cílem toho projektu je posunout celou technologii na nový vývojový stupeň návrhem a implementací nových dokazovacích architektur navržených přímo tak, aby co nejvíce těžily ze spojení příslušných deduktivích a induktívních metod. Ultimátním cílem projektu je vylepšit výkon moderního dokazovače ve smyslu obecných dokazovací schopností (měřených na problémech z reprezentativní knihovny TPTP) o alespoň 15 procent. Očekavá se i odpovídající vylepšení v aplikačních oblastech jako je automatizace v interaktivním dokazovaní vět či při verifikaci programů.
Scientific branches
R&D category
ZV - Basic research
OECD FORD - main branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
OECD FORD - secondary branch
—
OECD FORD - another secondary branch
—
AF - Documentation, librarianship, work with information
BC - Theory and management systems
BD - Information theory
IN - Informatics
Solution timeline
Realization period - beginning
Jan 1, 2024
Realization period - end
Dec 31, 2026
Project status
B - Running multi-year project
Latest support payment
Feb 29, 2024
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP25-GA0-GA-R
Data delivery date
Feb 21, 2025
Finance
Total approved costs
7,885 thou. CZK
Public financial support
7,885 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Recognised costs
7 885 CZK thou.
Public support
7 885 CZK thou.
0%
Provider
Czech Science Foundation
OECD FORD
Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Solution period
01. 01. 2024 - 31. 12. 2026