The Carneades software system provides support for constructing, evaluating and visualizing arguments, using formal representations of facts, concepts, defeasible rules and argumentation schemes. This paper illustrates how rules and ontologies can be combined in Carneades with a prototype legal application for analyzing open source software license compatibility issues in particular cases.
This paper illustrates how rules and ontologies can be used in combination in the
Carneades argumentation system [
The Carneades software system is based on a well-founded formal model of
structured argumentation with support for proof burdens and standards [
Building on this formal foundation, the Carneades software provides a
number of tools for interactively constructing, evaluating and visualizing arguments,
as well as computing positions. Arguments are constructed using formalizations
of facts, concepts, defeasible rules and argumentation schemes [
A combination of forwards and backwards reasoning is used to construct arguments: a description logic reasoner constructs the deductive closure of the concepts and facts in a forwards manner; the Carneades rules engine uses backwards reasoning to apply the defeasible inference rules in a goal-directed and stratified way to the deductive closure of the description logic theory of facts and concepts. The LKIF rule language has been extended to provide a way to declare the domain of variables using predicates defined in OWL, similar to the way variables are typed in programming languages. These domain declarations provide important control information that enables the rule engine to iterate over instances of the domains to more e ciently instantiate the rules. 1 http://carneades.github.com
In addition to the arguments constructed automatically from a knowledgebase of facts, concepts and rules, arguments can manually entered into the system by the user. These arguments can be completely ad hoc or instantiations of argumentation schemes. The Carneades system currently includes a library of about 20 of Walton’s most important argumentation schemes along with a software assistant which steps the user through the process of selecting and instantiating schemes.
As the arguments are constructed and edited, they are visualized in an
argument map [
The rest of this paper show how ontologies and rules can be used in combination in Carneades with examples from the prototype legal application for analyzing open source license compatibility issues. We start with examples from a simple OWL ontology for describing software licenses and use and derivation relationships between works of software. Next we show how to use the ontology to model the facts of a case. We then show how to model some rules of copyright law in LKIF, focusing on the issue of whether linking to a software library produces a derivative work.
Carneades uses the Web Ontology Language (OWL), a World Wide Web standard XML schema for representing and interchanging description logic knowledge bases. These knowledge bases have two parts, for concepts (TBox) and facts (ABox). The top-level concepts, called classes in OWL, for our application are CopyrightLicense, CopyrightLicenseTemplate, LegalEntity, LicenseTerm and Work. The Work class is for all works protectable by copyright. There is a SoftwareEntity subclass of Work, intended to cover all kinds of software artifacts.
The main property of software entities of interest for license compatibility issues is the isDerivedFrom property, expressing that one entity has been derived from another. The ontology includes properties for representing various ways that software can use other software, such compiledBy and linksTo.
The software ontology was used to model an example software project, roughly based on the current version of the Carneades system.
Description logic (DL) is semantically a decidable subset of first-order logic. This means that the inferences of description logic reasoners are strict : if the axioms of a DL knowledge base are true in some domain, then all of the inferences made by a (correctly implemented) DL reasoner are necessarily also true, without exception. While DL is very powerful and useful, monotonic logics are not su cient for modeling legal rules, such as the rules of copyright law, in a maintainable and verifiable way, isomorphic with the structure of legislation and regulations. Legislation is typically organized as general rules subject to exceptions. Arguments made by applying legal rules are defeasible. Their conclusions can be defeated with better counterarguments. Various legal rules may conflict with each other. Theses conflicts are resolved using legal principals about priority relationships between rules, such as the principal of lex superior, which gives rules from a higher authority, such as federal law, priority over rules from a lower authority, such as state law. These properties of legal rules are well known in AI and Law and have been studied extensively. References are omitted for lack of space.
Thus we model legal rules using a defeasible rule language which has been developed especially for this purpose, as part of the Legal Knowledge Interchange Format (LKIF), and use description logic (OWL more specifically) for more limited purposes: 1) to declare the language of unary and binary predicate symbols and 2) to make assertions about these predicates, using DL axioms, which are judged to be universally true and beyond dispute in the domain.
Here we illustrate the LKIF rule language by modeling two interpretations of the concept of a derivative work in copyright law. We begin with the general rule that the copyright owner of software may license the software using any license template he chooses. <rule id="DefaultLicenseRule"> <head> <s pred="&oss;mayUseLicenseTemplate"> <v>SE</v> may be licensed using the <v>T</v> template </s> </head> </rule> Since LKIF is an XML schema, rules are represented in XML. This particular rule has a head (conclusion) but no body (conditions). Even though the rule has no conditions, inferences made using this rule are not necessarily or universally true, but remain defeasible. We will make use of this feature to express exceptions to this general rule below.
The rule has been assigned an identifier, DefaultLicenseRule, which may be used to formulate statements about the rule. That is, rules are reified and may be reasoned about just like other objects.
The predicate symbol of the statement (proposition) in the head of the rule is specified using the pred attribute. Its value can be the name of a class or property in a OWL ontology, as in this example. The ? entity reference refers to the ontology, using its URI.
Declaring predicate symbols in ontologies makes it possible to divide up the model of a complex domain theory into modules, with a separate LKIF file for each module. OWL provides a way to import the classes and properties of other OWL files, recursively. Similarly, LKIF provides a way to import both LKIF and OWL files. OWL makes it easy to manage predicate symbols across the boundaries of modules and to make sure that symbols in di↵ erent modules refer to the same class or property when this is desired.
The XML syntax for rules in LKIF is rather verbose and not especially readable. Fortunately, it is easy to write programs for converting XML into more readable formats. Moreover, XML structure editors exist which use style sheets to enable authors to edit XML documents directly in a more readable form. Using this feature, the above rule can be displayed in the editor as follows: rule DefaultLicenseRule
head SE may be licensed using the T template We will use this more readable format for displaying LKIF rules in the remainder of this article. Next let us formulate an exception to the general rule that any license template may be used for reciprocal licenses: rule ReciprocityRule head
not: SE1 may be licensed using the T1 template domains
This reciprocity rule states that a software entity, SE1, may not be licensed using a license template, T1, if the software is derived from another software entity, SE2, licensed using a reciprocal license, L, unless L is an instance of a template license, T2, which is compatible with T1. The use of domains in this rule provides control information to make use of forward chaining in the description logic reasoner, as discussed in the introduction. Notice that the conclusion of the rule is negated and that the last condition of the rule expresses a further exception, using an unless operator.
These two rules illustrate two kinds of exceptions. In argumentation terms, arguments constructed using the ReciprocityRule rebut arguments constructed using the DefaultRule and arguments which make use of the explicit exception of the ReciprocityRule, by showing that the licenses are compatible, undercut the reciprocity argument.
Let us end this brief overview with rules modeling two conflicting views about whether or not linking creates a derivative work. According to the lawyers of the Free Software Foundation, linking does create a derivate work. Lawrence Rosen, a legal expert on open source licensing issues, takes the opposing point of view and argues that linking per se is not su cient to create derivate works. rule FSFTheoryOfLinking head
rule RosenTheoryOfLinking head body not: SE1 is derived from SE2
The last condition of each of these rules requires that the interpretation of copyright law represented by the rule is legally valid. Making this condition explicit enables us to argue about which theory of linking is correct, to compare the e↵ ects of these two theories on particular cases, and to use abduction to derive positions about which theory to prefer.
We have illustrated how ontologies and rules can be used together in the Carneades argumentation system with a prototype legal application for analyzing software licensing issues. To our knowledge, no other argumentation or rule-based system currently provides the combination of tools required for this application: 1) automatic argument construction from a knowledge base of strict and defeasible rules; 2) argument mapping; 3) argument evaluation; 4) interactive construction of arguments using argumentation schemes; 5) exploration of e↵ ects of alternative legal theories; and 6) computation of positions, using abduction. The source code of the application is freely available, as open source software.
The current user interface is a desktop application, written in Java using the Swing user interface library. Work is in progress on a web version of Carneades. The user interface of this web version is a Rich Internet Application (RIA) implemented using only World-Wide-Web Concortiums standards, in particular XML and Javascript (AJAX). Argument graphs in the web version are rendered using Scalable Vector Graphics (SVG), another W3C standard.
This work was partially funded by the European projects Qualipso (IST-FP6– 034763) and IMPACT (IST-FP7–247228). Earlier version of this paper were presented at the Jurix 2010 workshop on Modeling Legal Cases and Legal Rules and the Thirteenth International Conference on Artificial Intelligence and Law (ICAIL 2011).