DELORES − a defeasible logic interpreter
delores [−q] [−an|−An] [−rn|−Rn] [−mn] [in-file]
delores −−help
delores −−version
DELORES (DEfeasible LOgic REasoning System) is a forward-chaining reasoning engine for defeasible logic, a less-expressive but more efficient non-monotonic logic. In contrast with most other non-monotonic logics, defeasible logic has linear complexity, allowing DELORES to execute large theories very quickly. DELORES’s algorithm extends to general defeasible theories through the use of a pre-processing transformation which eliminates all uses of defeaters and superiority relations. The transformation was designed to provide incremental transformation of defeasible theories, and systematically uses new atoms and new defeasible rules to simulate the eliminated features.
−q |
Quiet mode −− nonessential messages are suppressed. | ||
−an |
Make the atom hash table size the smallest prime greater than or equal to n. | ||
−An |
Make the atom hash table size exactly n. | ||
−rn |
Make the rule hash table size the smallest prime greater than or equal to n. | ||
−Rn |
Make the rule hash table size exactly n. | ||
−mn |
Pre-allocate memory in n-byte chunks. It is strongly recommended that n be a power of 2. In absence of this option, the chunk size defaults to 65536 bytes. This option is available only if DELORES is compiled with the BGET memory allocator. | ||
−−help |
Print a brief list of command-line arguments and then quit. |
−−version
Print out version and copyright information and then quit. If the BGET memory management routines have been compiled in, this will be noted in the version information.
in-file
Process the theory contained in the named file and then quit. If no input file is specified, DELORES starts up in interactive mode.
Regarding hash table sizes, n should be a prime number, or at least not divisible by a small prime; for this reason, it is recommended that the −a and −r options be used if n is not known for certain to be prime. In absence of any options setting the atom or rule hash table sizes, the default is 10^6 + 3.
Note that the ranges of acceptable values for options taking integer arguments are system-dependant. While DELORES makes every effort to report argument values which are too large, there remains a small chance that overflow errors will go undetected. For this reason, DELORES prints the atom hash table size, rule hash table size, and, if applicable, memory chunk size at startup (in non-quiet mode). If the numbers do not correspond to the values specified on the command line, try invoking DELORES again with smaller argument values.
A name is any sequence of one or more digits, letters, and underscores which begins with a lowercase letter. A label is any sequence of one or more digits, letters, underscores, and forward slashes which begins with a letter or a slash. A filename is any sequence of one or more characters except newlines. In terms of regular expressions, these three basic patterns can be represented as follows:
name ::= [a-z][A-Za-z0-9_]*
label ::= [A-Za-z/][A-Za-z0-9_/]*
filename ::= .+
Note: Users may not define rules with labels containing the ‘/’ character; this character is reserved for rules named by the interpreter.
METASYNTAX
In this manual the following BNF-like notational conventions
are used for expressing DELORES syntax:
[ pattern ]
optional
( pattern )
grouping
pattern1 | pattern2
choice of either pattern1 or pattern2
"literal"
interpret quoted text literally
It should be noted that all white space (tabs, spaces, and newlines) between tokens is ignored. Thus, white space may be omitted when the omission does not lead to ambiguity.
BASIC TOKENS
NOT ::= "neg" | "not" |
SARROW ::= ":-" | "<-"
DARROW ::= ":=" | "<="
DEFARROW ::= ":^" | "<~"
DL_TRUE ::= "true"
DL_FALSE ::= "false"
THEORY CONSTRUCTS
program ::= [ program ] statement "." |
statement ::= rule | fact | suprel | directive
suprel ::= label ( "<" | ">" ) label
atom ::= name
term ::= variable | name
lliteral ::= [ NOT ] atom
literal ::= ( lliteral | [ NOT ] ( DL_TRUE | DL_FALSE ) )
fact ::= [ "unknown" ] lliteral
rule ::= srule | drule | defeater
litlist ::= [ litlist "," ] literal
srule ::= [ label ":" ] lliteral SARROW litlist
drule ::= [ label ":" ] lliteral DARROW litlist
defeater ::= [ label ":" ] lliteral DEFARROW litlist
INTERPRETER
DIRECTIVES
Interpreter directives are special commands issued to the
interpreter which do not, strictly speaking, form part of
the user’s theory. They are used for reading and
printing theories, executing the inference engine, and
terminating the interpreter. Interpreter directives are
considered statements for the purposes of the language
grammar.
directive ::= listing | print | infer | end | include |
listing ::= "listing" [ "(" label ")" ]
print ::= "print" "(" atom ")"
infer ::= "infer"
end ::= "end"
include ::= "include" "(" filename ")"
THEORY
CONSTRUCTS
A discussion of the semantics of the theory constructs is
well beyond the scope of this manual; please refer to the
papers by Maher et al. listed near the end of this
document.
INTERPRETER
DIRECTIVES
include
The include directive is used to read and interpret a theory file on disk. The specified file will be read from disk as if it were entered via standard input. The maximum nesting depth for include is 16 files; this limit prevents infinite loops from two or more files which include each other.
listing
When called without arguments, the listing directive prints a list of all rules in the theory, in the order they were initially created. If the user supplies a rule label as an argument, only that rule is printed (if it exists).
|
This directive takes the name of an atom, a, as its argument. All conclusions about a and its negation are printed, as well as the labels of all rules where a or its negation is the head. See the following section for an explanation of the format used for the conclusions. | ||
infer |
This directive executes the defeasible logic inference engine. Timing information is printed upon completion. | ||
end |
The end directive indicates that the interpretation is over. No further statements are read. This directive is optional at the end of a file, as the interpretation will simply end when there is no further data in standard input. |
After running the infer directive, various conclusions of a defeasible theory T can be printed using the print directive. A conclusion of T is a tagged literal and can have one of the following four forms:
+Dq |
This means that q is definitely provable in T (i.e., using only facts and strict rules). | ||
-Dq |
This means that we have proved that q is not definitely provable in T. | ||
+dq |
This means that q is defeasibly provable in T. | ||
-dq |
This means that we have proved that q is not defeasibly provable in T. |
SYNTAX
ERRORS
Syntax errors are detected during reading. Each statement
that fails to comply with syntax requirements causes DELORES
to print a "parse error" message listing the
filename, line number, and if possible, the exact token at
which the error occurred. The interpretation will then
continue as if the erroneous statement were never entered.
In batch mode (that is, when DELORES is processing a theory
file given on the command line or with an include
directive), DELORES will print out the first sixteen syntax
errors before aborting the interpretation. In interactive
mode, a syntax error will never cause the interpretation to
abort, as it is assumed that the user will correct the error
upon reading the error message.
FATAL
ERRORS
Fatal errors include system errors such as running out of
memory or attempting to open a theory file (via
include or a command-line argument) that does not
exist or cannot be opened, and other exceptional cases such
as exceeding the include nesting depth. As the name
implies, fatal errors result in immediate termination of the
interpreter. As with syntax errors, DELORES will attempt to
identify the exact point in input at which the error
occurred. The list of the most common fatal errors is as
follows:
out of memory!
atom table too big for available memory!
rule table too big for available memory!
cannot insert into rule table
cannot insert into atom table
There is not sufficient memory for the interpretation to continue. Try using the command-line arguments to decrease the size of the hash tables and/or the memory chunk size (if applicable). Failing that, if DELORES has been compiled with the BGET memory allocator, try recompiling it with the BGET BestFit macro set, or even without BGET support at all. The resulting interpreter may be slower, but it will probably use less memory. If recompiling is not an option or does not solve the problem, consult your operating system’s documentation for hints on increasing the amount of memory available to DELORES.
too many nested includes
The include directive has a maximum nesting depth of 16. It is unlikely that files would ever be nested to this depth in practice; if this error occurs it is most likely that an infinite loop has arisen from a particular file includeing itself indirectly.
no such file or directory
The user has instructed the interpreter to read in a file which either does not exist, or is otherwise unopenable. Check that the path, filename, and file permissions are correct.
There are other fatal errors which DELORES may produce in the extremely unlikely event that certain system limits are exceeded, or if the interpreter encounters some completely unexpected error condition. In these cases, please contact the program’s maintainer with the exact error message given, as well as instructions on how to reproduce the error.
WARNINGS
Warning messages indicate an anomaly that may be of interest
to the user, though it is unlikely interfere with the
interpretation. The warnings are as follows:
warning: ignoring redefinition of rule
The same label has been used to define two separate rules. The second rule is ignored; if it is to be entered into the theory, then its label should be changed or omitted.
warning: rule count overflow
DELORES assigns every rule an identifying number so that the listing directive prints out the rules in the order they were entered. This message indicates that DELORES has run out of unique numbers for the rules; consequently, listing can no longer be guaranteed to print rules in the proper order.
warning: same rule appears on both sides of of superiority relation
This message is printed when a superiority relation such as rule2 > rule2 is entered. Such a declaration makes no sense semantically.
/usr/local/share/delores/primes.txt
List of prime numbers used by the −a and −r options.
The only known bug in the interpreter has to do with its processing of include directives; sometimes the filename is not properly recognized. To avoid any potential problems, users are cautioned to place their include directives on lines separate from any other statements.
Please report bugs to <Tristan.Miller@dfki.de>.
Michael J. Maher, Allan Rock, Grigoris Antoniou, David Billington, and Tristan Miller. Efficient defeasible reasoning systems. International Journal on Artificial Intelligence Tools, 10(4):483-501, 2001.
Michael J. Maher, Allan Rock, Grigoris Antoniou, David Billington, and Tristan Miller. Efficient defeasible reasoning systems. In Proceedings of the 12th IEEE International Conference on Tools with Artificial Intelligence, pages 384-392, 2000.
More publications on DELORES and defeasible reasoning are available on Michael Maher’s publications page: http://www.math.luc.edu/~mjm/pubs/#DL
DELORES home page: http://www.dfki.uni-kl.de/~miller/delores/
DELORES was conceived by Michael Maher <mjm@math.luc.edu> and implemented by Tristan Miller <Tristan.Miller@dfki.de>. DELORES uses BGET, a public domain memory allocation library by John Walker.
Copyright
(C) 1999, 2000 Michael Maher.
Copyright (C) 1999, 2000, 2003 Tristan Miller.
Permission is granted to anyone to make or distribute verbatim copies of this document as received, in any medium, provided that the copyright notice and this permission notice are preserved, thus giving the recipient permission to redistribute in turn.
Permission is granted to distribute modified versions of this document, or of portions of it, under the above conditions, provided also that they carry prominent notices stating who last changed them.