| Presentation | 1994/7/7 Analysis of proof term transformation in reasoning by analogy Ken-etsu Fujita, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | We formalize an Analogical Framework (AF) in terms of a contextual schema,which is a natural extension of well-known replacement rule equals by equals.In theorem proving a similarity relation between formulae is defined by the schema,and similarity checking is executed by pattern matching with the schemata.The notion of AF enable us to describe variant and invariant part of objects under analogical reasoning (transformation).Hence in order to discover a proof we can decompose a formula to obtain already known simpler formulae by maintaining the provability,and can reuse already given formulae for the decomposed ones to prove a new formula.Moreover the notion of Curry-Howard-DeBruijn isomorphism makes it possible to treat analogical reasoning as proof terms transformation.Our approach can provide a way of how to construct proof term transformation rules according to formulae similarity expressed by the schema.This method fits naturally with the way in which humans carry out proving,and it will serve as a guide to the discovery of the new proofs as a tool of analogical reasoning,which is also practically important to prove formulae efficiently and marcroscopically. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | reasoning by analog / natural deduction / curry-Howard isomorphism / proof terms / schema |
| Paper # | SS94-17 |
| Date of Issue |
| Conference Information | |
| Committee | SS |
|---|---|
| Conference Date | 1994/7/7(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Software Science (SS) |
|---|---|
| Language | ENG |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Analysis of proof term transformation in reasoning by analogy |
| Sub Title (in English) | |
| Keyword(1) | reasoning by analog |
| Keyword(2) | natural deduction |
| Keyword(3) | curry-Howard isomorphism |
| Keyword(4) | proof terms |
| Keyword(5) | schema |
| 1st Author's Name | Ken-etsu Fujita |
| 1st Author's Affiliation | Faculty of Computer Science and System Engineering,Kyushu Institute of Technology() |
| Date | 1994/7/7 |
| Paper # | SS94-17 |
| Volume (vol) | vol.94 |
| Number (no) | 134 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |