<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">\documentstyle[fleqn,11pt]{article}
%\documentstyle[fleqn,11pt,citestyle]{article}

%\input{epsf.sty}

\pagestyle{empty}
\pagenumbering{arabic}

\setlength{\topmargin}{-0.4in}
\setlength{\textheight}{8.5in}
\setlength{\oddsidemargin}{0.2in}
\setlength{\textwidth}{6in}


\newcommand{\eg}{{\it e.g.}}
\newcommand{\ie}{{\it i.e.}}

\newcommand{\ucpop}{\mbox{\sc ucpop}}
\newcommand{\lang}{\mbox{\sc PDDL}}
\newcommand{\fddl}{\mbox{\sc FDDL}}
\newcommand{\prodigy}{\mbox{\sc prodigy}}
\newcommand{\zeno}{\mbox{\sc zeno}}
\newcommand{\clpr}{\mbox{CLP({$\cal{R}$})}}
\newcommand{\HOLDS}{\mbox{\tt holds-at}}
\newcommand{\VALUE}{\mbox{\tt value-at}}



\newcommand{\?}{\mbox{?}}
\newcommand{\bi}{\begin{itemize}}
\newcommand{\ei}{\end{itemize}}
\newcommand{\ddt}{\mbox{$\frac{d}{dt}\,$}}  %* no strut
\newcommand{\PS}{\mbox{$\prec\!\! S, O, B\!\! \succ$}} % plan state
\newcommand{\SPP}{\mbox{$\prec\!\! {\cal O}, \Sigma, \Omega \!\!\succ$}}
\newcommand{\comment}[1]{}
\newtheorem{defn}{Definition}
\newcommand{\clink}[3]{\mbox{${#1}\!\!\stackrel{#2}{\rightarrow}\!\!{#3}$}}
\newcommand{\hlink}[3]{\mbox{${#1}\!\!\stackrel{#2}{\rightarrow *}\!\!{#3}$}}
\newcommand{\bug} {\mbox{\rule{4mm}{4mm}}}
\newcommand{\Bug}[1]{\mbox{\rule{4mm}{4mm}}\footnote{{\bf BUG:} #1}}

\newtheorem{them}{Proposition}
\newtheorem{lemma}[them]{Lemma}
\newtheorem{corol}[them]{Corollary}
\newtheorem{conj}[them]{Conjecture}
\newtheorem{example}{Example}

\newcommand{\goal}[1]{\prec\!\!{#1}\!\!\succ}
\newcommand{\PDB}{\mbox {\sc pdb}}
\newcommand{\pdb}{\PDB}

\setcounter{tocdepth}{2}

\def\oom{$^{\tt +}$}
\def\zom{$^*$}
\def\bump{\hspace{1cm}}
\def\req#1{$^{\tt #1}$}
\newenvironment{tabtt}{\begin{tt}\begin{tabbing}}{\end{tabbing}\end{tt}}
\def\noteme#1{}%{[[#1]]}
\def\notecoauth#1{\ }
\def\notereader#1{[[#1]]}
\def\meta{$\uparrow\uparrow$}
\def\la{\langle}
\def\ra{\rangle}

\begin{document}
\pagenumbering{footnote}
\pagestyle{empty}
\thispagestyle{empty}
\comment{\maketitle}

\begin{center}
{\bf {\LARGE \fddl{} --- Finite Domain Definition Language}} \\
\date{18 February 2003}

\vspace{1cm}

Adapted from the PDDL manual produced by the AIPS-98 Planning Competition
Committee \\
\vspace{1cm}
Michael P Fourman\\

\vspace{1cm}

Institute for Communicating and Collaborative Systems\\
Institute for Intelligent Systems and their Applications\\
Laboratory for Foundations of Computer Science\\
Informatics \\
The University of Edinburgh 
\end{center}



\vspace{0.8in}
{\large\bf 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.
\newpage

\pagestyle{plain}
%\pagenumbering{roman}
%\tableofcontents

%\newpage
\pagenumbering{arabic}

\section{Introduction}
\label{intro}

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

\section{Domains}
A domain, is a finite set, $\mathcal{D}$, equipped with a set,
$\mathcal{T}\subseteq {\large\mathcal{P}}( \mathcal{D})$, of
\emph{types} (fixed subsets of the domain), a number of fixed
relations (of various typed arities), and a \emph{signature},
$\mathcal{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 \emph{axiom}, true, and exhibit one such, if any
there be.

\section{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.

\begin{verbatim}
(define (domain tournament)
  (:types team)
  (:constants t0 t1 t2 t3 t4 t5 t6 t7 - team)
  (:predicates (plays ?x ?y - team))
  (:axioms
    (forall (?x - team) (not (plays ?x ?x)))                  ;irreflexive
    (forall (?x ?y - team) (iff (plays ?x ?y) (plays ?y ?x))) ;symmetric
    (forall (?x - team) (= 3 (?y - team) (plays ?x ?y)))
   )
  )             
\end{verbatim}
This domain has one type, with eight elements. We search for graphs
with this set of nodes, such that each node has degree three ---
binary relations which are irreflexive, symmetric, and have the
required property.

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:
\begin{verbatim}
      ["(plays t7 t6)", "(plays t6 t7)", "(plays t7 t5)", "(plays t5 t7)",
       "(plays t6 t5)", "(plays t5 t6)", "(plays t7 t4)", "(plays t4 t7)",
       "(plays t6 t4)", "(plays t4 t6)", "(plays t5 t4)", "(plays t4 t5)",
       "(plays t3 t2)", "(plays t2 t3)", "(plays t3 t1)", "(plays t1 t3)",
       "(plays t2 t1)", "(plays t1 t2)", "(plays t3 t0)", "(plays t0 t3)",
       "(plays t2 t0)", "(plays t0 t2)", "(plays t1 t0)", "(plays t0 t1)"]
\end{verbatim}
Suppose we now elaborate the example. There are three junior and five
senior teams. We want to ensure that each junior team plays at least
one junior team, and each senior team at least one senior team.

\begin{verbatim}
(define (domain tournament)
  (:types junior senior - team)
  (:constants t0 t1 t2 - junior t3 t4 t5 t6 t7 - senior)
  (:predicates (plays ?x ?y - team))
  (:axioms
    (forall (?x - team) (not (plays ?x ?x)))
    (forall (?x ?y - team) (iff (plays ?x ?y) (plays ?y ?x)))
    (forall (?x - junior)(exists (?y - junior) (plays ?x ?y)))
    (forall (?x - senior)(exists (?y - senior) (plays ?x ?y)))  
    (forall (?x - team)(= 3 (?y - team) (plays ?x ?y)))
   )
  )
\end{verbatim}
The \texttt{types} declaration introduces junior and senior as
subtypes of team. The \texttt{constants} declaration introduces the
eight teams, within their respective subtypes.

All domains include the built-in type, {\tt object}, interpreted as
the underlying set of the domain, and the equality relation,
\texttt{=}.  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.
\section{Syntactic Notation}

Our notation is an Extended BNF (EBNF) with the following conventions:
\begin{itemize}
\item Each rule is of the form {\tt &lt;{\it syntactic element}&gt; ::= {\it expansion}}.

\item Angle brackets delimit names of syntactic elements.

\item Square brackets ({\tt [} and {\tt ]})  surround 
optional material. 

\item An asterisk ({\tt *})  means ``zero or more
of''; a  plus ({\tt +})  means ``one or more of.''

\item 
  Some syntactic elements
are parameterized.  E.g., {\tt &lt;list (symbol)&gt;} might denote a list of
symbols, where there is an EBNF definition for {\tt &lt;list $x$&gt;} and
a definition for {\tt &lt;symbol&gt;}.  The former might look like
\begin{tabtt}
\bump &lt;list $x$&gt; ::= ($x$*)
\end{tabtt}
so that a list of symbols is just {\tt (&lt;symbol&gt;*)}.

\item Ordinary parentheses are an essential
part of the syntax we are defining and have no semantics in the EBNF meta
language.
\end{itemize}

Comments in \fddl{} begin with a semicolon (``{\tt ;}'') and end with
the next newline.  Any such string behaves like a single space.

\section{Syntax}
\label{syntax}
 
We now describe the language more formally. The EBNF for defining a
domain structure is:

\begin{tabtt}
\bump \= &lt;domain&gt; \bump\bump\=::= (def\=ine (domain &lt;name&gt;)\+\+\+\\
                        {[}&lt;types-def&gt;] \\
                        {[}&lt;constants-def&gt;] \\
                        {[}&lt;relations-def&gt;] \\
                        {[}&lt;predicates-def&gt;] \\
                        {[}&lt;facts-def&gt;] \\
                        {[}&lt;axioms-def&gt;]) \-\-\\
  &lt;types-def&gt;    \&gt; ::= (:types &lt;typed list (name)&gt;) \\
  &lt;constants-def&gt; \&gt;::= (:constants &lt;typed list (name)&gt;) \\
  &lt;relations-def&gt; \&gt; ::= (:relations &lt;atomic formula skeleton&gt;\oom) \\
  &lt;predicates-def&gt; \&gt; ::= (:predicates &lt;atomic formula skeleton&gt;\oom) \\
  &lt;facts-def&gt; \&gt; ::= (:facts &lt;positive formula&gt;\oom) \\
  &lt;axioms-def&gt; \&gt; ::= (:axioms &lt;formula&gt;\oom) \\
  &lt;atomic formula skeleton&gt; \\
                \&gt; ::= (&lt;predicate&gt; &lt;typed list (variable)&gt;) \\
  &lt;predicate&gt; \&gt; ::= &lt;name&gt; \\
  &lt;variable&gt; \&gt; ::= ?&lt;name&gt; 
\end{tabtt}

The optional components of a domain may come in any order. Just one
\fddl{} definition of a domain may appear per file.

Names of domains, like other occurrences of syntactic category {\tt
&lt;name&gt;}, are strings of characters beginning with a letter and
containing letters, digits, hyphens (``-''),and underscores (``\_'').
Case is not significant. 

\noteme{Say more somewhere}

The {\tt :types} argument uses a syntax borrowed from McDermott's NISP:

\begin{nopagebreak}\begin{tabtt}
\bump\=  &lt;typed($x$)&gt; \=::= $x$\oom - &lt;type&gt;\+\\
 &lt;typed($x$)&gt; \=::= $x$\zom\\
  &lt;typed list ($x$)&gt; \=::= &lt;typed ($x$)&gt;\zom\\
  &lt;type&gt;\&gt; ::= &lt;name&gt; \\
  &lt;type&gt; \&gt; ::= (either &lt;type&gt;\oom) \\
\end{tabtt}\end{nopagebreak}

A typed list is used to declare the types of a list of entities; the types
are preceded by a minus sign (``{\tt -}''), and every other element of the list
is declared to be of the first type that follows it, or {\tt object} if there
are no types that follow it.
An example of a  {\tt &lt;typed list(name)&gt;} is 
\begin{center}
{\tt integer float - number physob}  
\end{center}
If this occurs as a 
{\tt :types} argument to a domain, it declares four new types, {\tt integer}, \texttt{number},
{\tt float}, and {\tt physob}.  The first two are subclasses of {\tt number},
all are subclasses of {\tt 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 {\tt (either
  $t_1$ \ldots $t_k$)} is the union of types $t_1$ to $t_k$.

The {\tt :constants} field has the same syntax as the {\tt :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
\begin{tabbing}
\bump \tt (:constants \= sahara - theater \\
                      \&gt; division1 division2 - division)
\end{tabbing}
indicates that in this domain there are three distinguished constants,
{\tt sahara} denoting a {\tt theater} and two symbols denoting {\tt
  division}s. 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 {\tt :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 {\tt &lt;literal(name)&gt;} will be defined in Section~\ref{gd}.
\section{Formulae}
\label{gd}

\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 \texttt{and} and \texttt{forall}.
Horn formulae are built from positive formulae using universal
quantification and, at most, a single implication.


\begin{tabtt}
 \= &lt;formula&gt; \hspace{2cm} \= ::= &lt;atomic formula(term)&gt; \+\\
  &lt;formula&gt; \&gt; ::= &lt;literal(term)&gt; \\
  &lt;formula&gt; \&gt; ::= (and &lt;formula&gt;\zom) \\
  &lt;formula&gt; \&gt; ::= (or  &lt;formula&gt;\zom) \\
  &lt;formula&gt; \&gt; ::= (not &lt;formula&gt;) \\
  &lt;formula&gt; \&gt; ::= (imply &lt;formula&gt; &lt;formula&gt;) \\
  &lt;formula&gt; \&gt; ::= (iff &lt;formula&gt; &lt;formula&gt;) \\
\smallskip
  &lt;formula&gt;\&gt; ::=
             (exists (&lt;typed list(variable)&gt;) &lt;formula&gt; )\\ 
\smallskip
  &lt;formula&gt;\&gt; ::=
            (forall (&lt;typed list(variable)&gt;) &lt;formula&gt; ) \\  
\smallskip
  &lt;formula&gt;\&gt; ::=
            (&lt; &lt;num&gt; (&lt;typed list(variable)&gt;) &lt;formula&gt; ) \\  
  &lt;formula&gt;\&gt; ::=
            (= &lt;num&gt; (&lt;typed list(variable)&gt;) &lt;formula&gt; )\\  
  &lt;formula&gt;\&gt; ::=
            (&gt; &lt;num&gt; (&lt;typed list(variable)&gt;) &lt;formula&gt; ) \\  
  &lt;formula&gt;\&gt; ::=
            (=&lt; &lt;num&gt; (&lt;typed list(variable)&gt;) &lt;formula&gt; )\\  
  &lt;formula&gt;\&gt; ::=
            (&gt;= &lt;num&gt; (&lt;typed list(variable)&gt;) &lt;formula&gt; )\\  
  &lt;horn formula&gt; \&gt; ::= &lt;positive formula&gt; \\
  &lt;horn formula&gt; \&gt; ::= (imply &lt;positive formula&gt; &lt;positive formula&gt;) \\
  &lt;horn formula&gt;\&gt; ::=
            (forall (&lt;typed list(variable)&gt;) &lt;horn formula&gt; ) \\  
  &lt;positive formula&gt; \&gt; ::= &lt;atomic formula(term)&gt; \\
  &lt;positive formula&gt; \&gt; ::= (and &lt;positive formula&gt;\zom) \\
  &lt;positive formula&gt; \&gt; ::=
            (forall (&lt;typed list(variable)&gt;) &lt;positive formula&gt; ) \\  
  &lt;literal($t$)&gt; \&gt;::= &lt;atomic formula($t$)&gt; \\
  &lt;literal($t$)&gt; \&gt;::= (not &lt;atomic formula($t$)&gt;) \\
  &lt;atomic formula($t$)&gt; \&gt;::= (&lt;predicate&gt; $t$\zom) \\
  &lt;term&gt; \&gt; ::= &lt;name&gt; \\
  &lt;term&gt; \&gt; ::= &lt;variable&gt; 
\end{tabtt}

\noindent where the category \texttt{&lt;num&gt;} represents natural numbers, represented in decimal notation. 

\textbf{Warning:} An occurrence of a {\tt &lt;predicate&gt;}
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.


\section{Semantics}
\label{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, \texttt{(exists (?x) &lt;phi&gt;)}
is equivalent to \texttt{(&gt;= 1 (?x) &lt;phi&gt;)}.

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 --- \ie the facts are true in this interpretation.

\section{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.

\subsection*{PropSat onLine}
\texttt{propsat} can be invoked online at \texttt{http://homepages.inf.ed.ac.uk/mfourman/propsat/}.
\subsection*{PropSat@Edinburgh}
\texttt{propsat} can be invoked locally (on DICE machines within Informatics)
by running the script at\texttt{/home/mfourman/bin/propsat}. This puts
you into an interactive PolyML session where propsat is available.

\textbf{Usage:} at the ml prompt \verb!&lt;! type \texttt{propsat
  "}$\langle$\textit{domain-file}$\rangle$\texttt{";}

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

Example domain files can be found at 

\texttt{http://www.inf.ec.ac.uk/teaching/modules/propm/domains}
\newpage
\bibliographystyle{plain}

%\nocite{barrett-aaai94}
%\nocite{carbonell-prodigy-manual}
%\nocite{tate-oplan2-manual}

%\bibliographystyle{yalethesis}
\bibliography{uw,biblio}
%\bibliography{/u/jsp/tex/general}


\end{document}


 

</pre></body></html>