Mathematical Reasoning With Diagrams. From Intuition To Automation

Par : Mateja Jamnik

Formats :

  • Réservation en ligne avec paiement en magasin :
    • Indisponible pour réserver et payer en magasin
  • Nombre de pages204
  • PrésentationBroché
  • Poids0.31 kg
  • Dimensions15,4 cm × 23,0 cm × 1,2 cm
  • ISBN1-57586-324-3
  • EAN9781575863245
  • Date de parution05/02/2002
  • CollectionCSLI Lecture notes
  • ÉditeurCSLI Publications

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.
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.