Sciweavers

LPAR
2010
Springer
13 years 9 months ago
Automated Proof Compression by Invention of New Definitions
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...
Jirí Vyskocil, David Stanovský, Jose...
TPHOL
2003
IEEE
14 years 4 months ago
Program Extraction from Large Proof Developments
Abstract. It is well known that mathematical proofs often contain (abstract) algorithms, but although these algorithms can be understood by a human, it still takes a lot of time an...
Luís Cruz-Filipe, Bas Spitters