fasp2smt

Fuzzy Answer Set Programming (FASP) allows to represent and reason on incomplete and imprecise knowledge under stable model semantics. This is a solver based on translations into SMT theories.

Download link: [GitHub].

File README, reported below, should give enough information on how to use the script.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
fasp2smt
========
 
Fuzzy answer set programming solver based on satisfiability modulo theories.
 
Requirements:
 
- gringo 3: http://sourceforge.net/projects/potassco/files/gringo/3.0.5/
 
- z3: http://z3.codeplex.com/releases
 
Commands gringo and z3 are used by fasp2smt. The path to these tools can be specified by using the command-line options --grounder and --solver, respectively.
 
 
Example usage:
 
$ ./fasp2smt.py example.fasp
Answer 1:
    c   0.600000    (3.0/5.0)
    b   0.400000    (2.0/5.0)
    a   0.600000    (3.0/5.0)
 
where example.fasp contains
 
a :- #0.6.
b :- #0.4.
c :- a, ~b.
 
For details on the syntax of input programs, run
 
$ ./fasp2smt.py --help-syntax

Run the script with flag --help-syntax for more instruction.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
$ ./fasp2smt.py --help-syntax
 
FASP programs are sets of rules. Each rule must be written in a single line, and each line can contain at most one rule. A rule has a head and a body, separated by the implication symbol :-, and it is terminated by a dot. For example,
 
    head :- body.
 
Either the head or the body can be omitted. For example, the followings are valid rules:
 
    head.
    head :- .
    :- body.
 
The first two rules above are called facts, and are shortcut for
 
    head :- #1.
 
while the third rule is called constraint, and is a shortcut for
 
    #0 :- body.
 
A head is either an atom, or sequence of atoms separated by a fuzzy connective. For example,
 
    a + b + c :- body.
 
is a rule using Lukasiewicz disjunction as head connective. At most one kind of connective can be used in the same rule head. The available connectives are + (plus; Lukasiewicz disjunction), * (times; Lukasiewicz conjunction), | (pipe; Godel disjunction), and , (comma; Godel conjunction).
 
A body is a possibly nested expression made combining atoms with fuzzy connectives and default negation, where default negation is denoted not or ~. For example,
 
    head :- a * (b + ~c).
 
is a rule whose body is the Lukasiewicz conjunction of atom a with the result of the Lukasiewivz disjunction between atom b and the negation of atom c.
 
Atoms are formed by a predicate and a possibly empty list of arguments. For example,
 
    p :- q(X,0).
 
is a rule whose head is the propositional atom p, and whose body is the atom with predicate q and arguments X (a variable) and 0 (a constant). Note that the arguments use the usual syntax of Prolog/ASP.
 
Atoms can be also numeric constants in the interval [0,1]. For example,
 
    p :- #0.5.
    q :- #1/2.
 
declare p and q to be at least one half.
 
There is a third kind of atom that can be used to specify some arithmetic conditions (and will be used only during the grounding phase). Such atoms are specified in brackets. For example,
 
    p(X) :- #0.5, [X = 1..5].
 
declares p(X) to be at least 0.5 for each substitution of X in [1..5].