Rulelog: Syntax and Semantics
 Authors:

Benjamin Grosof (Benjamin Grosof & Associates, LLC)
Michael Kifer (Stony Brook University)
 This version:

$Date: 20130531 #$
Rulelog is the logic underlying knowledge representation languages such as
FLORA2 and SILK. It
combines much of the latest work in logic programming,
nonmonotonic reasoning, business rules, and the Semantic Web. It is
designed to be appropriately expressive for supporting knowledge
representation in complex domains, such as sciences and law, and yet to be
efficiently implementable.
This document provides a formal account
of the syntax and semantics of Rulelog.
Copyright ©
2013 retained by the authors. All
Rights Reserved.
Contents
1 Introduction
1.1 Acknowledgments
1.2 Typography
2 Organization of the Document
3 The Syntax of Rulelog
3.1 The Alphabet of Rulelog
3.2 Symbol Spaces and Datatypes
3.3 The Base Language
3.3.1 Terms
3.3.2 Basic Formulas
3.3.3 Compound Formulas
3.3.4 Rules, Facts, and Queries
3.4 Syntactic Extensions
3.4.1 Path Expressions
3.4.2 UserDefined Functions
3.4.3 Statement descriptors
3.4.4 Skolem Constants and Function Symbols
3.4.5 Various Other
3.5 Nonlogical Markup
3.5.1 IRI Prefix and Base Declarations
3.5.2 Comments
3.5.3 Import and Export of Modules
3.5.4 Preprocessor
3.6 Creation of and Loading into Rulelog Modules
3.7 The LloydTopor Syntactic Extensions
3.7.1 Monotonic LloydTopor Extensions
3.7.2 Nonmonotonic LloydTopor Extensions
4 The Semantics of Rulelog
4.1 A Model Theory for the Base Syntax
4.1.1 Semantic Structures
4.1.2 Models
4.1.3 Wellfounded Models
4.2 Semantics for Rulelog Syntactic Extensions
4.2.1 Path Expressions
4.2.2 UserDefined Functions
4.3 Argumentation Theories
4.3.1 Argumentation Theory with Multiway Exclusions (AME)
4.3.2 Cautious Argumentation Theory with Multway Exclusions (CAME)
4.3.3 Argumentation Theory with Binary Exclusions (ABE)
4.3.4 Cautious Argumentation Theory with Binary Exclusions (CABE)
4.4 Additional Background Axioms
4.5 Semantic Directives
5 Rulelog Builtins and Their Semantics
Index
1 Introduction
Rulelog is the logic underlying knowledge representation languages such as
FLORA2 and SILK. It
combines much of the latest work in logic programming,
nonmonotonic reasoning, business rules, and the Semantic Web. It is
designed to be appropriately expressive for supporting knowledge
representation in complex domains, such as sciences and law, and yet to be
efficiently implementable.
This document provides a formal account
of the syntax and semantics of Rulelog.
Rulelog includes a novel combination of features that hitherto have not
been present in a single system. Many of these features are drawn from
earlier systems, including FLORA2
[
KYWZ13], SweetRules
[
GDG^{+}], XSB [
SW11], and others, and
the design of Rulelog incorporates
extensive feedback collected from the users of these systems.
1.1 Acknowledgments
An earlier attempt to integrate some of the key features of these systems
was made as part of the Semantic Web Services Initiative
and resulted in the
Semantic
Web Services Language [
BBB^{+}05], which was never finalized or
implemented, however.
The authors thank Mike Dean for his very useful comments on the earlier
draft of this document.
Members of the HalAR team provided very helpful comments and critique.
This work was sponsored by Vulcan Inc. as part of the SILK project.
1.2 Typography
This document distinguishes several types
of sections that may be of varying interest to different audiences:
 Example: Contains a Rulelog fragment.
 Editor's Note: Identifies an outstanding editorial issue.
 Issue: Identifies an outstanding design issue.
 Important Change: Identifies an
important change with respect to the earlier specifications. May require
reimplementation.
 Rationale: Discussions on why certain design decisions were made.
2 Organization of the Document
The syntax of Rulelog is divided in three parts:
base language,
syntactic extensions, and
extralogical markup.
The base language includes those features of Rulelog to which we
provide
direct modeltheoretic semantics.
Like the base language,
syntactic extensions are used for knowledge representation in
Rulelog. However, they are
specified indirectly, via a translation into the base syntax, and no direct
model theory is given to these features.
In contrast to the base language and the extensions,
the extralogical markup is
not used for knowledge representation per
se. This markup includes various macros, like the CURIE macros, pragmas, compilation
directives, etc.
Presentation of the semantics of Rulelog is split in two parts. The
base semantics refers only to the base language of Rulelog; it
provides direct meaning to the constructs of the base Rulelog language.
The rest of the semantics
is specified
axiomatically, with the help of the
background axioms.
The base language includes Rulelog's most important features such as
as frames, path expressions, higherorder predicates and functions, and
defeasible rules. Defining the semantics of these highlevel knowledge
representation constructs via complex translations would have caused their
meaning to be obscured and, literally, lost in translation, making it
virtually impossible
to use these constructs correctly.
A good example of extralogical markup is the
compact URI
notation (or
CURIEs) [
BM08], which is
used throughout this document.
A CURIE has
the form
prefix:
localname. It is a macro that
evaluates into a concatenation of the value of the
prefix part and
the
localname part, and the resulting string is enclosed in single
quotes. A
prefix is an alphanumeric symbol
whose value is defined by a special Rulelog statement (also part of the
extralogical markup); this value is a
character sequence that is expected to have the form of an IRI. The
localname part is a character sequence that must be acceptable as
a path component in a URI. A CURIE macro is expected to expand into a
full IRI.
In this document we will use the following prefixes, which are defined in
Rulelog by default and do not require explicit definitions:
rlg: http://......./2013/Rulelog#
rdf: http://www.w3.org/1999/02/22rdfsyntaxns#
rdfs: http://www.w3.org/2000/01/rdfschema#
owl: http://www.w3.org/2002/07/owl#
xsd: http://www.w3.org/2001/XMLSchema#
rif: http://www.w3.org/2007/rif#
silk: http://vulcan.com/2008/silk#
Although these prefixes can be
redefined by the user, this is strongly discouraged.
3 The Syntax of Rulelog
This section describes the syntax of Rulelog.
First we introduce the alphabet of the language followed by the syntax of
the base language, the
base syntax.
Then we define syntactic extensions followed by the extralogical markup.
Throughout this section, we will be using a
convention in which the symbols written in the monospace font will
denote concrete elements of the language while
italicized symbols will denote nonspecific examples. Specific examples
will also use monospace. For instance, in
"string"^^xsd#string the symbol
string denotes
some arbitrary string but the double quotes,
^^, and
xsd#string are part of the language. Likewise, in
"ab12"^^xsd#string,
ab12 is a concrete sequence of the characters
a,
b,
1, and
2.
3.1 The Alphabet of Rulelog
The
alphabet of Rulelog consists of
disjoint
subsets of symbols described below. Some additional symbols, including
don'tcare variables "
?", Skolem constants, and local constants,
are not part of the logic and are therefore defined as part of syntactic
extensions in Section
3.4.
Editor's Note 3.1:
Functions and predicates with named arguments are not included in
the syntax at this point.
The set of constants,
Consts, can be broadly divided into two
disjoint categories:
uninterpreted symbols and
interpreted symbols.
The main kinds of uninterpreted symbols are
Rulelog abstract symbols
and
IRIs. These two types of symbols are disjoint.
The main kinds of interpreted symbols are data types.
Other kinds of interpreted and uninterpreted symbols may be introduced in
the future.
The syntax for Rulelog abstract symbols and IRIs is given below. In addition,
a Rulelog constant can have the form
"some string"^^symbol_space_name.
In this case it is called a constant with an
explicit symbol
space. Typically such constants belong to one of
the supported
datatypes (see below) but other,
nondatatype symbol spaces may be
introduced later.
 Uninterpreted symbols.
 Rulelog abstract symbols. A Rulelog abstract symbol is a sequence
of characters enclosed between a pair of single quotes. For instance,
'abc#$%'.
Single quotes that are part of a symbol are escaped with a backslash.
For example,
the symbol
a'bc"d
should be written as
'a\'bc\'\'d'.
A backslash is escaped with another backslash. Symbols that consist
exclusively of alphanumeric characters and the underscore
(_) and begin with a letter or an underscore do
not need to be quoted.
For example:
abc1 or
_abc. Compare this to
'12abc' and 'abc#de', which must be quoted.

IRIs or international resource
identifiers. An IRI is a sequence of characters enclosed between the
angle brackets. All printable ASCII characters are allowed except for
< and >.
For example:
<mailto:silkannounce@semwebcentral.org>,
<http: //w3.org/>.
The intent is that the enclosed sequence of characters forms a
syntactically valid IRI as specified in [
DG05]. However, Rulelog
allows malformed IRIs as well.
Since IRIs are typically very long, a CURIE macro notation is a typical
way of coping with this problem, as described in
Section 2.
Rulelog reserves IRI constants that have the following CURI prefixes:
silk, rlg, rdf, rdfs,
owl, xsd, rif.
For instance, rlg#defeated.
Issue 3.1:
Decide what kind of restrictions are to be imposed on the use of these
things. For instance, can such predicates be defined by the user?
 Interpreted symbols: datatypes.
