RDL Tutorial

The Constraint Contextual Rewriting Project: Software

RDL Version 1.1: Tutorial

RDL Version 1.1 is a system for clause simplification in a quantifier-free first-order logic with equality. So its input is a pair of (quantifier-free first-order) clauses in Prolog-like syntax. The former is the clause to be simplified and the latter is the clause that the user aims to obtain from the simplification activity of RDL. (However, specifying the output clause is optional.) Running RDL on such a pair of clauses results in the final output

Status: ok!

if the result of the simplfication activity of RDL is syntactically equivalent to the second clause proposed by the user, and

Status: failed!

otherwise.

Notice that RDL always terminates. This is because Constraint Contextual Rewriting (CCR) is terminating (see the paper [ccr-frocos2000] for details) and the actual implementation of the system closely resembles the abstract characterization of CCR.

Lets start a complete loop through the usage of RDL. Starting point is always the clause to be simplified. Assume that you want to simplify to true the following clause:

not(x=<0) \/ rem(x*y,x)=0

where `not(_)' denotes the negation, `_>_' (`_*_') is the greater-than relation (multiplication, resp.) over integers, and `rem(_,_)' denotes the remainder of two integers defined in the usual way. Furthermore, assume that you know the following fact about `rem' and `*':

not(U=<0) ==> rem(U*_,U)=0

where `_==>_' denotes implication.

The first step is to write the given clause in the syntax accepted by RDL. For the clause above, this is easly done and the result is the following Prolog list:

[not(x=<0), rem(x*y,x)=0].

Hence, a clause of the form ``L1 \/ L2 \/ ... \/ Ln'' (where Li is a literal for i=1, ..., n) is represented in RDL as [l1, l2, ..., ln], where li is the RDL representation of the literal Li (for i=1, ..., n).

The next step is to provide RDL with an input file that contains exactly the above formulae (i.e. both the clause to be simplified and the fact about the relationship between `rem' and `*') in a Prolog-like syntax:

