Scheme-based Theorem Discovery and Concept Invention: Rewriting theory-exploration - Couverture souple

Montaño Rivas, Omar

 
9783659886201: Scheme-based Theorem Discovery and Concept Invention: Rewriting theory-exploration
Couverture souple
ISBN 10 : 3659886203 ISBN 13 : 9783659886201
Editeur : LAP LAMBERT Academic Publishing, 2016

Synopsis

This book describes an approach to automatically invent/explore new mathematical theories, with the goal of producing results comparable to those produced by humans, as represented, for example, in the libraries of proof assistants. The approach described is based on schemes, which are formulae in higher-order logic. It shows that it is possible to automate the instantiation process of schemes to generate conjectures and definitions. It also shows how the new definitions and the lemmata discovered during the exploration of a theory can be used, not only to help with the proof obligations during the exploration, but also to reduce redundancies inherent in most theory-formation systems. It describes how to exploit associative-commutative (AC) operators using ordered rewriting to avoid AC variations of the same instantiation. All ideas contained in this book are implemented in an automated tool, called IsaScheme, which employs Knuth-Bendix completion and recent automatic inductive proof methods. This systematic and comprehensive introduction to the scheme-based theory exploration will be welcome by researchers and graduate students alike.

Les informations fournies dans la section « Synopsis » peuvent faire référence à une autre édition de ce titre.

Présentation de l'éditeur

This book describes an approach to automatically invent/explore new mathematical theories, with the goal of producing results comparable to those produced by humans, as represented, for example, in the libraries of proof assistants. The approach described is based on schemes, which are formulae in higher-order logic. It shows that it is possible to automate the instantiation process of schemes to generate conjectures and definitions. It also shows how the new definitions and the lemmata discovered during the exploration of a theory can be used, not only to help with the proof obligations during the exploration, but also to reduce redundancies inherent in most theory-formation systems. It describes how to exploit associative-commutative (AC) operators using ordered rewriting to avoid AC variations of the same instantiation. All ideas contained in this book are implemented in an automated tool, called IsaScheme, which employs Knuth-Bendix completion and recent automatic inductive proof methods. This systematic and comprehensive introduction to the scheme-based theory exploration will be welcome by researchers and graduate students alike.

Biographie de l'auteur

Omar Montaño Rivas is a Professor of Automated Reasoning at the Universidad Politécnica de San Luis Potosí. His research interests focus on the exploration of mathematical theories and the automation of mathematical reasoning with applications to formal methods. He is the author of a number of publications and has held several research grants.

Les informations fournies dans la section « A propos du livre » peuvent faire référence à une autre édition de ce titre.

Éditeur
LAP LAMBERT Academic Publishing
Date d'édition
2016
Langue
anglais
ISBN 10 
3659886203
ISBN 13 
9783659886201
Reliure
Broché
Nombre de pages
152
Coordonnées du fabricant
non disponible
Personne responsable
KreGa Onlinehandel GmbH
4950000000000
info@krega-onlinehandel.de

Birkenweg 31
Brakel
33034
Allemagne