Abstract

This note describes the syntax and semantics of the Domain Definition Language, FDDL, a specification language for finite domains. The language provides rudimentary facilities for specifying structures with a fixed finite domain, equipped with a collection of subsets (known as types), a collection of relations, and some uninterpreted predicates.

In addition, FDDL provides a syntax for typed first-order logic (without function symbols).

A domain specification fixes the underlying structure of elements, types, and relations. Our aim is to find and count the ways in which the predicates may then be interpreted over this structure to satisfy given axioms.

PropSat is a BDD-based package for counting and finding models for FDDL domains.

1 Introduction

This note describes the syntax and semantics of the Finite Domain Definition Language, (FDDL). The language provides rudimentary facilities for specifying finite structures, and a syntax for typed first-order logic (without function symbols).

2 Domains

A domain, is a finite set, D, equipped with a set, T P(D), of types (fixed subsets of the domain), a number of fixed relations (of various typed arities), and a signature, S, specifying a number of predicates, and their typed arities. (Although types correspond semantically to unary relations, in the current implementation, types are not syntactically available as unary relations-they can only be used to restrict the range of a quantified variable.)

Once we have specified a domain, we can ask whether the predicates have interpretations making a given formula in first-order predicate calculus, true. We can count the number of interpretations making a given formula, or axiom, true, and exhibit one such, if any there be.

3 A Simple Example

To give a flavour of the language, consider the following problem. There are eight teams in a tournament. Each team must play exactly three others. How many ways are there to arrange such a tournament? Find one.

Of the 268,435,456 irreflexive symmetric relations on eight elements, 19,355 represent valid ways to order the tournament. Here is one of them:

All domains include the built-in type, object, interpreted as the underlying set of the domain, and the equality relation, =. Most domains, like our examples, define further types, interpreted as subsets, and further predicates. FDDL provides syntax for specifying type inclusions.

Elements of the domain are specified by constants (whose interpretations are assumed to be distinct).

The two features of the language not exhibited by these examples are facts and relations. These will be introduced in due course.

4 Syntactic Notation

Our notation is an Extended BNF (EBNF) with the following conventions:

• Each rule is of the form <syntactic element> ::= expansion.
• Angle brackets delimit names of syntactic elements.
• Square brackets ([ and ]) surround optional material.
• An asterisk (*) means “zero or more of”; a plus (+) means “one or more of.”
• Some syntactic elements are parameterized. E.g., <list (symbol)> might denote a list of symbols, where there is an EBNF definition for <list x> and a definition for <symbol>. The former might look like

  <list x> ::= (x*)

  so that a list of symbols is just (<symbol>*).
• Ordinary parentheses are an essential part of the syntax we are defining and have no semantics in the EBNF meta language.

Comments in FDDL begin with a semicolon (“;”) and end with the next newline. Any such string behaves like a single space.

5 Syntax

We now describe the language more formally. The EBNF for defining a domain structure is:

Names of domains, like other occurrences of syntactic category <name>, are strings of characters beginning with a letter and containing letters, digits, hyphens (“-”),and underscores (“_”). Case is not significant.

The :types argument uses a syntax borrowed from McDermott’s NISP:

If this occurs as a :types argument to a domain, it declares four new types, integer, number, float, and physob. The first two are subclasses of number, all are subclasses of object (by default). That is, every integer is a number, every float is a number; every number, and every physical object, is an object.

In addition to atomic type names, there are union types (either t₁ ...t_k) is the union of types t₁ to t_k.

The :constants field has the same syntax as the :types field, but the semantics is different. Now the names are taken as new constants in this domain, whose types are given as described above. E.g., the declaration

indicates that in this domain there are three distinguished constants, sahara denoting a theater and two symbols denoting divisions. An object may be declared repeatedly to belong to any number of types; the types are just subsets of the finite set of all declared objects.

The :predicates field consists of a list of declarations of predicates, once again using the typed-list syntax to declare the arguments of each one.

The syntax <literal(name)> will be defined in Section 6.

6 Formulae

FDDL axioms are quite expressive. All of function-free first-order predicate logic (including nested quantifiers) is allowed. Numeric quantifiers are provided.

FDDL facts are (much) more restrictive: only universal horn formulae are allowed. Since we are dealing with only finite domains these can be syntactically slightly more relaxed than usual. Positive formulae are built from relation atoms using and and forall. Horn formulae are built from positive formulae using universal quantification and, at most, a single implication.

Warning: An occurrence of a <predicate> should agree with its declaration in terms of number and, when applicable, types of arguments. In the current implementation, declarations of predicates are permitted, but neither required nor used to check that predicates are applied consistently. Declarations of relations are used -- they are used in facts and a closed-world assumption is applied to them. However, the types and number of their arguments are not checked.

7 Semantics

The semantics of most of these expressions is standard. The numeric quantifiers are interpreted as expressing that there are particular numbers of instantiations of the (tuple of) quantified variables making the body true. Thus, for example, (exists (?x) <phi>) is equivalent to (>= 1 (?x) <phi>).

Facts have a closed-world semantics. This means that relations are given a minimally true interpretation. A particular instantiation of a relation is true iff it is implied by the facts. Since the facts are universal Horn sentences, this gives a structure consistent with the facts -- i.e.the facts are true in this interpretation.

8 Checking Propositional Satisfiability

PropSat is a tool written in ML to check the satisfiability of FDDL specifications. It translates specifications to propositional form and uses David Long’s LIBBDD library to check satisfiability.

PropSat onLine

propsat can be invoked online at http://homepages.inf.ed.ac.uk/mfourman/propsat/.

PropSat@Edinburgh

propsat can be invoked locally (on DICE machines within Informatics) by running the script at/home/mfourman/bin/propsat. This puts you into an interactive PolyML session where propsat is available.

Usage: at the ml prompt < type propsat "<domain-file>";

To exit the ML session use control-C to interrupt the ML interpreter, and then type q (or ? for other options).

Example domain files can be found at

http://www.inf.ec.ac.uk/teaching/courses/propm/domains