Solving "How to Clear a Block" with Constructive Matching Methodology
Proceedings of the Twelfth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 232-238.
Abstract
Constructive Matcliinfj is a methodology for proving by induction Specifications Theorems (ST), i.e., theorems of the fonn 'Vx 3z (P(x) ~ Q(x,z)). ST fonnalize the problem of constructing a program specified by given an input vector x, an input condition P, find an output vector z verifying Q(x,z), whenever P(x) holds. Till now , we have applied our method to the so-called Constnu:tiEJfe 'DomtJins, for which one disposes of a unique way of building any input and output data. The goal of this paper is to enlarge our methodology to well-founded domains which are not constructible. As a simple example, Manna and Waldinger's "How to Clear a Block" problem 2 is solved. As opposed to theirs, our method does consider strategic aspects of program derivation from a fonnal specification.
@inproceedings{ijcai1991p35,
title = {Solving "How to Clear a Block" with Constructive Matching Methodology},
author = {Franová, Marta and Kodratoff, Yves},
booktitle = {Proceedings of the Twelfth International Joint Conference on
Artificial Intelligence, {IJCAI-91}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {John Mylopoulos and Ray Reiter},
pages = {232--238},
year = {1991},
month = {8},
note = {Automated Reasoning},
url = {https://ijcai.org/proceedings/1991/35},
}
TY - CPAPER TI - Solving "How to Clear a Block" with Constructive Matching Methodology AU - Franová, Marta AU - Kodratoff, Yves T2 - Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, IJCAI-91 PB - International Joint Conferences on Artificial Intelligence PY - 1991 SP - 232 EP - 238 UR - https://ijcai.org/proceedings/1991/35 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
