aspmt Files

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).