User Manual

User Manual Back to Home Page

1. Encoding in F2LP
2. Domain and domain variable declarations
3. Lparse and gringo rules
4. Built-in predicates and functions
5. New predicates and variables introduced
6. Aggregate Expressions
7. Reserved characters and keywords
8. Extensional predicates
9. Strong Negation and Backward Compatibility
10. Configuration Options
11. Invoking F2LP and F2LP options
12. Debugging
13. Temporary files created
14. Limitations
15. Future work

Encoding in F2LP

Atoms and variables are represented as in lparse and gringo.
An F2LP rule is of the form
F <- G.
where F and G are first-order formulas, which can be encoded using the following ASCII representations:

conjunction	disjunction	implication	default negation	strong negation	true	falsity	forall x,y,z	exists x,y,z
&	\|	->	not	-	true	false	![X,Y,Z]:	?[X,Y,Z]:

Note that each rule must end with a dot(.).

An F2LP encoding is a set of F2LP rules.

The arrow (<-) symbol has no special meaning.
It is just implication written backwards in order to make F2LP logic programming friendly.
For example, p -> q and q <- p have the same meaning.

In F2LP, the precedence for the quantifiers is same as the precedence for default negation.
This implies that the third occurrence of X in ?[X]:p(X) & q(X) is considered to be free.
The formula ?[X]:(p(X) & q(X)) has no free occurrences of variables.

up Back to Home Page

Domain and domain variable declarations

The domain and domain variable declarations are similar to the declarations in lparse and gringo.
For example, the following line declares the domain of object to be {a,b,c}:
object(a;b;c).
The following line declares X and Y as variables ranging over the domain of "object":
#domain object(X;Y).

The following is a complete example:
% file example1.fof
% domain from 0 to 9
number(0..9).
% domain variables X and Y
#domain number(X;Y).
r(1).
s(X) <- r(X) & not ?[Y]:(p(X,Y) & q(X,Y)).

up Back to Home Page

Lparse and gringo rules

F2LP supports rules in lparse and gringo syntax. These rules are simply copied to the output.
The following is an example:
% file example2.fof
% domain {a,b,c}
object(a;b;c).
% domain variable X
#domain object(X).
p(a).
r(c).
q(b) <- ?[X]:(p(X) & r(X)).
% rule in lparse/gringo syntax
q(X) :- p(X), not r(X).

up Back to Home Page

Built-in predicates and functions

F2LP supports the following built-in predicates and functions:

eq(X,Y)	assign(X,Y)	neq(X,Y)	lt(X,Y)	le(X,Y)	gt(X,Y)	ge(X,Y)
X==Y	X=Y	X!=Y	X<Y	X<=Y	X>Y	X>=Y

X+Y

X-Y

X*Y

X/Y

X mod Y (X \ Y)

X^Y (xor)

#abs(X)

For built-in predicates, either representation can be used. For example, if F2LP encounters neq(X,a), it will simply turn it to X != a.

up Back to Home Page

New predicates and variables introduced

In order to eliminate positive occurrences of the existential quantifier and negative occurrences of the universal quantifier,
F2LP introduces new predicates "_new_pred_*",
where * is a number that is incremented every time a new predicate is introduced.
For this reason names of the form "_new_pred_1", "_new_pred_2", etc. should not be used for encoding in F2LP.

The following is an example that shows introduction of new predicates:
% Begin F2LP input
% file example1.fof
% domain from 0 to 9
number(0..9).
% domain variables X and Y
#domain number(X;Y).
r(1).
s(X) <- r(X) & not ?[X]:(p(X,Y) & q(X,Y)).
% End F2LP input

Run F2LP:
f2lp example1.fof

% Begin F2LP output
number(0..9).
#domain number(X;Y).
r(1) :- true.
s(X) :- r(X), not _new_pred_1(Y).
_new_pred_1(Y) :- p(X,Y), q(X,Y).
true.
:- false.
#hide true.
% End F2LP output
Here "_new_pred_1" is the new predicate introduced by F2LP.

In order to eliminate negative occurrences of the existential quantifier and positive occurrences of the universal quantifier,
F2LP introduces new variables "_NV_*", where * is a number that is incremented every time a new variable is introduced.
For this reason, variables of the form "_NV_1", "_NV_2", etc. should not be used for encoding in F2LP.

The following is an example that demonstrates how F2LP introduces new variables.
% Begin F2LP input
% file example2.fof
% domain {a,b,c}
object(a;b;c).
% domain variable X
#domain object(X).
p(a).
r(c).
q(b) <- ?[X]:(p(X) & r(X)).
% End F2LP input

% Begin F2LP output
object(a;b;c).
#domain object(X).
p(a) :- true.
r(c) :- true.
#domain object(_NV_1).
q(b) :- p(_NV_1), r(_NV_1).
true.
:- false.
#hide true.
% End F2LP output
Here "_NV_1" is the new variable introduced which has the same domain as the variable it replaced (X).

up Back to Home Page

Aggregate Expressions

