---
title: "Solving \"How to Clear a Block\" with Constructive Matching Methodology"
authors:
  - "Marta Franová"
  - "Yves Kodratoff"
doi: ""
url: "https://ijcai.org/proceedings/1991/35"
pdf: "https://ijcai.org/proceedings/1991/0035.pdf"
venue: "Proceedings of the Twelfth International Joint Conference on Artificial Intelligence"
year: 1991
pages: "232-238"
track: "Automated Reasoning"
keywords:
---

# Solving "How to Clear a Block" with Constructive Matching Methodology

Marta Franová, Yves Kodratoff

*Proceedings of the Twelfth International Joint Conference on Artificial Intelligence*, 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.