CM-Strategy: A Methodology for Inductive Theorem Proving or Constructive Well-Generalized Proofs
Proceedings of the Ninth International Joint Conference on Artificial Intelligence. Theorem Proving. 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.
@inproceedings{ijcai1985p245,
title = {CM-Strategy: A Methodology for Inductive Theorem Proving or Constructive Well-Generalized Proofs},
author = {Franová, Marta},
booktitle = {Proceedings of the Ninth International Joint Conference on
Artificial Intelligence, {IJCAI-85}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Aravind Joshi},
pages = {1214--1219},
year = {1985},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1985/245},
}
TY - CPAPER TI - CM-Strategy: A Methodology for Inductive Theorem Proving or Constructive Well-Generalized Proofs AU - Franová, Marta T2 - Proceedings of the Ninth International Joint Conference on Artificial Intelligence, IJCAI-85 PB - International Joint Conferences on Artificial Intelligence PY - 1985 SP - 1214 EP - 1219 UR - https://ijcai.org/proceedings/1985/245 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