F2LP supports lparse, gringo and dlv aggregates.
However, since the current versions of gringo and lparse do not support dlv aggregates,
the output of F2LP cannot be understood by lparse and gringo if dlv aggregates are used.

F2LP treats aggregate expressions as atoms. As a result, they can also be used in the scope of quantifiers.
In order to handle aggregates, F2LP internally converts them to atoms of the form "_agg_exp_*".
So, names beginning with "_agg_exp_" are reserved for use by F2LP.
F2LP does not support nested aggregates (aggregates within aggregates).

Example:
{p(X):q(X)} & r(Y) <- s(Y) & not 2{t(X,Z,Z):s(Z)}.
{p(X)} <- #sum[t(X,Y,Z):r(Z):q(Y),s(X)]5 | s(X).

is turned to

{p(X):q(X)} :- s(Y), not 2{t(X,Z,Z):s(Z)}.
r(Y) :- s(Y), not 2{t(X,Z,Z):s(Z)}.
{p(X)} :- #sum[t(X,Y,Z):r(Z):q(Y),s(X)]5.
{p(X)} :- s(X).

up Back to Home Page

Reserved characters and keywords

The following characters and keywords are reserved for use by F2LP:

_new_pred_*

_NV_*

_agg_exp_*

lparse built-in names (eq, ge, mod, etc)

Extensional predicates

F2LP allows predicates to be extensional.
Predicates can be declared as extensional by using the keyword "extensional" as follows:
#extensional p(X,Y).

The above line declares the predicate p to be extensional.
Here X and Y have to be domain variables. This is because F2LP cannot automatically identify the domain of the arguments of predicates.
When F2LP encounters the above line, it just replaces it with the choice rule
{p(X,Y)}.

up Back to Home Page

Strong Negation and Backward Compatibility

For the sake of backward compatibility, F2LP treats the symbol "-" as default negation under certain circumstances:
(a) if the description contains the F2LP arrow (<-), then "-" is treated as strong negation;
(b) if the description does not contain the F2LP arrow but contains implication, then "-" is treated as default negation;
(c) if neither F2LP arrow nor implication are found, then "-" is treated as strong negation.

F2LP also provides run time options to set "-" to either strong negation or default negation.
See Section Invoking F2LP and F2LP options for further details.

If "-" is used for default negation, then strong negation can be represented using "~".
For example, the following (complete) description uses "-" for default negation and "~" for strong negation
(note the absence of F2LP arrow (<-)):

object(a;b;c).
#domain object(X;Y).
p(X) & -?[Y]:q(X,Y) -> ~r(X).

up Back to Home Page

Configuration Options

The following parameters are configurable:

Parameter	Macro	Default value
Maximum length of any formula	LINE_MAX	as defined in "limits.h"
Maximum length of any atomic formula	MAX_PREDICATE_LENGTH	500 bytes
Maximum number of connectives and arithmetic operators in a formula	MAX_SYMBOLS	500

F2LP can be compiled using gcc. The following line should work with most gcc distributions:
gcc f2lp.c -o f2lp

The above command line sets the configurable parameters to default values.
LINE_MAX is by default set to the value defined in "limits.h". If LINE_MAX is not defined in "limits.h", then the value is set to 2048 bytes.
The parameter values can be defined by the user during compile time.
The following line sets LINE_MAX to 1000 bytes, MAX_PREDICATE_LENGTH to 50 bytes and MAX_SYMBOLS to 20.
gcc -D LINE_MAX=1000 -D MAX_PREDICATE_LENGTH=50 -D MAX_SYMBOLS=20 f2lp.c -o f2lp

up Back to Home Page

Invoking F2LP and F2LP options

Input can be provided to F2LP through STDIN or file interface:
f2lp input_file_1 input_file_2 . . . input_file_n

If no input file is provided, STDIN is considered.
For example, using the following command line is equivalent to providing input_file as an argument to F2LP:
cat input_file | f2lp

Other run time options are as follows:
1. -h, --h, -help, --help : displays all options.
2. -v, --v, -version, --version: displays the version number.
3. -d: treat "-" as default negation.
4. -c: treat "-" as classical negation.

up Back to Home Page

Debugging

F2LP can be compiled to output debug information using the following command line:
gcc -D DEBUG f2lp.c -o f2lp

Note that the output of f2lp in this case cannot be directly provided as input to the answer set solvers.

up Back to Home Page

Temporary files created

F2LP creates the following files in the working directory:
(a) .f2lp_input.fof
(b) .solver_input.lp

This implies that the user should have write permissions in the working directory.

up Back to Home Page

Limitations

1. Variables cannot contain any characters other than alphabets, numbers and underscore(_).
2. The domain of a variable might not be identified if it occurs before its declaration as a domain variable.
This does not imply that every variable has to be a domain variable.
It only implies that if the variable needs to be replaced by a new variable during quantifier elimination,
F2LP might not declare the domain of the new variable.

up Back to Home Page

Future work

1. To implement safety preserving transformation.
2. To output programs in the language of DLV.
3. To overcome the limitations described above.

up Back to Home Page