Rulelog datatypes
are modeled after XML Schema datatypes [BM04].
A datatype constant is a constant with an explicit symbol space, i.e., it
has the form
"string representation"^^typename
where string representation is a sequence of characters and typename is
the name of the data type. The character
sequence string must belong to the lexical
space of the data type (see Section 3.2).
To include a doublequote """ inside string one must
escape it with a backslash. For instance,
"ab\"cd\"gf"^^\string.
The sets of constants that belong to different datatypes are disjoint
from each other. The following is a list of supported datatypes in Rulelog.
 Strings
have the form
"string"^^\string.
To simplify the use of strings, Rulelog provides a shortcut notation in
which a string of the form
"string"^^\string can be
written simply as "string".
For instance, äbcde" instead of
äbcde"^^\string.
 Integers have the form
"integer"^^\integer, where integer is an
integer value such as 123 or 25.
A shortcut for integers in Rulelog is simply to write them as above, i.e.,
123 and so on.
 Doubles have the form
"double"^^\double, where double is an
floating point number such as 123.45, 34.2e12, or
2e5. A shortcut for double numbers in Rulelog is simply to write
them as above, i.e., 123.45 or 34.2e12.
Editor's Note 3.2:
Add more datatypes.
Issue 3.2:
XSB and Flora do not parse 23e5. They require 23.0e5.
Do we want to allow this?
Issue 3.3:
Flora does not treat the full and the shortcut representation of strings
and numbers synonymously.
One solution is to change Flora to translate the long representation of
these types into their short representation.
Also, Flora does not implement decimals because XSB does not.
It maps them to doubles (which is contrary to the semantics of XML Schema).
3.2 Symbol Spaces and Datatypes
A
symbol space consists of
 A name that uniquely identifies that symbol space among all
symbol spaces.
 A lexical space  the set of all character
sequences that represent valid constants for that symbol space.
For a symbol space named α, its lexical space will be denoted
Consts_{α}.
A constant belongs to a symbol space,
sym, if and only if
it has the form
"charseq"^^sym and
charseq belongs to the
lexical space of
sym.
Example 3.1:
The following are Rulelog constants:
"12345"^^\integer
"123.345"^^\double
because the sequence of characters
12345 is a syntactically valid integer and
123.345 is a syntactically correct doubleprecision number. Thus,
each belongs to the lexical space of integers and doubles, respectively.
In contrast,
"123.45"^^\integer
is
not a Rulelog constant because
123.45 is not an integer.
A
datatype is a symbol space that, in addition, has
 A set called that datatype's value space.
For a datatype named α, its value space will be denoted
V_{α}.
 A mapping from the datatype's lexical space to its value space, called
lexicaltovaluespace mapping.
For the datatypes introduced in Section
3.1, these
notions are as follows:
 Strings. The symbol space name is \string.
Both the lexical and the value spaces Consts_{\string} and
V_{\string}
consist of the
set of all character sequences, and the lexicaltovaluespace mapping is
the identity mapping.
 Integers. The symbol space name is \integer.
The lexical space Consts_{\integer} consists of character strings that represent
syntactically valid positive or negative integers as well as 0.
The value space V_{\integer} is the set of all integer numbers and the
lexicaltovaluespace map maps any character string that represents an
integer into that integer.
 Doubles. The symbol space name is \double.
The lexical space Consts_{\double} is the set of all character strings that represent
doubles, as specified in the XML Datatypes document [BM04].
The value space V_{\double} is the set of all 64bit floating point numbers.
The lexicaltovaluespace map maps each string in the lexical space into
the floating point number it represents.
3.3 The Base Language
Rulelog has several types of
terms and
formulas. In this section we first define the notion of a term, then
of a basic formula, and then of a compound formula, of a rule, and of a
query.
3.3.1 Terms
A (pure)
HiLog term has one of these forms:
 A constant from the set Consts; or
 A variable in Vars; or
 An expression of the form t(t_{1},...,t_{n}), where n ≥ 0 and
t, t_{1}, ..., t_{n} are HiLog terms. When n=0, the term has the
form t().
In Section
3.4.1, we will introduce
generalized HiLog
terms, which incorporate
path expressions into the above syntax.
For example:
f(?X,abc), ?X(a,?Y),
?X(a)(?Y,b), b(?X,?Y),
abc, p(), p()q()r(),
b(?X,c)e(?Z)(u,22).
A
firstorder term has
an even more restricted form of a HiLog term: If is
either
 A constant from the set Consts; or
 A variable in Vars; or
 An expression of the form t(t_{1},...,t_{n}), where
t is a constant in Constsand
t_{1}, ..., t_{n} are firstorder terms. When n=0, the term has the
form t().
Note that this precludes variables over function symbols.
A
list term has one of these two forms:
 [t_{1},...,t_{n}]
 [t_{1},...,t_{n}  rest]
where t
_{1},...,t
_{n}, and
rest are terms.
For example:
[a,b,?X(?Z,s),c(p)], [a,?X,c?Y].
Editor's Note 3.3:
Not sure if it is worth giving a modeltheoretic semantics for lists.
If not, we'll move them to Syntactic Extensions.
A
reification term is an expression of the form
${φ}, where φ is a Rulelog formula
(see Section
3.3.2).
For example:
${p(a,b)}, ${a[p>b,q>c]},
${p(?X) :q(?X,?Y)}.
Editor's Note 3.4:
Need to see what kind of formulas can go under reification or instance,
quantifiers?
An
aggregation term is an expression that has one of the
following forms:
aggr{ ResultVar  Query }
aggr{ ResultVar [ GroupByVars ]  Query }
where
 aggr is the name of the aggregate operation, which can be
sum, avg, min, max, count,
or prod.
 ResultVar is a variable.
 Query is a query, as described in Section 3.3.4.
 GroupByVars is a commaseparated list of groupby variables.
For example:
avg{?Xo[p>?X], ?X[q>cde]},
count{?X[?Y,?Z] o[p>?X[?Y>cde],
q>?Z]}.
Editor's Note 3.5:
The prod operator is not implemented. Also rarely used.
Keep it?
An
comprehension term is an expression that has one of the
following forms:
cmpr{ ResultVar  Query }
cmpr{ ResultVar [ GroupByVars ]  Query }
cmpr{ ResultVar ( SortSpec )  Query }
cmpr{ ResultVar [ GroupByVars ]( SortSpec,...,SortSpec )  Query }
where
 cmpr is the name of the comprehension operation, which can be
setof or bagof.
 ResultVar is a variable.
 Query is a query, as described in Section 3.3.4.
 GroupByVars is a commaseparated list of groupby variables.
 SortSpec can be asc, desc, or a list of
the form [spec,...,spec], where each
spec has the form asc(N) or
desc(N).
Example 3.2:
The following are examples of comprehension in Rulelog:
setof{?X(desc) o[p>v[?Y>cde], q>?Z], ?X=f(?Y,?Z)}
setof{?X[?Y,?Z]([asc(2),desc(1)]) o[p>?X[?Y>cde], q>?Z]}
bagof{?X o[p>v[?Y>cde], q>?Z], ?X=f(?Y,?Z)}
bagof{?X[?Y,?Z] o[p>?X[?Y>cde], q>?Z]}
A
parenthesized term is an expression of the form
(
T), where
T is a term.
In Rulelog a parenthesized term
(T) is allowed wherever
T is allowed.
Parenthesizing is typically used for clarity or to override
associativity. For instance, we shall see that semantically a path
expressions of the form
a.b.c is the same as
(a.b).c. If
we want to change this default associativity, we could write, for example,
a.(b.c).
3.3.2 Basic Formulas
A Rulelog
basic formula plays a role similar to firstorder
atomic formulas. We call them
basic rather than atomic because these
formulas are not really atomic: they are equivalent to conjunctions of
atomic formulas.
Basic formulas will also sometimes be called
positive
literals.
In Rulelog
every formula is associated with a module explicitly or
implicitly.
Explicit association happens when a basic
formula occurs as a subformula of a
foreign formula (see
Section
3.3.3).
Implicit association
happens when a Rulelog rule set is loaded into the system. Every Rulelog rule set
is loaded into a specific module, M, and all basic
formulas that are not explicitly associated with a module become associated
implicitly with that module M. This is explained in
Section
3.6.
° Any Rulelog term is a formula, called
term formula.
(Jumping ahead, only reification terms are of any significance as
formulas. All other terms will uniformly be considered as false.)
° A
HiLog formula is a basic formula of the
form
H, where
H is a HiLog term. Although syntactically a HiLog formula may look
identical to a HiLog term, the former is associated with a module and,
as we shall see, it is interpreted differently by the Rulelog semantics.
° An
equality formula has the form T :=:S, where T and
S are HiLog terms.
° A
disequality formula has the form
T !=!S, where T, S are HiLog terms.
° A
unification formula has the form
T =S, where T, S are HiLog terms.
° A
disunification formula has the form
T !=S, where T, S are HiLog terms.
° A
comparison formula has the form T op S, where
op is
<,
>,
>=,
=<. Again, T and S are HiLog terms.
Editor's Note 3.6:
More comparisons? E.g., @<, @>, @=<, @>=
° An
evaluable expression is a formula of the form T
is Expr,
where T is a term and Expr is an expression.
For example:
?X is 2+min(3,?Z), 14 is 5*31,
a.b.c is ?X*?Y.
Issue 3.4:
The form of Expr needs to be sorted out. For now, this is an
arithmetic expression as in XSB and FLORA2, but we might want to add
string manipulation and others.
Issue 3.5:
Need to add sensor/builtin formulas. We don't want their names to be
returned by HiLog variables. So, we either put their names into a
separate domain (or do something similar).
° A
membership formula has the form P
:T where both P and
T are path expressions.
° A
subclass formula has the form P
::T where both P and
T are path expressions.
° A
frame formula is a statement of the form P[Spec
_{1}, ...,Spec
_{n}],
where n ≥ 0, P is a term, and each Spec
_{i} has one of these forms:
 Q_{i}, where Q_{i} is a term.
 Q_{i} > V_{i}, where Q_{i} is a term and V_{i} is a term or a frame
formula.
 Q_{i} > {W_{i,1},...,W_{i,k}}, where k ≥ 0 and each
W_{i,j} is a term or a frame formula.
Note that n=0 and k=0 are possible, so
foo[ ]
and
foo[bar>{}] are frame formulas.
In a frame formula, the Q
_{i}s are called
methods (or
properties, if they are just constants) and the V
_{i},
W
_{i,j} are called
values or
results. In the first case,
when
Spec
_{i} is Q
_{i}, the method has no explicitly specified value and is called a
Boolean method.
Example 3.3:
The following are frame formulas:
a[p(foo,bar)>v(?Z), q(?X,123)]
abc[pqr(1,2)]
abc[foo>{bar1,bar2,bar3}]
In the first, the method p(foo,bar)
has the name p, the arguments
foo and bar, and v(?Z) is its result.
The second method, q(?Z,123), is Boolean. It does not return any
results; it is simply true or false depending on its arguments (which are
?X and 123).
The second frame formula has only one method, and it is Boolean. The last
frame formula has the method foo that returns a set as its result.
Since foo is just a constant, this method is a property.
Spec Change 3.2:
Note: another restriction with respect to the old document: The Q_{i}'s
above cannot be frame formulas  only terms.
Signature formulas are used to say something about collections of
basic formulas. Such statements can be made about classes of objects (their
types and default property values) or about predicates.
° A
signature formula can have one the following forms:
C [ Spec_{1} , ... , Spec_{n} ]
P ( T_{1} , ... , T_{n} )
where n ≥ 0, C, P, T
_{1}, ..., T
_{n} are terms, and each Spec
_{i}
has the form
 M  typing for Boolean methods
 M=>V  typing for nonBoolean methods
 M {Low..High}=>V  same as above, but also specifies
min (Low) and max (High)
cardinality constraints on the result returned by the method
 M>V  specifies the default value for the method
Here M and V are path expressions and Low, High are nonnegative
or variables integers.
High can also be the symbol *, which denotes infinity.
Spec Change 3.3:
This is what we previously called
inheritable signatures (in case
of M=>V) and
inheritable defaults (in case of M>
V). Note the significant change in the syntax.
Also, we no longer have objectlevel signatures, i.e.,
foo[bar=>type]. The drawback is that some
inconvenience in specifying background axioms for typing and the
inability to specify types for a property directly in the framehave to
go up the class hierarchy. But the advantage is that we have one less
type of formulas. We can always add objectlevel signatures back later.
Spec Change 3.4:
Note: using low..high instead of low:high. This makes
":" less overloaded.
A signature of the form C[...] is a statement
about a class, C. In such a statement, an expression
of the form M=>V informally says that M is a property or a
method whose return value has the
type (i.e., belongs to the class) V.
An expression of the form M in signature formulas is used to give the
type for Boolean methods in frame formulas.
An expression of the form
M>V states that the
default value for M in class C is V.
For instance,
Human[ name{1..*}=>\string,
married(Year),
age(Year){1..2}=>\integer,
offspring{0..*}=>Human,
num_chromos=>\integer,
num_chromos>46 ]
states that the property
name for
humans has the type
\string,
the Boolean method
married tells us whether that person
was married in a particular year. Welltyped invocations of the method
married
must be provided instances of class
Year as an argument. The method
age is a method that tells us
person's age in a given year. Welltyped invocations of that method
take arguments that are instances of class
Year and returns an
integer. The cardinality constraint says that this method can return one or
two values: most people's age can change during the year except for those
born on January 1.
The property
offspring
returns values of type
Human; there are no cardinality restrictions
on that method (
0..* is redundant).
The property
num_chromos
has the type
\integer and its default value of 46.
A formula of the form P(...) is a statement about the argument types
of the predicate P where
the arguments are intended to represent classes of objects.
For instance,
Flight(City,City,\integer) states that
Flight is a
ternary predicate whose first two arguments have the type
City and
the last
\integer.
3.3.3 Compound Formulas
A
compound formula is a formula that combines basic formulas
into more complex ones. Rulelog has several different kinds of compound
formulas, as described below.
Some of them are allowed in the rule heads only and some both in
rule heads and bodies.
A
conjunctive formula (or a
conjunction,
for short) is a formula of the form
φ
and ψ, where both φ and ψ
are compound
formulas. As a
shortcut, Rulelog allows to use comma (",") instead of
and. Thus,
p(?X) and q(a,b) and
p(?X),q(a,b) are considered to
be synonymous.
A
defaultnegated literal is a compound formula of the form
nafφ,
where φ is a basic formula or an explicitlynegated formula.
An
explicitlynegated literal is a compound formula of the
form
negφ, where φ is a basic formula other than a
comparison formula or an evaluable expression.
A
parenthesized compound formula is an expression of the form
(φ) where φ is a compound formula.
In Rulelog,
a parenthesized formula,
(φ), is allowed wherever φ is allowed.
A
foreign formula is an expression of the form
φ@ModuleRef where φ is a basic or a parenthesized compound
formula, and
ModuleRef is a
module reference (to remind: a
module reference is an abstract symbol or a variable).
Foreign formulas can occur
only in rule bodies.
3.3.4 Rules, Facts, and Queries
A
rule is a statement of the form
@!{ruleid[tag>T, DefeasibilityFlag,OtherProperties]} head : body.
where
body is a compound formula,
T is a pure HiLog
term,
ruleid is a term, and
DefeasibilityFlag is either
strict or
defeasible.
OtherProperties is a commaseparated, possibly empty list of items
of the form
term or
term>
term. The tag
property above can appear in any order with respect to the other items
inside the brackets or it may be omitted.
The head of a rule,
head, is a basic formula
other than:
 a comparison formula
 an evaluable expression
The expression
head in the above rule is called the
head of the
rule and
body is called the
body of that rule.
The
@!{...} part is called the
descriptor
of the rule. Its primary role is to provide a handle by which the rule
could be used as part of the defeasible reasoning machinery. Other uses of descriptors include
identification and syntax extensions.
Rulelog defines a number of components of statement descriptors, which are
listed in Section
3.4.
The descriptor part is optional but, if omitted, a unique rule Id
descriptor is assumed to be assigned b the systemSee
Section
3.4.
Note that rules are terminated with a period. Facts and queries, defined
below, are also terminated with periods.
A
fact is a statement of the form
fact.
where
fact is a term.
A
query is a statement of the form
? query.
where
query is a compound formula.
Spec Change 3.5:
Note: exclusions will no longer be specified using the exclusion
annotation. Instead, we'll be using a predicate or a frame.
Issue 3.6:
Need to come up with a predicate/frame/whatever to express exclusions in
an argumentationtheoryindependent way.
Editor's Note 3.7:
Note: overriding and exclusions are not part of this syntax section. That is
because they are not new kinds of syntactic formulas. They are regular
predicates syntaxwise, but their semantics is special.
So, they'll be addressed in the semantics section.
3.4 Syntactic Extensions
3.4.1 Path Expressions
A
path expression is a term of the form
e
_{1}.e
_{2}. … .e
_{n}, where n ≥ 1 and
 Each e_{i}, is either a generalized HiLog term (see below), a frame
formula (defined in Section 3.3.2), or a parenthesized
path expression;
and
 e_{n} is a generalized HiLog term.
For example,
the following are path expressions:
a.b.c, a.b[p>c,q>d].e,
a.b[p.r>c,q>d.h].e[abc.cde].f,
?X(a,?Y), abcde,
?X(a)(?Y,b), a.b(?X,?Y.f(s)).
In contrast, a.b.c[d>e] and a.b[p>c,q>d]
are not path expressions.
Spec Change 3.6:
The last condition in the definition of path expressions
makes Rulelog path expressions a little more
restricted than before (see the above negative examples). This is to avoid unintuitive semantics of formulas
such as p(a.b[c>d]), which people often confused with
p(${a.b[c>d]}).
Also, no path expressions of the form p!q!r. Our experience has
been
that we never used them (also in FLORA2), and we are changing the syntax of
signatures anyway.
A
foreign path expression is a term of the form
T@ModuleRef,
where
T is a path expression and
ModuleRef is a
module reference, which can be an uninterpreted Rulelog symbol (a
module name) or a variable.
Editor's Note 3.8:
Terms as module names are also useful. However,
this is not implemented at present. Terms as module names
are also hard to implement efficiently.
A
generalized HiLog term has one of the following forms:
 A (pure) HiLog term.
 A reification term.
 A path expression.
 An expression of the form t(t_{1},...,t_{n}), where n ≥ 0 and
t, t_{1}, ..., t_{n} are path expressions. When n=0, the term has the
form t().
For example:
f(?X,abc), ?X(a,?Y),
?X(a)(?Y,b), a.b(?X,?Y),
a.b(?X,c).d(e(?Z).f,q.p[r>13].u,22).
Editor's Note 3.9:
Note: a.b(c.d,e.f) is a generalized HiLog term.
Check if FLORA2 parses this correctly.
Note: need to specify associativity correctly. Flora parses the above as
(a.b)((c.d),(e.f)), as expected.
Generalized HiLog terms are permitted anywhere where
pure HiLog terms are allowed in the Rulelog syntax, except:
 Statement descriptors.
 Places where specialized terms
are explicitly required (e.g., variables, firstorder terms).
Example: aggregate variables are explicitly
required in comprehension terms, so generalized HiLog terms are not allowed
there.
 Wherever otherwise stated explicitly.
3.4.2 UserDefined Functions
Userdefined functions (abbr., UDF) are a syntactic extension that permits the
users to enjoy certain aspects of functional programming in the framework
of a logicbased language.
A
declaration of a userdefined function has one of the following
forms:
udf FunctionName(t1,...,tn) := Expr if Definition.
udf FunctionName(t1,...,tn) := Expr : Definition.
udf FunctionName(t1,...,tn) := Expr.
The first two forms are equivalent; the last is an abbreviation for the
case where Definition is empty (i.e., tautologically true).
Expr is a term and
Definition can be any formula that can
be used as a rule body. The arguments of the UDF
foo are terms,
which usually are distinct variables, but generally the arguments can be
any terms.
Expr and
Definition can contain occurrences of
other UDFs, but those UDFs must be defined previously.
Example 3.4:
The following example defines
father/1 as a function.
udf father(?x):=?y if father(?x,?y).
father(mary,tom).
father(john,sam).
Now, instead of writing
father(John,?y) and then using
?y
one can simply write
father(?John):
? ?y=father(?x).
will return
?x=mary ?y=tom
?x=john ?y=sam
The query
? writeLn(father(mary))@\pplg.
will output
tom.
Although the UDFs used in the definition of another UDF must be previously
defined, it is still possible to create mutually recursive UDFs with a
little syntactic workaround.
Example 3.5:
The following function declaration is not allowed:
udf foo(a) := b.
udf foo(?X) := f(?X) if p(bar(?X)), ?X>0.
udf bar(?X) := foo(?Y) if ?X is ?Y+2.
because the definition of
foo uses the UDF
bar, which is defined only later. However, the following
legal workaround captures the original intent:
udf foo(a) := b.
udf foo(?X) := f(?X) if newpred(?X).
udf bar(?X) := foo(?Y) if ?X is ?Y+2.
newpred(?X) : p(bar(?X)), ?X>0.
The following examples illustrate a number of advanced uses of the UDF
feature. One of the most interesting such features is a simplification of
the use of arithmetics. For instance, normally one would write
? ?x is 1+2, writeLn(?x)@\prolog.
but with UDFs we can define "+" as a function:
udf ?x+?y := ?z if ?z is ?x+?y.
and then issue the following query:
? writeLn(1+2)@\prolog.
to get the same result.
The following example uses the above arithmetic functions
in an elegant definition of the Fibonacci function:
Example 3.6:
Functional definition of Fibbonacci:
udf ?x+?y := ?z if ?z is ?x+?y.
udf ?x?y := ?z if ?z is ?x?y.
udf fib(0) := 0.
udf fib(1) := 1.
udf fib(?x) := fib(?x1)+fib(?x2) if ?x>1.
We can now write queries like the following:
? writeLn(fib(34))@\prolog.
instead of the more cumbersome
? fib(34,?X), writeLn(?X)@\prolog.
This also illustrates how a definition of a UDF can
consist of multiple
functionstatementsjust like a definition
of a predicate can have multiple rules.
3.4.3 Statement descriptors
Editor's Note 3.10:
This section might be moved to nonlogical markup.
Statement descriptors are used to modify the
syntax and semantics of the Rulelog expressions in which they
appear and to attach metadata to those expressions.
Spec Change 3.7:
Note: @[prefix] and @[argumentation] are
gone.
These are statements that belong to nonlogical markup and to semantic
directives. They have global effect and are absolutely out of place among
descriptors.
The general form of a descriptor is
@!{ruleid[descriptor1, ...,
descriptorn]}
where each
descriptori has one of these forms:
keyword
keyword>value.
where
keyword and
value are terms.
The keywords
tag,
strict, and
defeasible are
reserved and are described in more details below.
The explicit rule id may be replaced with
"
\@!". The descriptor may be omitted altogether. In these two
cases, a unique abstract symbol is implicitly assigned as the id of the
rule. The frame part of the descriptor, [...], can also be omitted
(leaving only the rule Id).
At most one rule Id descriptor can precede the same Rulelog
rule. However, as we shall see shortly, several shortcuts are allowed, and
any number of these shortcuts can be specified in addition to or instead of
the rule Id descriptor.
These multiple rule descriptors must
not conflict, however. For
example, the same rule cannot be specified both as strict and
defeasible.
Note also that, since
value above must be a term, frames cannot be
nested inside rule descriptors.
The aforesaid descriptor shortcuts are defined below.
Example 3.7:
Explicit and implicit rule Ids:
Explicit rule id:
@!{123[tag>{foo,bar},defeasible]} or, equivalently,
@!{123} @foo @bar @@defeasible using the shortcut
notation defined below. Note the use of multiple annotation blocks in the
shortcut form (and also multiple tags).
Implicit rule id:
@!{\@![tag>foo,defeasible]} or, equivalently,
@foo @@defeasible using the shortcut
notation.
Users can introduce their own descriptors properties:
Example 3.8:
@!{r123[my#tag>abc,
dc#creator>'http://ex.com/Bob',
another_property>1]}
p(?X) : q(?X).
The explicit ids of rules in the same file or document must be distinct.
However, different documents and files can, in principle, have rules with
the same id. Given the potentially decentralized nature of knowledge base
development, it is impractical to assume that ids in different documents
will not clash.
The
full rule ids are thus defined as triples of the form
(explicit_ruleid, file/document_url, Rulelog_module) 

This schema makes it possible to uniquely identify rules both at run time
and statically, in a Rulelog document. Static uniqueness
is ensured by the fact that ids are unique within each file, and
the inclusion of file/document URLs provides the rest.
Runtime uniqueness is achieved by including the modules into which the rules
are loaded. (Recall that the same Rulelog file/document can be loaded into
several different modules. For instance, several agents can be initialized
with the same knowledge base.)
An important side effect of specifying descriptors (whether builtin
or userdefined) is that certain facts are automatically generated and
added to the knowledge base. These facts are accessible to the user
knowledge base. The form of these facts are up to each particular
implementation of Rulelog, but they must be queriable through the
standard Rulelog primitive
@!{...}, described later.
The following keywords are reserved:
 tag:
 Specifies a rule tag or tags to be
used by the defeasible reasoning
mechanism (see Section 4.1).
The tags do not have to be unique and multiple rules may have the same tag.
If no tag is given, the value of the id descriptor is assumed.
Shortcut: @sometag or @{sometag}
instead of
@!{\@![tag>sometag]}.
For instance, @foobar instead of
@!{\@![tag>foobar]} and @tag1
@tag2 instead of
@!{\@![tag>{tag1,tag2}]}.
 strict:
 Indicates that the rule is to be strict, i.e.,
nondefeasible. Rulelog allows strict rules to have tags, as some
implementations might opt to make strictness a runtime property, which
could be turned on and off.
Shortcut: @@strict or @@{strict}.
 defeasible:
 Indicates that a rule is to be
defeasible. This is a default.
strict and defeasible are mutually
exclusive and cannot be both specified.
Shortcut: @@defeasible or @@{defeasible}.
Note that shortcut and the unabbreviated form of the rule descriptor can be
combined in various ways, as shown below.
Example 3.9:
Various alternatives:
@!{myid[abcd>123,tag>{tag1,tag2},strict]} rule.
@tag1 @!{myid[abcd>123, tag>tag2, strict]} rule.
@tag1 @tag2 @!{myid[abcd>123, strict]} rule.
@tag1 @tag2 @@strict @!{myid[abcd>123]} rule.
Querying statement descriptors.
Statement descriptors can be queried using the
@!{frame}
construct in rule bodies or queries. Here
frame is a
frame formula of the form
Obj[prop1,prop2,...].
It has the same syntax as the frame in the rule Id descriptor and has the
same restrictions. In particular, these frames cannot be nested.
For instance,
Example 3.10:
A descriptor query:
? ..., @!{?X[strict,tag>B,foo>1,bar>?Y]}, ...
3.4.4 Skolem Constants and Function Symbols
Skolemization is a logical process which introduces a completely new
constant of function symbol as a replacement for existential quantifiers.
Silk supports skolemization by providing syntax that the user can use to
specify a skolem constant or function and the compiler will automatically
take care of the uniqueness. Two type of Skolem symbols are supported:
named and unnamed.
 Unnamed Skolem symbol:
 \#.
Every occurrence of this symbol is replaced by the compiler with a
completely new abstract symbol. This symbol can occur both as a constant
and as a function symbol.
For example,
\#, \#(a,b), \#(a,\#(b,\#))
 Named Skolem symbol:

\#12, \#59.
These symbols are written as an unnamed Skolem followed by a number.
Each numbered Skolem symbol has the scope of the Rulelog rule/fact in which it
occurs. Identically named such symbols that occur in the same rule/fact are
replaced by the compiler with the same new symbol, while
symbols that occur in different rules are treated as unrelated.
Example 3.11:
Consider the following two rules:
\#12(?X,\#12(?X,b), \#34(a,\#34(b,\#,\#))) : ...
\#12(?X) : \#12(?X,d), \#34(a,\#34)) : ...
In the first rule, the two occurrences of
\#12 are replaced
with the same new abstract symbol. The two occurrences of
\#34 are also replaced with a new abstract symbol, but with
one that differs from the symbol used for
\#12. The two
occurrences of the symbol
\# are replaced
with two different new symbols that are unrelated to each other and to
the symbols used for
\#12 and
\#34.
The two occurrences of the symbol
\#12 in the second rule
are also replaced with the same new symbol, but this symbol is
different from the one used for
\#12 in the first rule. Ditto
for
\#34 in the second rule.
Observe that in this example all Skolem symbols occur only in the rule heads.
This is not accidental': such symbols are allowed only in rule heads.
Using them in rule bodies is considered an error because, due to the
uniqueness of these symbols, a bodyoccurrence of such a symbol cannot be
satisfied by matching against of another Rulelog fact or rule.
3.4.5 Various Other
TBD
 Omni.
 Composite frame formulas (combinations of frames and
subclass/membership)
 introduce notation like {obj1,obj2,obj3}:class likewise for
{cl1,cl2,cl3}::cl.
 introduce class expressions like (class1 and class2), (class1
or class2). This will allow writing obj:(class1 andclass2)
(equivalently obj:(class1,class2)),
i.e., it belongs to both.
3.5 Nonlogical Markup
Nonlogical markup consists of Rulelog statements that do not affect the
semantics. The purpose of these
statements is to make the use of Rulelog more convenient. Statements that
belong to
nonlogical markup include macros, comments, import statements, and the
like.
3.5.1 IRI Prefix and Base Declarations
A
prefix declaration is a statement of the
form
: prefix prefixname = <URI>.
Such a statement defines
prefix names that can be later used in
CURIE macros. For instance,
: prefix w3 = <http://www.w3.org/TR/>.
defines a prefix,
w3. As a result of this declaration,
a macro such as
w3#xquery expands into the IRI
'http://www.w3.org/TR/xquery'. Note that the
concatenated string is enclosed in single quotes. If the expansion of the
prefix contains single quotes then those quotes must be escaped
with a backslash.
A
base declaration declares a prefix to be used with CURIE
macros that have no explicitly given prefix. It has the form:
: base <URI>.
At most one base directive per file or document is allowed.
Issue 3.7:
Or should we allow later base declarations to replace earlier ones?
What about multiple declarations of the same prefix?
A CURIE macro that has no explicit prefix looks like this:
#localname,
where
localname is the local name of a CURIE.
For instance, if a Rulelog document has this declaration:
: prefix <http://www.w3.org/TR/>.
then
#xquery will expand into
'http://www.w3.org/TR/xquery'.
3.5.2 Comments
Rulelog has two kinds of comments:
single line comments and multiline comments. The syntax is the same as
in Java. A
singleline comment is any text
that starts with a
// and continues to the end of
the current line. If
// appears within a string
(
"...") or a quoted symbol
(
'...') then these characters are
considered to be part of the string or the symbol, and in this case
they do not start a comment. A
multiline
comment begins with
/* and ends with a matching
*/. The combination
/* does
not start a comment if it appears inside a string or a quoted symbol.
3.5.3 Import and Export of Modules
An
import statement has the form
: import module_{1}, ..., module_{n}.
where module
_{i} are Rulelog module names.
Informally, this means that external formulas that match the modules'
exported templates can be
invoked (i.e., appear in rule bodies) in
the module where the import statement appears.
A
formula template is a pure HiLog, frame, membership, or subclass formula
of the following form:
 HiLog: t(?,...,?) (zero or more arguments), where
t is either the anonymous variable ? or a term.
 Frame: ?[m>?], where m is ? or a term.
 Membership: ? :c, where c is ? or a term.
 Subclass: ? ::c, where c is ? or a term.
An export
statement has the form
: export Template_{1} [>> (module_{11}, ..., module_{1k1})],
...,
Template_{n} [>> (module_{n1}, ..., module_{nkn})].
where Template
_{i} are formula templates and moduleij are module names
and
parentheses around the module lists are needed only if more than one module
is listed.
The parts inside the brackets are optional. If the
>>clause is
not present, the corresponding template is exported to all modules.
If the
>>clause is present, the template is exported only to
the listed modules.
If a module has no export statement, all HiLog, frame, membership, and
subclass formulas are exported. If a module
has an export statement
then only the listed templates are exported.
A runtime attempt by a rule in module M
to call an atomic formula that does not unify with a
template exported to M
will result in an error and the current query will be terminated.
Example 3.12:
Here are some examples of the import and export statements in Rulelog:
:
import foobar.
:
export ?(?)>>(me,you), p(?,?), ?[name>?], ?::person>>him.
The first statement makes all exported formulas in module
foobar
available in the module where the above
import statement occurs.
The second statement exports various formulas from the current module as
follows:
 export ?(?)>>(me,you): any unary HiLog predicate to
modules me and you (and none other).
 p(?,?): binary predicate p to any module.
 ?[name>?]: the method name (in any
class) to any module.
 ?::person>>him: the ability to query which
classes are subclasses of person to module him.
3.5.4 Preprocessor
Rulelog has a Clike preprocessor, which can be used to make
Rulelog knowledge bases more readable and flexible.
TBD
Here we intend to include something like
the C language macros, i.e., #define, #include.
For this we might be able to reuse gpp, the preprocessor used by XSB and
Flora.
3.6 Creation of and Loading into Rulelog Modules
Rulelog modules can be created
 by loading a file or a document into a module.
 by a newmodule command.
On startup, the module
main is automatically created and all
rules and facts inserted directly through the Rulelog shell
are automatically in that module.
These rules can be overwritten with an explicit
load command or
added to using an
add command:
? load{FileOrURL)}.
? add{FileOrURL)}.
The
load command deletes all the rules and facts that exist in
module
main and instead inserts the rules and facts from the file
or document specified by
FileOrURL into that module. The
add command works similarly, but does not erase the old contents
of
main.
The above commands can also be used to create (or refresh) other modules as
follows:
? load{FileOrURL>>ModuleName)}.
? add{FileOrURL>>ModuleName)}.
The first command works as follows. In the module
ModuleName does
not exist, it is created empty and then the rules and facts found in
FileOrURL are inserted in the new module. If the module does
exist then the old contents is erased and the new contents is taken to be
that of
FileOrURL. The
add command works similarly except
that the old contents is not erased:
ModuleName is created empty, if
necessary, and then the contents of
FileOrURL is added to what is
currently in the module.
Modules can be deleted with the help of the
erasemodule command:
? erasemodule{Module_{1},...,Module_{n}}.
An empty module can be also created using the
newmodule command:
? newmodule{Module_{1},...,Module_{n}}.
Rulelog also supports shortcuts for loading and addition to modules: instead
of
load one can type
[...] and instead of
add(...) one can use
[+...]. These commands are
illustrated below.
Example 3.13:
Loading, addition, deletion, and creation of modules.
? load{foo}, add{'http://example.com/test'}.
? add{bar>>moo}, load{'http://example.com/test'>>testmod}.
? [foo]. // same as load
? [+bar>>moo], [+bar2>>moo]. // same as add to moo
? ['http://example.com/test'>>test]. // same as load into test
? erasemodule{moo,test}.
? newmodule{moo,testmod}.
it should be kept in mind that the code that is loaded into a module is
compiled into very efficient virtual machine code and therefore is
much faster than the code that is added to a module.
This difference in performance is especially pronounced for rules (even
small ones), but does not exist for facts.
Therefore, users should structure their knowledge bases by first loading
most of the rules into the relevant modules and keep subsequent rule addition
in check. Adding facts does not cause significant overhead, however.
3.7 The LloydTopor Syntactic Extensions
The LloydTopor syntactic extensions [
Llo87] make it
possible to include firstorderlooking formulas in the rule bodies subject
to certain restrictions. They also slightly generalize the
heads of the rules. We distinguish between the relatively simple
monotonic LloydTopor extensions and the more complex
nonmonotonic ones.
3.7.1 Monotonic LloydTopor Extensions
These extensions introduce the following features:
 Disjunction in rule bodies.
 Conjunction in rule heads.
 Additional forms of implication.
A
LloydTopor implication is a statement of
one of the following forms:
formula_{1} ~~> formula_{2}
formula_{2} <~~ formula_{1}
where the
formula
_{2}
is a conjunction of basic formulas
and formula
_{1} can be a Boolean combination of basic
formulas that contains conjunctions and disjunctions only.
Intuitively, the implication
f_{1} ~~>
f_{2} is interpreted as
"
naff_{1} or f_{2}" while
f_{2} <~~ f_{1} is treated as
"
f_{2} or naff_{1}".
If LloydTopor implication holds in both directions between formulas,
their logical equivalence can be expressed in a single statement using
LloydTopor biimplication of the following
form:
formula_{1} <~~> formula_{2}
In that case, both
formula_{1} and
formula_{2} must be
conjunctions of basic formulas.
Horn rules are extended as follows. A rule
still has the form
head : body.
but
head can now be a conjunction of basic formulas
^{1}
and of LloydTopor implications (including biimplications) and
body can have basic formulas combined
using the
and and
or connectives.
Editor's Note 3.11:
Add the implications of the form
==>, <==, <==>.
Monotonic LloydTopor extensions are viewed as shortcuts that reduce
to the base Rulelog via the following
monotonic LloydTopor transformations:
 head : body_{1} or body_{2}
reduces to
head : body_{1}.
head : body_{2}.

head_{1} and head_{2} : body
reduces to
head_{1} : body.
head_{2} : body.

(head_{1} <~~ head_{2})
: body
reduces to
head_{1} : head_{2} and body.

(head_{1} ~~> head_{2})
: body
reduces to
head_{2} : head_{1} and body.

(head_{1} <~~> head_{2})
: body
reduces to
head_{2} : head_{1} and body.
head_{1} : head_{2} and body.
Complex formulas in the head are broken down using the last four
reductions. Rule bodies that contain both disjunctions and conjunctions
are first converted into the disjunctive normal form and then are broken
down using the first reduction.
3.7.2 Nonmonotonic LloydTopor Extensions
Nonmonotonic LloydTopor extensions include explicit bounded
quantifiers (both
exist and
forall) and also permit LloydTopor implications
<~~, ~~>, and <~~>
in rule bodies.
^{2}
These extensions essentially permit arbitrary firstorderlooking formulas
in the
body of Rulelog, although, as we shall see, with certain restrictions.
We emphasize that
the semantics of Rulelog is
not firstorder and this is why we
call these formulas "firstorder looking" and not firstorder.
For example, LloydTopor
implication
A <~~ B is interpreted in a
nonclassical way: as
(A ornaf B) (either
A is known or
B is not known to be true). This is quite different from
classical implication, which is interpreted as
(A orneg B) (either
A is known or
B is known to
be false).
Recall that without explicit quantification, all variables in a rule are
considered
implicitly quantified with
forall outside of the rule, i.e.,
forall
?X,?Y,... (head : body).
A variable that occurs in the body of a rule but not in its head can be
equivalently considered as being existentially quantified in
the body. For instance,
forall(?X,?Y)^( p(?X) : q(?X,?Y) ).
is equivalent to
forall(?X)^( p(?X) : exist(?Y)^(q(?X,?Y)) ).
In the scope of the
naf operator, unbound
variables have a different interpretation under negation as failure.
For instance, if
?X is ground and
?Y is not ground as, for instance, in
p(?X) : naf q(?X,?Y), r(?Y).
then the evaluation of
naf q(?X,?Y) is delayed until
?Y
is bound by other subgoals (such as
r(?Y)). If
?Y cannot
be ground (e.g., if
r(?Y) does not ground
?Y) then a
runtime error is issued. The user can also explicitly request that instead
of an error the variable
?Y should be treated as existential, if
it is not grounded by subsequent subgoals:
forall(?X)^( p(?X) : wish(ground(?Y))^(naf q(?X,?Y)) ).
Here
wish(...) is a
delay quantifier, which will be
explained elsewhere.
Formally, Nonmonotonic LloydTopor extensions include the following kinds
of rules. The rule
heads are the same as
in the monotonic LloydTopor extension. The rule
bodies are defined as follows.
 Any basic formula is a legal rule body
 If f and g are legal rule
bodies then so are
 f and g
 f or g
 naf f
 f ~~> g
 f <~~ g
 f <~~> g
 If f is a legal rule body then so is
 exist(?X_{1},...,?X_{n})^f
where ?X_{1}, ..., ?X_{n}
are variables that occur positively (defined below) in
f.
 If g_{1}, g_{2} are legal rule bodies then
 forall(?X_{1},...,?X_{n})^(g_{1}~~> g_{2})
 forall(?X_{1},...,?X_{n})^(g_{2}<~~ g_{1})
are legal rule bodies provided that
?X_{1}, ..., ?X_{n} occur
positively in g_{1}
The above quantifiers bind stronger than the other connectives such as
and,
or, ~~>, etc., so parentheses should
be used when ambiguity might arise. For instance,
forall(?X)^p(?X),q(?X) is interpreted as
forall(?X)^(p(?X)),q(?X) rather than
forall(?X)^(p(?X),q(?X)).
A
positive occurrence of a variable in a
formula is defined as follows:
 All variables in a basic formula occur there positively
 A free variable occurs positively in f and g
iff it occurs positively in either f or g.
 A free variable occurs positively in f or g
iff it occurs positively in both f and g.
 A free variable occurs positively in f ~~> g
iff it occurs positively in g.
 A free variable occurs positively in f <~~ g
iff it occurs positively in f.
 A free variable occurs positively in f <~~> g
iff it occurs positively in both f and g.
 A free variable occurs positively in
exist(?X_{1},...,?X_{n})^f
or forall(?X_{1},...,?X_{n})^f
iff it occurs positively in f.
Editor's Note 3.12:
Need rationale here.
Issue 3.8:
Need to add restrictions to the above syntax. For instance, universal
quantifiers over builtins should be disallowed
because one cannot generally compute things like
naf exists somebuiltin or forall(...)^somebuiltin.
Similarly, universal quantification
of subgoals that are in the scope of the delay
quantifiers wish and must cannot be allowed for the same
reason.
Nonmonotonic LloydTopor Transformations
These transformations aim
to eliminate the extended LloydTopor syntactic
forms in rule bodies
and reduce these rules to the base Rulelog syntax.
The intuition behind most of these transformations is that
(f ~~> g) is treated as a
shorthand for
(naf f) org
and
forall(?X)^f as a shorthand for
naf exist(?X)^(naf f).
Note that the rules, below, must be applied topdown, that
is, to the conjuncts that appear directly in the rule body. For
instance, if the rule body is as follows
forall(?X)^exist(?Y)^(foo(?Y,?Y)~~> bar(?X,?Z)) <~~ foobar(?Z)
then one should first apply the rule for <~~,
then the rules for
forall,
and finally the rules for
exist and ~~>.
The nonmonotonic LloydTopor transformations are listed next.
 Let the rule have the form
head :
body_{1} and(f ~~> g)
and
body_{2}.
Then the LloydTopor transformation replaces it with the following pair of rules:
head : body_{1} andnaf
f andbody_{2}.
head : body_{1} andg
and body_{2}.
The transformations for <~~ and <~~> are similar.
 Let the rule be
head :
body_{1} and
forall(?X_{1},...,?X_{n})^(g_{1}
~~>
g_{2})
and
body_{2}.
where ?X_{1},...,?X_{n}
are free variables that occur positively in
g_{1}.
The LloydTopor transformation replaces this rule with the following pair
of rules, where q(?X′_{1},...,?X′_{n}) is a new nary
predicate and ?X′_{1},...,?X′_{n} are new variables:
head : body_{1} andnaf
q(?X′_{1},...,?X′_{n}) andbody_{2}.
q(?X_{1},...,?X_{n}) :
g_{1} andnaf g_{2}.
The transformation for <~~ is similar. Biimplications, such as
g_{1} <~~>g_{2}, are first broken into conjunctions of unidirectional
implications, e.g., g_{1} <~~g_{2}
and g_{1} <~~>g_{2}, and the the transformation rules for the
latter are applied.
 Let the rule be
head : body_{1} and
exist(?X_{1},...,?X_{n})^(f)
andbody_{2}.
where ?X_{1},...,?X_{n}
are free variables that occur positively in f.
The LloydTopor transformation replaces this rule with the following:
head :
body_{1} andf′ and
body_{2}.
where
f′ is f in which the variables
?X_{1},...,?X_{n} are
consistently renamed into new variables. Since the variables in
f′ are new and do not appear elsewhere in the rule,
the explicit existential
quantification can be dropped in favor of implicit
quantification.
4 The Semantics of Rulelog
Like the syntax of Rulelog, the description of
its semantics is organized into several parts. The
first part consists of a
formal model theory for the base sublanguage of Rulelog
(i.e., the sublanguage formed by Rulelog's base syntax); it is presented in
Section
4.1. The second part presents a
semantics for the syntactic extensions of Rulelog's language. This does not require a separate
model theory. Instead,
syntactic extensions are
translated directly into the base syntax, as described in
Section
4.2.
The third part consists of
background axioms that are
not covered by the model theory. These axioms are given in
Section
4.4. In addition, the semantics of Rulelog can be
controlled
by various userlevel directives, such as the directives that prescribe the
argumentation theory to be used. These directives are described in
Section
4.5.
4.1 A Model Theory for the Base Syntax
We now turn to a rigorous modeltheoretic description of the semantics of
the base sublanguage of Rulelog. First we define semantic structures and then
the notion of entailment.
4.1.1 Semantic Structures
The
extended Herbrand universe U_{H}
consists of all
ground (i.e., variablefree) Rulelog terms
of the following kinds:
 ground pure HiLog terms (Section 3.3.1).
This subset of U_{H} will be denoted by U^{pure}_{H}.
 ground reification terms.
This subset of U_{H} will be denoted by U^{reif}_{H}.
Since here we will be dealing only with extended Herbrand universes, we
will usually omit the adjective "extended."
Rulelog's semantics is based on a variant of the wellfounded semantics for
logic programs [
VRS91], which is a form of
threevalued logic that relies on partial interpretations. In describing
the model theory of Rulelog we follow the outline of [
Prz94].
A Rulelog
semantic structure,
I, is a tuple of the form 〈
D_{I},
I_{C},
I_{V},
I_{true}〉,
where
4.1.2 Models
If φ is a ground formula,
M a semantic structure, and
M_{true}(φ) =
t, then we write
M=φ
and say that
M is a
model of φ or that φ is
satisfied in (or by)
M.
An interpretation
M is a model of
a Rulelog rule set
P if and only if all the rules in
P are satisfied
in
M, i.e., if
M=R for every R ∈
P.
If
Ais an argumentation theory (such as the ones in
Section
4.3) then
M is a
model of
P
with respect to the argumentation theory A if and only if
M is a
model of
P and of
A. In this case we write
M=(
P,
A).
We now define a
truthorder on Herbrand semantic structures. Let
M^{1}
and
M^{2} be two such structures. We write
M^{1}≤
_{t}M^{2} if the
following conditions hold for every ground term t in
U_{H}:
 M_{true}^{1}(t) = t implies M_{true}^{2}(t) = t
 M_{true}^{2}(t) = f implies M_{true}^{1}(t) = f
A model of (
P,
A) that is minimal with respect to ≤
_{t} is called
a
least model.
In general, there can be several least models for
Pwith respect to an
argumentation theory.
It is known that rule sets that do not have defaultnegated literals
(i.e., those negated with
naf) have a
unique
least partial model [
Prz94].
If
P is such a knowledge base, then its unique least model is denoted
by LPM(
P).
4.1.3 Wellfounded Models
We now define
wellfounded models for Rulelog knowledge bases. There
are several equivalent ways to define wellfounded models. Here we adopt
the definition from [
WGK^{+}09], which follows the general outline of
[
Prz94]. First, we define the notion of a
quotient.
Let
Pbe a set of rules, which can include defeasible as well as strict
rules, and let
I be a Rulelog semantic structure for
P. We
define the
Rulelog quotient of Pby I, written as
[(
P)/(
I)], via the following sequence of steps:
 Replace every defaultnegated literal (i.e., negated with naf)
that occurs in a rule
body in P
by its truth value in I.
 For every defeasible rule in P of the form
@[tag>R,defeasible] Head : Body.
in some module M:
If
I_{true}(\prolog(R,Head,M)) = t,
replace the defeasible rule with the following strict rule:
@[strict] Head :Body, f.
 For every defeasible rule in P of the form
@[tag>R,defeasible] Head : Body.
in some module M:
If
I_{true}(\prolog(R,Head,M)) = u,
replace the defeasible rule with the following strict rule:
@[strict] Head :Body, u.
 Remove all tags from the remaining rules.
The resulting set of rules constitute the
Rulelog quotient
[(
P)/(
I)].
Note that Rulelog quotients do not have
nafnegated literals so, as mentioned
earlier, every quotient has a unique least model. In other
words, LPM([(
P)/(
I)]) always exists and is unique.
A Rulelog semantic structure
I is
empty if
I_{true} maps every term
in
U_{H} to
u, i.e., all ground atomic formulas are
undefined.
We are now ready for the main definition:
The
wellfounded model of a Rulelog knowledge base
P
with respect to an argumentation
theory,
A, denoted WFM(
P,
A),
is the limit of the following transfinite, inductively defined,
sequence.
Initially,
I_{0} is the empty Rulelog semantic structure. Suppose
I_{m}
has already been defined for every m < k, where k is an
ordinal. Then:
 I_{k}=LPM([(P∪A)/(I_{k−1})]), if k is a nonlimit
ordinal.
 I_{k} = ∪_{i < k} I_{i}, if k is a limit ordinal.
The limit of the aforementioned inductive sequence exists and is unique, as
shown in [
WGK^{+}09], so the wellmounded model is welldefined and
is unique (provided the argumentation theory is fixed).
Wellfounded models are regarded as canonical models of Rulelog knowledge bases,
i.e., they determine the semantics of Rulelog. If P is a knowledge base,
A an argumentation theory, and φ we write
(P,A)=φ if and only if φ is true in the
WFM(P,A)=φ.
4.2 Semantics for Rulelog Syntactic Extensions
4.2.1 Path Expressions
The following transformation gives semantics to formulas that contain
generalized HiLog terms via a transformation to basic formulas.
First we define a transformation
unroll, which takes
a path expression and a pure HiLog term and replaces it with a conjunction
of frames and other atomic formulas. The resulting conjunction is true if
and only if the result of the path expression has an element that unifies
with the term.
 unroll(Expr,T) ~~~> Expr = T, if Expr is a pure HiLog term.
 unroll(Expr.S,T) ~~~> unroll(Expr,?newvar) and ?newvar[S>T], if Expr is a path
expression. Here ?newvar denotes a new variable that does not appear
anywhere in the surrounding rule.
 unroll(Expr[Spec_{1}, ..., Spec_{n}].S,T) ~~~> unroll(Expr,?newvar) and ?newvar[Spec_{1}, ..., Spec_{n},S>T], if Expr is a path
expression. Here again ?newvar is a new variable
and Spec_{1}, ..., Spec_{n} are the expressions that are allowed
inside frame formulas, as defined on page pageref.
Example 4.1:
Let Expr be the following path expression:
p(?X). q[foo>
23]. r(?x).s(?y). Then unroll(Expr,f(?y)) is
p(?X)[q>?V1, foo>23] and ?V1[r(?x)>?V2] and ?V2[s(?y)>f(?y)].
4.2.2 UserDefined Functions
The semantics of UDFs is defined by the following transformation.
A function definition of the form
function foo(t1,...,tn) := Expr if Definition.
is converted into the rule
newpred_foo(t1,...,tn,Expr) : Definition. 
 (1) 
where
newpred_foo is a new n+1ary predicate.
Then every occurrence of the nary function
foo in a rule head
head(...,foo(s1,...,sn),...) : Body.
is rewritten into
head(...,?newvar,...) : newpred_foo(s1,...,sn,?newvar), Body.
where
?newvar is a new variable.
In the rule body, any literal that has an occurrence of
foo(s1,...,sn) is rewritten as
follows:
... : ..., somepred(...,foo(s1,...,sn),...), ...
is replaced with
... : ..., newpred_foo(s1,...,sn,?newvar),
somepred(...,?newvar,...), ...
Again,
?newvar is a new variable here and
newpred_foo is
the predicate introduced above in (
1).
4.3 Argumentation Theories
In this section we describe the argumentation theories for defeasible reasoning
supported by Rulelog. The user can change the default argumentation theory via
a directive.
 General argumentation theory with multiway exclusions (AME)  the
default.
 Courteous argumentation theory with binary exclusions (CABE)  the
argumentation theory corresponding to the original Courteous logic
programming [Gro99].
 Cautious courteous
argumentation theory with binary exclusions (CCABE)  the
argumentation theory proposed in [WGK^{+}09].
Argumentation theories are
always loaded in their own
separate modules in order to not interfere with knowledge bases
specified by the users.
All argumentation theories have certain things in common. First, their sole
purpose is to define the predicate
\prolog, which determines
which facts derived by which rules are "defeated," i.e., the very fact of
their inference is to be ignored:
 \prolog(RuleTag,RuleHead,Module): If
\prolog(t,h,m) is true, then the effect is as if
every defeasible ground rule instance in module m that has h as its
head literal and t as its tag
is treated as if it were not in the knowledge base. The
formal semantics is given in Section 4.1.1.
The second thing that unites all argumentation theories is that they
take as input
certain predicates (and sometimes frame formulas) defined as part of the
user knowledge base. These predicates are listed below.
 \prolog(Tag_{1},Head_{1},Tag_{2},Head_{2}): This
predicate specifies that any inference made by a rule with the tag Tag_{1}
and head Head_{1} has higher precedence than inferences made by the rules
having the tag Tag_{2} and head Head_{2}.
For convenience, users can also use a twoargument version of this
predicate, which takes tags only. The two versions of this predicate are
related by the following rule:
\prolog(?Tag_{1}, ?, ?Tag_{2}, ?)
:
\prolog(?Tag_{1}, ?Tag_{2}).
Argumentation theories use only the 4ary version of this predicate.
 \prolog(Tag_{1},Head_{1},Tag_{2},Head_{2}):
This predicate says that inferences made by
the rules with the tag Tag_{1} and head Head_{1} are inconsistent with
inferences made by the rules with tag Tag_{2} and head Head_{2}.
The exact meaning is given by the actual argumentation theories.
This predicate is symmetric:
\prolog(t_{1},h_{1},t_{2},h_{2}) ≡
\prolog(t_{2},h_{2},t_{1},h_{1}).
and also
\prolog(?, h, ?, neg h) is true for any head
literal h.
For users' convenience, there is also a 2argument version of this
predicate, which is related to the 4ary predicate as follows:
\prolog(?, ?Head_{1}, ?, ?Head_{2})
:
\prolog(?Head_{1}, ?Head_{2}).
Argumentation theories use only the 4ary version of this predicate.
 Excl : \exclusion[\opposers>{H_{1},...,H_{n}}]:
This frame specifies exclusions. An exclusion is similar to opposition
except that it can involve more than two rule heads, but tags are not
taken into account. Such a frame says that H_{1}, ..., H_{n} are part of
the exclusion Excl and so they should not be derived together.
Exclusions are used only by the AME argumentation theory and their
precise meaning is specified by that theory.
 \cancel(Tag,Head): This predicate specifies when a
rule is canceled. A canceled rule is like a defeated rule, with
the difference that the reason for cancellation is given directly by the
user. This stands in contrast to the \prolog predicate,
which is defined by the argumentation theory and the user has no direct
control over it.
There is also a unary version of this predicate, which is related to the
binary version as follows:
\cancel(?Tag, ?) : \cancel(?Tag).
Argumentation theories use only the binary version of this predicate.
 strict(Tag,Head): This predicate specifies which
rules are strict based on their tag/head combination.
This predicate cannot be changed by the user directly. Instead, it is
specified indirectly through the defeasible statement
descriptor (see Section 3.3.4).
4.3.1 Argumentation Theory with Multiway Exclusions (AME)
The AME theory uses the notions of multiway rebuttal and refutation to
decide whether a particular rule is to be defeated.
These notions are fairly complex and can be best understood by reading the
rules of the argumentation theory.
Another way to be defeated is through disqualification by being canceled.
A cancellation rule can also be defeated by virtue of being overridden by
the rule that it tries to cancel.
Editor's Note 4.1:
This is ATCK1
/********************** \defeated ***************************/
// using general exclusions
\defeated(?Tag,?Head,?Mod) :
?Exclusion#\exclusion[\opposers>{?Head,?OtherH}]@?Mod,
?Head@?Mod != ?OtherH@?Mod,
candidate(?,?OtherH,?Mod),
naf ?Exclusion[\beater(?Mod)>?Head].
// using exclusions via \opposes
\defeated(?Tag,?Head,?Mod) :
\opposes(?Tag,?Head,?OtherT,?OtherH)@?Mod,
?Head@?Mod != ?OtherH@?Mod,
candidate(?OtherT,?OtherH,?Mod),
naf \beater(?Head,?OtherH,?Mod).
// defeat via disqualification
\defeated(?Tag,?Head,?Mod) : disqualified(?Tag,?Head,?Mod).
/*********************** disqualification ***********************/
disqualified(?Tag,?Head,?Mod) :
beaten_by_strict_rule(?Tag,?Head,?TagOther,?HeadOther,?Mod).
disqualified(?Tag,?Head,?Mod) : \cancel(?Tag,?Head)@?Mod.
disqualified((?Tag1,${\cancel(?Tag2,?H2)@?Mod}),?Mod) :
\overrides(?Tag2,?H2,?Tag1,${\cancel(?Tag2,?H2)})@?Mod.
/***** refutation via competition through general exclusions ****/
refutes(?H1,?T2,?H2,?Exclusion,?Mod) :
competes(?H1,?H2,?Exclusion,?Mod),
\overrides(?T1,?H1,?T2,?H2)@?Mod,
candidate(?T1,?H1,?Mod).
/******* refutation via competition through \opposes ********/
refutes(?H1,?T2,?H2,?Mod) :
competes(?H1,?H2,?Mod),
\overrides(?T1,?H1,?T2,?H2)@?Mod,
candidate(?T1,?H1,?Mod).
/****** rebuttal via competition through general exclusions *****/
rebuts(?H1,?H2,?Exclusion,?Mod) :
competes(?H1,?H2,?Exclusion,?Mod),
candidate(?T1,?H1,?Mod),
naf refutes(?H2,?T1,?H1,?Exclusion,?Mod).
/******** rebuttal via competition through \opposes ********/
rebuts(?H1,?H2,?Mod) :
competes(?H1,?H2,?Mod),
candidate(?T1,?H1,?Mod),
naf refutes(?H2,?T1,?H1,?Mod).
/**************************** competition ***********************/
competes(?H1,?H2,?Exclusion,?Mod) :
?Exclusion#\exclusion[\opposers>{?H1,?H2}]@?Mod,
?H1 != ?H2.
competes(?H1,?H2,?Mod) :
\opposes(?T1,?H1,?T2,?H2)@?Mod,
?H1 != ?H2.
/**************************** candidacy *************************/
candidate(?Tag,?H,?Mod) :
clause{@{?Tag} ?H@?Mod, ?Body},
?Body.
strict_candidate(?Tag,?H,?Mod) :
\strict(?Tag,?H)@?Mod,
// metapredicate to get body of a rule
clause{@{?Tag} ?H@?Mod, ?Body},
?Body.
/***************************** battery **************************/
?Exclusion[\beater(?Mod)>?H] :
// competition via general exclusions
competes(?H,?Beaten,?Exclusion,?Mod),
naf rebuts(?Beaten,?H,?Exclusion,?Mod).
\beater(?H,?Beaten,?Mod) :
// competition via \opposes
competes(?H,?Beaten,?Mod),
naf rebuts(?Beaten,?H,?Mod).
beaten_by_strict_rule(?T,?H,?Tstrict,?Hstrict,?Mod) :
candidate(?T,?H,?Mod),
\opposes(?T,?H,?Tstrict,?Hstrict)@?Mod,
strict_candidate(?Tstrict,?Hstrict,?Mod).
4.3.2 Cautious Argumentation Theory with Multway Exclusions (CAME)
Editor's Note 4.2:
TODO. This will be a fixedup ATCK2.
4.3.3 Argumentation Theory with Binary Exclusions (ABE)
The ABE theory also uses the notions of
refutation, rebuttal, and disqualification in order to determine if a
rule is to be defeated. The disqualification rules are the same as before,
but the refutation and rebuttal rules are much simpler and straightforward.
Editor's Note 4.3:
This is the old GCLP
/********************** \defeated ***************************/
\defeated(?Tag,?Head,?Mod) :
defeats(?OtherTag,?OtherHead,?Tag,?Head,?Mod).
\defeated(?Tag,?Head,?Mod) : disqualified(?Tag,?Head,?Mod).
defeats(?T1,?H1,?T2,?H2,?Mod) : refutes(?T1,?H1,?T2,?H2,?Mod).
defeats(?T1,?H1,?T2,?H2,?Mod) : rebuts(?T1,?H1,?T2,?H2,?Mod).
/*********************** disqualification ***********************/
disqualified(?Tag,?Head,?Mod) :
beaten_by_strict_rule(?Tag,?Head,?TagOther,?HeadOther,?Mod).
disqualified(?Tag,?Head,?Mod) : \cancel(?Tag,?Head)@?Mod.
disqualified((?Tag1,${\cancel(?Tag2,?H2)@?Mod}),?Mod) :
\overrides(?Tag2,?H2,?Tag1,${\cancel(?Tag2,?H2)})@?Mod.
/******************* refutation and rebuttal ********************/
refutes(?T1,?H1,?T2,?H2,?Mod) :
\overrides(?T1,?H1,?T2,?H2)@?Mod,
conflicts(?T1,?H1,?T2,?H2,?Mod).
rebuts(?T1,?H1,?T2,?H2,?Mod) :
conflicts(?T1,?H1,?T2,?H2,?Mod),
naf refuted(?T1,?H1,?Mod),
naf refuted(?T2,?H2,?Mod).
conflicts(?T1,?H1,?T2,?H2,?Mod) :
\opposes(?T1,?H1,?T2,?H2)@?Mod,
candidate(?T1,?H1,?Mod),
candidate(?T2,?H2,?Mod).
refuted(?T,?H,?Mod) : refutes(?OtherT,?OtherH,?T,?H,?Mod).
/**************************** candidacy *************************/
candidate(?Tag,?H,?Mod) :
clause{@{?Tag} ?H@?Mod, ?Body},
?Body.
strict_candidate(?Tag,?H,?Mod) :
\strict(?Tag,?H)@?Mod,
// metapredicate to get body of a rule
clause{@{?Tag} ?H@?Mod, ?Body},
?Body.
/***************************** battery **************************/
beaten_by_strict_rule(?T,?H,?Tstrict,?Hstrict,?Mod) :
\opposes(?T,?H,?Tstrict,?Hstrict)@?Mod,
strict_candidate(?Tstrict,?Hstrict,?Mod).
4.3.4 Cautious Argumentation Theory with Binary Exclusions (CABE)
The CABE theory is similar to the ABE theory, but it is more cautious in
deciding when a rule is to be defeated. First, in order for another rule to
be a cause of defeat of a rule, that other rule must not itself be
refuted and defeated. Second, a rule may be disqualified for one additional
reason: it may transitively defeat itself.
This theory typically results in fewer rules being defeated and a larger
number of facts might become undefined compared to ABE.
Editor's Note 4.4:
This is the new GCLP
/********************** \defeated ***************************/
\defeated(?Tag,?Head,?Mod) :
defeats(?OtherTag,?OtherHead,?Tag,?Head,?Mod),
naf compromised(?OtherTag,?OtherHead,?Mod).
\defeated(?Tag,?Head,?Mod) : disqualified(?Tag,?Head,?Mod).
defeats(?T1,?H1,?T2,?H2,?Mod) : refutes(?T1,?H1,?T2,?H2,?Mod).
defeats(?T1,?H1,?T2,?H2,?Mod) : rebuts(?T1,?H1,?T2,?H2,?Mod).
/*********************** disqualification ***********************/
disqualified(?Tag,?Head,?Mod) :
transitively_defeats(?Tag,?Head,?Tag,?Head,?Mod).
disqualified(?Tag,?Head,?Mod) :
beaten_by_strict_rule(?Tag,?Head,?TagOther,?HeadOther,?Mod).
disqualified(?Tag,?Head,?Mod) : \cancel(?Tag,?Head)@?Mod.
disqualified((?Tag1,${\cancel(?Tag2,?H2)@?Mod}),?Mod) :
\overrides(?Tag2,?H2,?Tag1,${\cancel(?Tag2,?H2)})@?Mod.
/******************* refutation and rebuttal ********************/
refutes(?T1,?H1,?T2,?H2,?Mod) :
\overrides(?T1,?H1,?T2,?H2)@?Mod,
conflicts(?T1,?H1,?T2,?H2,?Mod).
rebuts(?T1,?H1,?T2,?H2,?Mod) :
conflicts(?T1,?H1,?T2,?H2,?Mod),
naf compromised(?T1,?H1,?Mod).
conflicts(?T1,?H1,?T2,?H2,?Mod) :
\opposes(?T1,?H1,?T2,?H2)@?Mod,
candidate(?T1,?H1,?Mod),
candidate(?T2,?H2,?Mod).
compromised(?T,?H,?Mod) :
refuted(?T,?H,?Mod),
defeated(?T,?H,?Mod).
refuted(?T,?H,?Mod) : refutes(?OtherT,?OtherH,?T,?H,?Mod).
rebutted(?T,?H,?Mod) : rebuts(?OtherT,?OtherH,?T,?H,?Mod).
/**************************** candidacy *************************/
candidate(?Tag,?H,?Mod) :
clause{@{?Tag} ?H@?Mod, ?Body},
?Body.
strict_candidate(?Tag,?H,?Mod) :
\strict(?Tag,?H)@?Mod,
// metapredicate to get body of a rule
clause{@{?Tag} ?H@?Mod, ?Body},
?Body.
/***************************** battery **************************/
beaten_by_strict_rule(?T,?H,?Tstrict,?Hstrict,?Mod) :
\opposes(?T,?H,?Tstrict,?Hstrict)@?Mod,
strict_candidate(?Tstrict,?Hstrict,?Mod).
/************************** transitive defeat *******************/
transitively_defeats(?T1,?H1,?T2,?H2,?Mod) :
defeats(?T1,?H1,?T2,?H2,?Mod).
transitively_defeats(?T1,?H1,?T3,?H3,?Mod) :
transitively_defeats(?T2,?H2,?T3,?H3,?Mod),
defeats(?T1,?H1,?T2,?H2,?Mod).
4.4 Additional Background Axioms
This section describes the axioms that are part of the Rulelog semantics, but
are not covered by the direct modeltheoretic semantics of
Section
4.1.
4.5 Semantic Directives
This section defines the directives that directly affect the semantics of Rulelog.
 Directive that affects the argumentation theory.
 Directive for turning off equality maintenance.
 Directives to turn on various optimizations.
Editor's Note 4.5:
The above directives are to be decided upon.
5 Rulelog Builtins and Their Semantics
References
 [BBB^{+}05]

S. Battle, A. Bernstein, H. Boley, B. Grosof, M. Gruninger, R. Hull, M. Kifer,
D. Martin, S. McIlraith, D. McGuinness, J. Su, and S. Tabet.
SWSL: Semantic Web Services Language.
Technical report, W3C, April 2005.
http://www.w3.org/Submission/SWSFSWSL/.
 [BM04]

Paul V. Biron and Ashok Malhotra.
XML schema part 2: Datatypes second edition.
Recommendation 28 October 2004, W3C, 2004.
 [BM08]

M. Birbeck and S. McCarron.
CURIE Syntax 1.0: A syntax for expressing compact URIs.
Technical report, W3C, May 2008.
http://www.w3.org/TR/curie/.
 [DG05]

M. Duerst and M. Guignard.
Internationalized resource identifiers (iris).
Technical report, Internet Engineering Task Force, January 2005.
http://www.ietf.org/rfc/rfc3987.txt.
 [GDG^{+}]

B. Grosof, M. Dean, S. Ganjugunte, S. Tabet, , and C. Neogy.
SweetRules: An open source platform for semantic web business
rules.
Web site.
http://sweetrules.projects.semwebcentral.org/.
 [Gro99]

B.N. Grosof.
A courteous compiler from generalized courteous logic programs to
ordinary logic programs.
Technical Report RC 21472, IBM, July 1999.
 [KYWZ13]

M. Kifer, G. Yang, H. Wan, and C. Zhao.
FLORA2: User's manual.
The FLORA2 Web Site, 2013.
http://flora.sourceforge.net/docs/floraManual.pdf.
 [Llo87]

J.W. Lloyd.
Foundations of Logic Programming (Second Edition).
SpringerVerlag, 1987.
 [Prz94]

T. Przymusinski.
Wellfounded and stationary models of logic programs.
Annals of Mathematics and Artificial Intelligence, 12:141187,
1994.
 [SW11]

T. Swift and D.S. Warren.
Xsb: Extending the power of prolog using tabling.
Theory and Practice of Logic Programming, 2011.
 [VRS91]

A. Van Gelder, K.A. Ross, and J.S. Schlipf.
The wellfounded semantics for general logic programs.
Journal of ACM, 38(3):620650, 1991.
 [WGK^{+}09]

H. Wan, B. Grosof, M. Kifer, P. Fodor, and S. Liang.
Logic programming with defaults and argumentation theories.
In Int'l Conference on Logic Programming, July 2009.
Index (showing section)
 ≤_{t} truthorder,
4.1
 Consts, 3.1, 3.1
 @tag, see tag, property of rule descriptor
 @@defeasible,
see defeasible, property of rule descriptor
 @@strict,
see strict, property of rule descriptor
 Vars, 3.1
 \doubledatatype, 3.1,
3.2
 \integerdatatype, 3.1,
3.2
 \stringdatatype, 3.1,
3.2
 abstract domain, 4.1
 aggregation term, 3.3
 alphabet of Rulelog, 3.1
 association of formulas to modules,
3.3
 basic formula
 comparison, 3.3
 disequality, 3.3
 equality, 3.3
 evaluable expression,
3.3
 frame, 3.3
 HiLog, 3.3
 membership, 3.3
 signature, 3.3
 subclass, 3.3
 body
 of rule, 3.3
 Boolean method, 3.3

 comment, 3.5
 multiline, 3.5
 singleline, 3.5
 comparison formula, 3.3
 compound formula, 3.3
 comprehension term, 3.3
 congruence relative to equality,
4.1
 conjunctive formula, 3.3
 constant, 3.1
 CURIE, 2.0
 prefix, 2.0
 prefix declaration,
3.5
 datatype, 3.1, 3.2
 \double, 3.1,
3.2
 \integer, 3.1,
3.2
 \string, 3.1,
3.2
 defaultnegated literal,
3.3
 defeasibility flag, 3.3
 defeasible, 3.3
 defeasible, property of rule descriptor,
3.4
 delay quantifier, 3.7
 descriptor
 defeasible, 3.4
 of rule, 3.3
 of statement, 3.4
 strict, 3.4
 tag, 3.4
 disequality
 formula, 3.3
 disunification
 formula, 3.3

 empty semantic structure,
4.1
 equality
 formula, 3.3
 evaluable expression, 3.3
 explicitlynegated literal,
3.3
 export statement, 3.5
 extended Herbrand universe,
4.1
 fact, 3.3
 factor (of a set by equivalence relation),
4.1
 firstorder
 term, 3.3
 foreign
 formula, 3.3
 path expression, 3.4
 formula
 compound, 3.3
 conjunctive, 3.3
 defaultnegated literal,
3.3
 explicitlynegated literal,
3.3
 foreign, 3.3
 frame, 3.3
 parenthesized, 3.3
 signature, 3.3
 term, 3.3
 formula template, 3.5
 frame formula
 method in, 3.3
 property in, 3.3
 function
 UDF, 3.4
 userdefined, 3.4

 ground term, 4.1
 head
 of rule, 3.3
 HiLog
 formula, 3.3
 generalized term, 3.4
 pure term, 3.3
 term, 3.3
 import statement, 3.5
 international resource identifier,
3.1
 interpreted symbol, 3.1
 IRI, 3.1
 least model, 4.1
 lexical space, 3.2
 lexicaltovaluespace mapping,
3.2
 list term, 3.3
 literal
 defaultnegated, 3.3
 explicitlynegated,
3.3
 positive, 3.3
 LloydTopor biimplication,
3.7
 LloydTopor Extensions
 Monotonic,
3.7
 LloydTopor implication,
3.7
 LloydTopor transformations
 monotonic,
3.7
 nonmonotonic,
3.7

 macro, 3.5
 membership
 formula, 3.3
 method
 Boolean, 3.3
 method (in frame formula),
3.3
 model
 least, 4.1
 of formula, 4.1
 of knowledge base with respect to argumentation theory,
4.1
 wellfounded, 4.1
 module
 name, 3.4
 reference, 3.4
 Monotonic LloydTopor Extensions,
3.7
 monotonic LloydTopor transformations,
3.7
 nonmonotonic LloydTopor transformations,
3.7
 owl (a prefix), 2.0
 parenthesized
 formula, 3.3
 term, 3.3
 path expression, 3.4
 foreign, 3.4
 transformation into frames,
4.2
 unrolling, 4.2
 positive literal, 3.3
 prefix
 declaration for CURIE,
3.5
 in CURIE, 2.0
 owl, 2.0
 rdf, 2.0
 rdfs, 2.0
 rif, 2.0
 rlg, 2.0
 silk, 2.0
 xsd, 2.0
 property (in frame formula),
3.3

 quantifier
 delay, 3.7
 query, 3.3
 rdf (a prefix), 2.0
 rdfs (a prefix), 2.0
 reification term, 3.3
 rif (a prefix), 2.0
 rlg (a prefix), 2.0
 rule, 3.3
 body, 3.3
 head, 3.3
 Rulelog abstract symbol,
3.1
 Rulelog quotient, 4.1
 semantic structure, 4.1
 empty, 4.1
 truthorder on,
4.1
 signature formula, 3.3
 silk (a prefix), 2.0
 skolemization, 3.4
 statement descriptor, 3.4
 strict, 3.3
 strict, property of rule descriptor,
3.4
 subclass
 formula, 3.3
 symbol
 datatype, 3.1
 interpreted, 3.1
 IRI, 3.1
 Rulelog abstract, 3.1
 uninterpreted, 3.1
 with explicit symbol space,
3.1
 symbol space, 3.1,
3.2
 datatype as, 3.2
 name, 3.2

 tag property of rule descriptor,
3.4
 term
 aggregation, 3.3
 comprehension, 3.3
 firstorder, 3.3
 foreign path expression,
3.4
 generalized HiLog,
3.4
 ground, 4.1
 HiLog, 3.3
 list, 3.3
 parenthesized, 3.3
 path expression, 3.4
 pure HiLog, 3.3
 reification, 3.3
 term formula, 3.3
 terminterpreting mapping,
4.1
 truthorder ≤_{t},
4.1
 UDF, 3.4
 unification
 formula, 3.3
 uninterpreted symbol, 3.1
 unroll transform, 4.2
 userdefined function, 3.4

 value space, 3.2
 variable, 3.1
 wellfounded model, 4.1
 xsd (a prefix), 2.0

Footnotes:
^{1}
Subject to the restrictions of Section
3.3.4. Namely: these
basic formulas cannot be comparison formulas or evaluable expressions.
^{2}
Recall that
monotonic LloydTopor extensions permit these implications
only in rule heads.