# Mathematical Reasoning with Diagrams. From Intuition to Automation

## Mateja Jamnik

Note moyenne
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
26,80 €

## Résumé

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.

## Sommaire

• The History of Diagrammatic Systems
• Diagrammatic Theorems and the Problem Domain
• The Constructive w-Rule and Schematic Proofs
• Designing a Diagrammatic Reasoning System
• Diagrammatic Operations
• The Construction of Schematic Proofs
• The Verification of Schematic Proofs
• Diamond in Action
• Complete Automation.

## Caractéristiques

• Date de parution
05/02/2002
• Editeur
• Collection
• ISBN
1-57586-324-3
• EAN
9781575863245
• Présentation
Broché
• Nb. de pages
204 pages
• Poids
0.31 Kg
• Dimensions
15,4 cm × 23,0 cm × 1,2 cm

26,80 €