DePYsible is a Python implementation of Defeasible Logic for argumentation. In particular, Defeasible Logic is a non-monotonic logic proposed to formalize defeasible reasoning and argumentation.
In a nutshell, Defeasible Logic supports three types of propositions:
- strict rules: to specify known facts or information that is always a consequence of other sure facts,
- defeasible rules: to specify information that is typically or possibly a consequence of other information,
- undercutting defeaters: to specify exceptions to defeasible rules.
Some approaches like the one used in this implementation, the undercutting defeaters are derived by identifying the defeating arguments among conflicting ones. (An argument relates to a fact called conclusion and includes the list of defeasible rules that have to be true to make the conclusion to hold.)
A priority ordering over the defeasible rules and the defeaters can be given or inferred by the generalised specificity of the arguments. Intuitively, this comparison criterion favours two aspects: it prefers arguments (1) with greater information content or (2) with less use of rules (more direct). In other words, given two conflicting arguments, the defeater is the more precise or more concise among them. Arguments that have the same generalised specificity can be ordered by means of user-specified priorities on the rules.
During the process of deduction, the strict rules are always applied, while a defeasible rule can be applied only if no defeater of a higher priority specifies that it should not. This process decides if each defeasible fact is true, false or undecided and provides the clues supporting these decisions.
> git clone https://github.com/stefano-bragaglia/DePYsible.git ./depysible
> cd depysible
> pip install virtualenv
> virtualenv --python=python3.6 .env
> source ./.env/bin/activate
> pip install pybuilder
> pyb install_dependencies
> pyb install
> depysible example.pl
% Strict rules
bird(X) <- chicken(X).
bird(X) <- penguin(X).
~flies(X) <- penguin(X).
% Facts
chicken(tina).
penguin(tweety).
scared(tina).
% Defeasible knowledge
flies(X) -< bird(X).
flies(X) -< chicken(X), scared(X).
~flies(X) -< chicken(X).
nests_in_trees(X) -< flies(X).
This program is a typical Defeasible Logic program that states that every chicken is a bird, that every penguin is a bird and that penguins don't fly (strict rules). We also know that Tina is a chicken, Tweety is a penguin and that Tina is scared (facts).
The program then says that birds can possibly fly, that scared chickens might fly, that chickens usually don't fly and that flying animals usually nest in trees (defeasible knowledge).
The argumentative procedure for Defeasible Logic can derive, for instance, that Tweety doesn't fly for sure (directly entailed from the strict knowledge) but also that Tina flies because she's scared (defeasibly entailed from the strict knowledge and flies(X) -< chicken(X), scared(X).
).
DePYsible is an application developed in Python 3.6.5 and requires Python 3.6.x (or later) to run. A more recent version of Python for your working environment, if needed, can be downloaded from the official Python website.
It is possible to use a virtual environment and install DePYsible in a sandbox into a user directory. Virtualenv is possibly the most popular tool to create isolated Python environments. Assuming that Python 3.6.x (or later) has been successfully installed, Virtualenv can be installed globally by running on a command line:
pip install virtualenv
The instructions to create a virtual environment can be found below.
Assuming that a virtual environment is available in a folder named .env
, it is activated by:
source ./.env/bin/activate
and deactivated by running:
deactivate
DePYsible's sources can be downloaded from github.com/stefano-bragaglia/DePYsible.git.
Alternatively, they can be cloned by issuing the following command on your terminal:
git clone https://github.com/stefano-bragaglia/DePYsible.git ./depysible
The interpreter might soon become available on pypi.org too. Once available, it will be possible to directly installing it into the current virtual (or global) Python environment (see above) with:
pip install DePYsible
If DePYsible has been installed as a package on a virtual (or global) Python environment, the compiling is not required. Otherwise compiling is mandatory, but DePYsible supports PyBuilder which simplifies this step.
Assuming that Python 3.6.x (or later)_ and Virtualenv are already installed (see here), it's highly recommended to create a local virtual environment by running:
cd ./depysible
virtualenv --python=python3.6 .env
The next step consists in installing PyBuilder in the local virtual environment after having activated it:
source ./.env/bin/activate
pip install pybuilder
PyBuilder is a build automation tool automates all the repetitive operations during the life cycle of the application such as installing the dependencies, testing the sources, compiling the sources, etc. In order to compile and install DePYsible, run the following commands:
pyb install_dependencies
pyb install
From now on, any time the local virtual environment is activated, the command depysible
becomes available on the command line.
DePYsible comes as a command line interface application. Once it has been installed (see above), DePYsible can be simply run by invoking it at the prompt:
> depysible
Welcome to Defeasible 0.1.0 (Darwin-18.0.0-x86_64-i386-64bit)
Defeasible comes with ABSOLUTELY NO WARRANTY. This is free software.
Type "help", "copyright", "credits" and "license" for more information.
?-
If no parameters is given, DePYsible is run with default configuration.
By passing -h
or --help
as a parameter, the list of possible parameters is returned:
> depysible --help
usage: depysible [-h] [-b] [filename]
positional arguments:
filename load the file with given name
optional arguments:
-h, --help show this help message and exit
-b, --blind ignore colours to render output
This parameter will display the list of possible parameters for DePYsible, as shown above.
Normally, DePYsible highlights the syntax of program that it holds in memory.
At the moment, only the dark theme displayed in the opening screenshot is supported.
On different setups, this theme might not render well or some people might find the syntax highlighting distracting.
In either cases the -b
, --blind
parameter will help by turning off the syntax highlighting.
When given, this parameter will preload the program contained in the file with the given name into the DePYsible interpreter.
For instance, the following command will load example.pl
into memory when started:
> depysible example.pl
DePYsible is a command-line interpreter application. When started, it enters into a loop that displays a message on the screen and then waits for a user's input.
Normally DePYsible presumes that a program is already loaded in memory, and assumes that anything the user types is a valid statement for its language. Valid statements are either sets of rules or just literals (see language below).
Any valid set of rules is automatically appended to the program currently in memory. The following input, for instance, adds a strict rule (every chicken is a bird) and a fact (Tina is a chicken):
?- bird(X) <- chicken(X). chicken(tina).
Any literal, instead, triggers the defeasible argumentation algorithm which checks whether it is true or not according to the information available on the domain.
Assuming that example.pl
has been loaded into memory, the given input triggers the following output:
?- ~flies(tina)
NO
flies(tina) -< chicken(tina), scared(tina).
This output means that the interpreter believes the fact "Tina does not fly" to be false because the opposite could be derived from the strict domain's knowledge and the given ground rules (if any): Tina, being a chicken, could fly if scared.
The interpreter accepts more specialised commands that are introduced in alphabetical order in the following sections.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
Heu, rusticus amor! Accentor de emeritis aonides, anhelare elevatus! Emeritis, albus itineris tramitems semper quaestio de magnum, placidus imber. Brevis ollas ducunt ad homo. Orexiss sunt rectors de mirabilis lanista. A falsis, absolutio nobilis cobaltum.
The minimal bit of information in Defeasible Logic is the atom.
Each atom consists of a functor and a possibly empty list of terms.
The number of terms is known as the arity of the atom (if no term is specified, the arity of the atom is zero).
A functor is either an identifier (a sequence of alphanumeric characters beginning with a lowercase letter) or a string.
Notice that a string is any sequence of characters enclosed in either double quotes or single quotes.
The following, for example, are all valid atoms (and their arities): atom
(0), "STILL AN ATOM"
(0), parent_of(homer, bart)
(2), 'has age'(bart, 10)
(2).
This implementation of Defeasible Logic supports strong negation (symbol: ~
).
Given an atom (i.e.: sky(blue)
), its strong negation consists in its complement (~sky(blue)
).
From a practical point of view, a complement is treated as a new atom that is false if the original atom is true, and vice versa.
Strong negation should not be confused with negation as failure (or default negation ⎯ currently not implemented).
From now on, we will refer to an atom or its complement as a literal.
Negation as failure, in fact, allows to consider something true if it is not possible to derive its complement from the context. Generally speaking, negation as failure is more powerful as it allows to deduce the truth value of an atom even though if it is not already available. Strong negation, however, is more conservative since it only allows to consider an atom true or false if it is defined as such, and makes no assumptions otherwise. The difference between the two kinds of negations it's similar to the difference between the inference in open-world and close-world assumption.
Literals can be combined together to form more expressive structures.
Rules (or clauses), in particular, consists of two sequences of literals called respectively head and body connected by the entailment symbol :-
(read if).
The meaning of these structures is that when all the literals in the body hold, then the literals in the head can be considered true.
In first-order logic, the heads usually consist of 1 literal and the bodies of 0 or more literals.
The following rules are hence all valid:
grandparent_of(X, Y) :- parent_of(X, Z), parent_of(Z, Y).
parent_of(abe, homer).
parent_of(homer, bart).
In Defeasible Logic, however, there are two kinds of rules: strict and defeasible.
A strict rule uses <-
as entailment symbol and is a strong implication of the head from its body (the head is true if the body holds).
A strict rule with an empty body is called fact (the entailment symbol might be omitted).
The above example then becomes:
grandparent_of(X, Y) <- parent_of(X, Z), parent_of(Z, Y).
parent_of(abe, homer).
parent_of(homer, bart).
A defeasible rule, instead, is a possible weak implication of the head from its body that can be proved wrong (the head os presumably true if the body holds) and uses -<
as entailment symbol.
A defeasible rule with an empty body is called presumption (the entailment symbol can not_ be omitted ti distinguish presumptions from facts ⎯ currently not supported anyway).
is_alias(X, Y) -< in_place(X, P, T), ~in_place(Y, P, T).
in_place(wayne, mansion, night). ~in_place(wayne, streets, night). ~in_place(wayne, offices, night). ~in_place(wayne, batcave, night).
in_place(wayne, offices, day). ~in_place(wayne, streets, day). ~in_place(wayne, mansion, day). ~in_place(wayne, batcave, day).
in_place(batman, streets, night). ~in_place(batman, mansion, night). ~in_place(batman, offices, night). ~in_place(batman, batcave, night).
in_place(batman, batcave, day). ~in_place(batman, streets, day). ~in_place(batman, mansion, day). ~in_place(batman, offices, day).
A defeasible (logic) program is a possibly infinite set of facts, strict rules and defeasible rules. Defeasible programs are also denoted as (𝛱, 𝛥) where 𝛱 is the subset of facts and strict rules and 𝛥 the subset of defeasible rules of the problem. A defeasible program is schematic if at least one of its rules contain variables, otherwise it is said to be ground.
The procedure for defeasible reasoning in this system assumes that programs to be ground.
program ::= rule* 'EOF'
rule ::= defeasible | strict
defeasible ::= literal '-<' literals? salience? '.'
strict ::= literal ( '<-' literals? )? salience? '.'
literals ::= literal ( ',' literal )*
literal ::= negation? atom
negation ::= '~'+
atom ::= functor ( '(' terms? ')' )?
functor ::= DOUBLE_QUOTE | SINGLE_QUOTE | IDENTIFIER
terms ::= term ( ',' term )*
term ::= boolean | number | string | IDENTIFIER | VARIABLE
boolean ::= TRUE | FALSE
number ::= REAL | INTEGER
string ::= DOUBLE_QUOTE | SINGLE_QUOTE
salience ::= '@' INTEGER
TRUE ::= [Tt] [Rr] [Uu] [Ee]
FALSE ::= [Ff] [Aa] [Ll] [Ss] [Ee]
REAL ::= '-'? [0-9]* '.' [0-9]+ ('E' '-'? [0-9]+)?
INTEGER ::= '-'? [0-9]+
DOUBLE_QUOTE ::= '"' [^"]* '"'
SINGLE_QUOTE ::= "'" [^']* "'"
IDENTIFIER ::= [a-z][a-z_A-Z0-9]*
VARIABLE ::= [_A-Z][a-z_A-Z0-9]*
COMMENT ::= '%' .* 'EOL'
program ::= rule* 'EOF'
no references
rule ::= defeasible
| strict
referenced by:
defeasible
::= literal '-<' literals? salience? '.'
referenced by:
strict ::= literal ( '<-' literals? )? salience? '.'
referenced by:
literals ::= literal ( ',' literal )*
referenced by:
literal ::= negation? atom
referenced by:
negation ::= '~'+
referenced by:
atom ::= functor ( '(' terms? ')' )?
referenced by:
functor ::= DOUBLE_QUOTE
| SINGLE_QUOTE
| IDENTIFIER
referenced by:
terms ::= term ( ',' term )*
referenced by:
term ::= boolean
| number
| string
| IDENTIFIER
| VARIABLE
referenced by:
boolean ::= TRUE
| FALSE
referenced by:
number ::= REAL
| INTEGER
referenced by:
string ::= DOUBLE_QUOTE
| SINGLE_QUOTE
referenced by:
salience ::= '@' INTEGER
referenced by:
TRUE ::= [Tt] [Rr] [Uu] [Ee]
referenced by:
FALSE ::= [Ff] [Aa] [Ll] [Ss] [Ee]
referenced by:
REAL ::= '-'? [0-9]* '.' [0-9]+ ( 'E' '-'? [0-9]+ )?
referenced by:
INTEGER ::= '-'? [0-9]+
referenced by:
DOUBLE_QUOTE
::= "'" [^']* "'"
referenced by:
SINGLE_QUOTE
::= '"' [^"]* '"'
referenced by:
IDENTIFIER
::= [a-z] [a-z_A-Z0-9]*
referenced by:
VARIABLE ::= [_A-Z] [a-z_A-Z0-9]*
referenced by:
COMMENT ::= '%' .* 'EOL'
no references
The procedure for querying Defeasible Logic programs described in Garciía and Simari requires the problems to be ground. The authors suggest to use the Lifschitz convention to turn a schematic problem into a ground one. This implementation uses a simplified forward-chaining rule-based engine implementing the Rete algorithm.
The engine builds a reticulate of
Include presumptions, negation_as_failure (standard negation) and concordance check.
The project is covered by the Simplified BSD license.