description(zhang_la_bis, 
'Silvio Ranise',                 
'A modified version of zhang_la which copes with  
the ordering of Prolog terms.').                  
fact(zhang_la_bis, rem_rew, [not(U=<0)],rem(U*_,U)=0). 
input(zhang_la_bis, [rem(x*y,x)=0,x=<0]).              
expected_output(zhang_la_bis, la, prolog, [true]).

An RDL input file consists of three parts, a description part (predicate description), a part where all the known facts about the function and predicate symbols occurring in the clause to be simplified are given (predicate fact), and a final part where both the clause to be simplified is presented (predicate input) and the expected simplified clause as well as two parameters of the system are given (predicate expected_output). Let us consider each part in more details.

description(p, a, d): p is a Prolog constant uniquely identifying the problem we are going to submit to RDL, a is a Prolog string identifying the author of the problem, and d is a Prolog string containing a brief description of the problem.
fact(p, n, prem, concl): p is the Prolog constant identifying the problem for which the fact can be used, n is a Prolog constant uniquely identifying the fact within the problem, prem is the list of premises (i.e. literals) of the fact abd concl is the conclusion (i.e. atom) of the fact.
input(p, clause): p is the Prolog constant identifying the problem and clause is the clause to be simplified.
expected_output(p, dp, ord, clause): p is the Prolog constant identifying the problem, dp is the decision procedure to be used (see below for details), ord is the ordering to be used (again see below for details), and clause is the clause the user aims to obtain from the simplification activity of the system. Notice that the user is free to leave the expected output clause unspecified by writing a Prolog variable (such as `_') for clause.

RDL must know two settings:

the decision procedure to use. The user can select one among the following:
1. eq: a decision procedure for ground equalities with the augmentation heuristics disabled,
2. aug(eq): a decision procedure for ground equalities with the augmentation heuristics enabled,
3. la: a decision procedure for linear arithmetic with the augmentation heuristics disabled,
4. aug(la): a decision procedure for linear arithmetic with the augmentation heuristics enabled,
5. aff(la): a decision procedure for linear arithmetic with the affinization technique enabled so to handle non-linear inequalities of the form s*t =< K, where s and t are first order terms interpreted as integers, and K is a non-negative integer.
6. aug_aff(la): a decision procedure for linear arithmetic with a combination of the augmentation and the affinization techniques enabled so to combine the flexibility of the former and the degree of automation of the latter.
7. eq_la: a combination of a decision procedure for ground equalties and a decision procedure for linear arithmetic over integers.
8. aug(eq_la): a combination of a decision procedure for ground equalties and a decision procedure for linear arithmetic with the augmentation heuristics enabled.
9. aff(eq_la): a combination of a decision procedure for ground equalties and a decision procedure for linear arithmetic with the affinization technique enabled.
10. aug_aff(eq_la): a combination of a decision procedure for ground equalties and a decision procedure for linear arithmetic over integers with a combination of the augmentation and the affinization techniques enabled so to combine the flexibility of the former and the degree of automation of the latter.
the ordering (if any) to use. The user can select among two options:
1. prolog: the standard Prolog total ordering over terms (see the SICStus manual for details),
2. none: the ordering is disabled.

Choosing an appropriate order is important for the particular form of rewriting we have adopted in Constraint Contextual Rewriting and hence in RDL. We perform a form of ordered (conditional) rewriting for which we assume that there exists a total ordering over ground terms. The ordering is also important for the augmentation heuristics. (For details, see the paper [ccr-frocos2000].)

Then after issuing the command

run(zhang_la_bis, la, prolog).

RDL tries to simplify the input clause until it finds the simplified clause specified by the user or it is not able to perform more simplification steps. In the case of our example, the output of RDL should be similar to the following:

Problem: zhang_la_bis  
Decision Procedure: linear arithmetic with augmentation disabled.
Ordering: Standard.
Input Formula: 		[x*y rem x=0,x=<0]
Expected Formula: 	[true]
Simplified Formula: 	[true]
Status: ok!
Strategy: osimp:[cl_simp:[cs_extend:[cs_add:[push_poly]],
crew:[crew_rlv:[cxt_entails_true:[cs_extend:[cs_add:
[push_poly>push_poly]]]]]>cxt_entails_true:[cs_extend:
[cs_add:[push_poly]]]]>cl_true]
Time (Elapsed-Theorem Proving): 30-10 msec

Firstly, RDL reminds the problem it is dealing with. Then, it recalls the decision procedure used and if augmentation is enabled, which ordering is used, the input clause, and the user-expected clause. Then, after some simplification activity, it prints the ok status if it was able to find a simplification strategy that reduces the input clause to the one desired by the user, failed otherwise. Then it prints the simplified clause and then, the simplification strategy, i.e. the combination of Constraint Contextual Rewriting rules that allows to reduce the input to the output clause. The last line reports the timings: the former is the time elapsed from the moment the user entered the run command and the latter is the time devoted to searching for the expected output clause.

There is one command of RDL that we have not covered above: the predicate pred_sym. Its use is best illustrated with the following problem:

description(bm95, 
'Alessandro Armando', 
'This is an example taken from the paper 
"Integrating Decision Procedures in Heuristic Theorem Provers: ..."
by Boyer and Moore, page 95.  Notice that we must disable the ordering.').
pred_sym(bm95, memb(_,_)).
fact(bm95, len_del_less_len, [memb(X,S)],len(del(X,S))< len(S)). 
input(bm95, [not(w>=0), not(k>=0), not(z>=0), not(v>=0),
             not(memb(z,b)),not(w+len(b)=< k), w+len(del(z,b))< k+v]). 
expected_output(bm95, la_aug, none, [true]).

The line pred_sym(bm95, memb(_,_)). tells RDL to consider `memb' as an interpreted predicate symbol by the decision procedure (similarly to, e.g., > and >= for the linear arithmetic decision procedure) because it appears in the precondition of the fact: fact(bm95, len_del_less_len, [memb(X,S)],len(del(X,S))< len(S)).

[ Home | Overview | Publications | Software: RDL Tutorial | Related links ]

This web site is maintained by the AI-Lab webmaster.
Last updated: 14-Dec-2006