類推における証明項の変換について

類推の枠組みを、置き換え規則の自然な拡張である文脈スキーマによって定式化する。類推の帰結は一般には一意に定まらず、これは類推の観点(類似性のとらえ方)に依存すると考え、スキーマにおける制約で表現する。また、文脈で類推において保存される部分(2つの対象間で同型対応の部分)を表す。制約を論理的帰結にとり、定理証明の問題において、論理式間の類似性をそのスキーマとのパターンマッチング可能性で定義する。類推を用いて証明をする際に証明可能性を保持しながら、証明したい論理式を単純な論理式に分解して既に得られている証明を再利用する。さらに、カリー・ハワード同型により類推による定理証明が証明項の変換として定式化され、論理式間の類似性を表現しているスキーマによって、この変換規則(類推)を得ることができる。
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.