Home / Mvsm System Files
Name Modified Size InfoDownloads / Week
Parent folder
readme.txt 2014-05-27 1.4 kB
mvpf2lpCompiler 2014-05-27 112.9 kB
gringo 2014-05-27 7.0 MB
f2lp 2014-05-27 86.3 kB
claspD 2014-05-27 1.8 MB
as2transition 2014-05-27 664.9 kB
Totals: 6 Items   9.7 MB 0
An input encoding consists of a declaration section and a set of multi-valued propositional rules.
The declaration includes sort declarations, object declarations, constant declarations, and variable 
declarations. These define the names of the sorts, the elements in the sorts, the argument and value sorts
for constants, and the sorts of variables respectively. See the examples for details on syntax.


The multi-valued propositional rules are formed using the constants, variables, objects, and propositional
connectives, which include & (conjunction), | (disjunction), -> (implication), <- (reverse direction
implication), not (negation). See the examples for more detailed usage.


Typical invocation of the toolchain will be

mvpf2lpCompiler <FILENAME> -a | f2lp | gringo <CONSTANTS>| claspD | as2transition -eql -l

where <FILENAME> is the name of the input file, <CONSTANTS> are of the form "-c <CONST>=<VALUE>".

See the example outputs for specific examples of the invocations.

Note: The -a flag prepares the translations for post processing by as2transition, while the -eql, -l, -A are
to make as2transition to format the output in the style of multi-valued propositional formula 
(using multivalued symbols, showing full interpretations without omitting boolean functions mapped to 
false, each on a separate line).
Source: readme.txt, updated 2014-05-27