Assume a statement or specification expressed as a first-order formula F Well established fields in Automated Deduction focus on algorithms for the detection of unsatisfiability of clause sets C, sat-equivalent to

We express the idea more formally:

Assume a deduction system I based on resolution. To prove the validity of F,The goal of our approach to Automated Model Building is to transform C' into a representation of an (infinite) Herbrand model of \C. We call this representationnotF is transformed into a sat-equivalent clause set C, To keep our argumentation simple, we assume C to be decidable by I If I is applied on C, then it terminates with a saturated set of clauses C'notcontaining the empty clause. Provided I is refutationally complete, C' is consistent. Hence, the set C represents a (possibly infinite) class of counter-examples, but it is usually not possible to extract one of these models of C' directly. In most cases it is not even possible to extract an `understandable' model representation of one of these models.

We motivate this by giving an example:

There are arbitrarily many possibilities to modify a statement so that it becomes valid. If we decide that our premises are correct, we have to reconsider the conclusion:No hungry cat gazes at the moon. Some cats gazing at the moon are in love. Conclude that some cats which are in love are hungry.

We want to know whether the conclusion is logically justified or not.

Let "H(x)" stand for "x is a hungry cat", "G(x)" for "cat x gazes at the moon", and "L(x)" for "cat x is in love". Now, we encode our problem in first-order logic:F <-> [(

forallx)( H(x) ->notG(x))and(existsx)( G(x)andL(x))] -> (existsx)( L(x)andH(x)).To apply resolution, we have to transform

notF into a clause setC= {

notH(x)ornotG(x), G(a), L(a),notL(x)ornotH(x) }It is easy to see that any reasonable resolution refinement terminates on C, without inferring the empty clause. If we want to correct F such that it becomes valid, the counter-example (assuming, we can actually construct one), can serve as guiding data. With the methods employed in TILT the following Herbrand model I = {

notH(a), G(a), L(a) } is derivable. This models describes a word in which exists exactly one cat a, this cat is in love, free of hunger and gazing at the moon.

The deduction system TILT implements the recent results of the Vienna Group. TILT embodies three componentsNo hungry cat gazes at the moon. Some cats gazing at the moon are in love. Conclude that some cats which are in love are {\em not} hungry.

We denote the corresponding formula as F'. Applying resolution to the new clause set C', sat-equivalent tonotF', we derive the empty clause. Hence, the new conclusion is justified. We call this approach to Automated Model buildingresolution-based.

- Classification

The Classification component tests the input clause set C for membership in safe classes. - Model Building

If C turns out to be satisfiable, the information achieved in the Classification component is used to generate a model representation for C. This component splits into two independent parts: a*standard*and an*experimental*part. - Clause Evaluation

The obtained model representation is applied to evaluate general clauses based on the same signature as C.

The overall structure of TILT is best presented by a picture

Download TILT

Usage

TILT Master Last modified: Mon Feb 19 14:01:37 CET 2001