Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems that humans can prove by the... > Lire la suite
Plus d'un million de livres disponibles
Retrait gratuit en magasin
Livraison à domicile sous 24h/48h* * si livre disponible en stock, livraison payante
26,80 €
Expédié sous 6 à 12 jours
ou
À retirer gratuitement en magasin U entre le 11 septembre et le 18 septembre
Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems that humans can prove by the use of geometric operations on diagrams, so-called diagrammatic proofs. This book investigates and describes how such diagrammatic reasoning about mathematical theorems can be automated. Concrete, rather than general, diagrams are used to prove particular instances of a universal statement. The " inference steps " of a diagrammatic proof are formulated in terms of geometric operations on the diagram. A general schematic proof of the universal statement is induced from these proof instances by means of the constructive w-rule. Schematic proofs are represented as recursive programs, which when given a particular diagram return a proof for that diagram. It is necessary to reason about this recursive program to show that it outputs a correct proof. One method of confirming the soundness of the abstraction of a schematic proof from proof instances is to prove the correctness of the schematic proof in the meta-theory of diagrams. This book presents an investigation of these ideas and their implementation in a system called DIAMOND.