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
Livré chez vous entre le 26 juillet et le 31 juillet
En magasin
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.