next up previous
Next: 5 Predicates and Functions Up: 4 Syntax Previous: 4.1 First-Order Logic

4.2 MLN Syntax

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

This syntax allows you to compactly express a relational Markov network in Markov logic.

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

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 $n$ conjuncts in a formula results in $n$ 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.


next up previous
Next: 5 Predicates and Functions Up: 4 Syntax Previous: 4.1 First-Order Logic
Marc Sumner 2010-01-22