Automated Mathematical Proof Simplifier (version 1.0)

Result code in 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>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Automated Mathematical Proof Simplifier (version 1.0)

Original language description

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.

Czech name

—

Czech description

—

Type

R - Software

CEP classification

JD - Use of computers, robotics and its application

OECD FORD branch

—

Project

—

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2009

Confidentiality

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

Internal product ID

amps-1.0

Technical parameters

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

Economical parameters

—

Owner IČO

68407700

Owner name

ČVUT FEL, Katedra kybernetiky