For convenience, Alchemy provides three additional operators:
`*`, `+` and `!`. When predicates in a formula are preceded
by `*`, Alchemy considers all possible ways in which `*` can be
replaced by `!`, e.g., `*student(x) ^ *professor(x)` is
expanded into four formulas:
0in

`student(x) ^ professor(x)``!student(x) ^ professor(x)``student(x) ^ !professor(x)``!student(x) ^ !professor(x)`

The `+` operator makes it possible to learn ``per constant'' weights.
When a variable in a formula is preceded by `+`, a separate weight is
learned for each formula obtained by grounding that variable to one of
its values. For example, if the input formula is `hasPosition(x,+y)`, a
separate weight is learned for the three formulas:
0in

`hasPosition(x,Faculty)``hasPosition(y,Faculty_adjunct)``hasPosition(y,Faculty_emeritus)`

If multiple variables are preceded by `+`, a weight is learned for each
combination of their values. When there are multiple databases, only those
containing the constant generated by the `+` operator contribute to the
weight.

The `!` operator allows you to specify variables that have mutually
exclusive and exhaustive values. For example, if the predicate
`hasPosition(x, y!)`
is declared, this means that any person has exactly one position
(all groundings for this person build one block).
This constraint is enforced when performing inference and learning: it is
guaranteed that exactly one grounding per block is true.
Note that the `!` appears after a variable. `!` can only be used in a
predicate declaration, and can be applied to any number of the predicate's
variables.

You can include comments in the `.mln` file with `//`
and `/* */` like in C++.

The characters `@` and `$` are reserved and should not be used. Due to
the internal processing of functions, variable names should not start with
`funcVar` and predicate names should not start with `isReturnValueOf`.

A formula in an `.mln` file can be preceded by a number representing the
weight of the formula. A formula can also be terminated by a
period (`.`), indicating that it is a hard formula.
However, a formula cannot have both a weight and a period.
In a formula, you can have a line break after
`=>`, `<=>`, `^` and `v`.

A legal identifier is a sequence of alphanumeric characters plus the
characters `-` (hyphen), `_` (underscore), and `'` (prime);
`'` cannot be the first character. Variables in formulas must begin with
a lowercase letter, and constants must begin with an uppercase one.
Constants may also be expressed as strings
(e.g., `Alice` and ```A Course in Logic''`
are both acceptable as constants).

Alchemy converts input formulas into CNF. This means that a conjunction of conjuncts in a formula results in formulas. In an effort to preserve the original formula as much as possible, Alchemy keeps all single literals in a conjunction together by negating the formula: the weight is negated and the formula becomes a disjunction of the negated literals. For instance, the formula

`2 P(x) ^ Q(x) ^ (R(x) v S(x))`

results in the two formulas

`-1 !P(x) v !Q(x)` and

`1 R(x) v S(x)`.

This is the default behavior of Alchemy; however, one can also declare parts of formulas to be indivisible. This is achieved by using square brackets around the part of the formula which should not be separated. If we revisit the previous example and we want to preserve, say, the last three literals, then we can declare

`2 P(x) ^ [ Q(x) ^ (R(x) v S(x)) ]`

which results in

`1 P(x)`

`0.5 Q(x)` and

`0.5 R(x) v S(x)`.

Here, the last two clauses are bound together when performing inference, menaing either both or none of them can be satisfied at any given point during inference.

Note that Alchemy does not use Skolemization to remove existential
quantifiers when converting a formula to CNF. Instead, it replaces
existentially quantified subformulas by disjunctions of all their
groundings. (Skolemization is sound for resolution, but not sound in
general.) For example, when there are only two constants `Alice`
and `Bob`, the formula
`EXIST x,y advisedBy(x,y)` becomes: `advisedBy(Alice,Alice) v
advisedBy(Alice,Bob) v
advisedBy(Bob,Alice) v advisedBy(Bob,Bob)`.
This may result in very large CNF formulas, and existential quantifiers
(or negated universal quantifiers) should be used with care.

Types and constants can be declared in an `.mln` file with the following
syntax: `<typename> = { <constant1>, <constant2>, ... }`,
e.g., `person = { Alice, Bob }`.
You can also declare integer types, e.g.,
`ageOfStudent = { 18, ..., 22 }`.
You may have a line break between
constants. Each declared type must have at least one constant.
A constant is considered to be declared the first time it is
encountered in a type declaration, a formula, or a ground atom
(in a`.db` file).

You can include other `.mln` files in a `.mln` file with the
`"#include" ` keyword. For example, you can include formulas about
a university domain in your `.mln` file about a company domain with
`#include "university.mln"`.

The executables will print out error messages when they encounter syntax or semantic errors. Each message will indicate the line and column number of the error (lines start from 1 and columns from 0). An error may not be exactly at the indicated column but near it, and an error may also be a result of previous ones (much like compiler error messages).

Predicates and functions play a large role in Alchemy and this topic (including syntax) is covered extensively in the next section.