---
title: "CM-Strategy: A Methodology for Inductive Theorem Proving or Constructive Well-Generalized Proofs"
authors:
  - "Marta Franová"
doi: ""
url: "https://ijcai.org/proceedings/1985/245"
pdf: "https://ijcai.org/proceedings/1985/0245.pdf"
venue: "Proceedings of the Ninth International Joint Conference on Artificial Intelligence"
year: 1985
pages: "1214-1219"
track: "Theorem Proving"
keywords:
---

# CM-Strategy: A Methodology for Inductive Theorem Proving or Constructive Well-Generalized Proofs

Marta Franová

*Proceedings of the Ninth International Joint Conference on Artificial Intelligence*, pages 1214-1219.

## Abstract

The main problem, when automatically proving theorems by induction is the problern of strategy, or, how to automatically direct deductlons. This is not trivial, and, at present, only a mlxture of complicated strategies have been investigated. The essential contribution of this paper is therefore the proposiog of a new strategy for inductive theorem proving, tnsplred by a new mecanlsm called Constructive Matehing (CM), and used for automatic programmlog [f04]. We also propose a new method for the recognltion of predicates and functions, necessary to prove a theorem by our approach, that are not defined in the knowledge-base ("Invention" of new operators). Finally, we illustrate the obtalnement of a sultable generalized Iemma necessary for the proof.