Laboratory of Informatics of Grenoble
A Flat Instantiation ScHema

What can be downloaded from this page ?
We have developed an instantiation schema which reduces (in some cases) the satisfiability problem for a set S1 of first-order clauses to a satisfiability problem for a (finite) set S0 of ground instances of the clauses in S1. The latter problem is well-known to be decidable, whereas the former is only sem-decidable. This instantiation schema is flat in the sense that every clause in S0 is obtained from a clause in S1 by replacing all the variables in it by constant symbols.
This instantiation schema is intented to be used for solving Satisfiability Modulo Theories problems. It is (trivially) sound, i.e. if the obtained clause set S0 is unsatisfiable then so is the original one S1. The converse (refutationally completeness) holds only for some particular clause sets, called controllable. Details can be found in the following research report.

Determining whether a given clause set is controllable or not is a decidable problem, but it is not straigtforward since it requires checking many different conditions involving fixpoint computations. Moreover several parameters have to be set properly. Thus we have developed a small program to automatise the process. Here is an example of an input file, containing the main theories that are useful in program verification (lists, arrays etc.).

The program is written in Prolog. It should run easily on any Prolog system (tested only on SWI-Prolog).
The instantiation schema itself is not yet implemented (we hope to be able to do this soon...). The program uses a straightforward implementation of the conditions defined in the above report, without any optimisation. It is not intended to be efficient, and will probably not work if the clause set is very large, but it is meant to be easily modifiable and extensible and as clear as possible.

Disclaimer: this program is a highly. experimental software. It has been developed for facilitating on-going researches and is delivered as it is, for research purpose only, without any guarantee. See here for details.

For further information, please contact N. Peltier or M. Echenim
Laboratory of Informatics of Grenoble, CAPP Team