Automated Mathematical Proof Simplifier (version 1.0)

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F09%3A00166492" target="_blank" >RIV/68407700:21230/09:00166492 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Automated Mathematical Proof Simplifier (version 1.0)

Popis výsledku v původním jazyce

State-of-the-art automated theorem provers (ATPs) are today able to solve relatively complicated mathematical problems. But as ATPs become stronger and more used by mathematicians, the length and human unreadability of the automatically found proofs become a serious problem for the ATP users. One remedy is automated proof shortening by invention of new definitions. This software uses a new algorithm for automated shortening of arbitrary terms (like mathematical proofs) by invention of new definitions. It is conjectured that the problem of finding the most shortening definition is NP-complete, thus a heuristics based on substitution trees is used. This software has been implemented and tested on several thousand automatically found proofs.

Název v anglickém jazyce

Automated Mathematical Proof Simplifier (version 1.0)

Popis výsledku anglicky

State-of-the-art automated theorem provers (ATPs) are today able to solve relatively complicated mathematical problems. But as ATPs become stronger and more used by mathematicians, the length and human unreadability of the automatically found proofs become a serious problem for the ATP users. One remedy is automated proof shortening by invention of new definitions. This software uses a new algorithm for automated shortening of arbitrary terms (like mathematical proofs) by invention of new definitions. It is conjectured that the problem of finding the most shortening definition is NP-complete, thus a heuristics based on substitution trees is used. This software has been implemented and tested on several thousand automatically found proofs.

Druh

R - Software

CEP obor

JD - Využití počítačů, robotika a její aplikace

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2009

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Interní identifikační kód produktu

amps-1.0

Technické parametry

Software pracuje v UNIXovém prostředí a vyžaduje nainstalovaný SWI-Prolog.

Ekonomické parametry

—

IČO vlastníka výsledku

68407700

Název vlastníka

ČVUT FEL, Katedra kybernetiky