We propose a novel tool to provide judicial explanations from provisions encoded in LegalRuleML. The tool performs reasoning based on a translation of the provisions in Defeasible Deontic Logic.

This paper examines the significance of weak permissions in criminal trials (judicial permission). It introduces a dialogue game model to systematically address judicial permissions, considering different standards of proof and argumentation semantics.

The use of machine and deep learning techniques to predict outcomes in legal proceedings is a highly debated topic among legal scholars and policymakers. These technologies have the potential for supporting judicial decision-making, assist litigants, and analyze biases within the legal process. However, challenges remain, notably in the reluctance of judges to adopt such tools due to concerns over judicial independence, the normative correctness, accuracy, and robustness of algorithmic decisions, and the transparency of AI systems. It is claimed that methods are needed to validate AI-based judicial predication mechanisms. This paper contributes to addressing these challenges by developing a rich computational normative framework for judicial case-based reasoning grounded in Defeasible Deontic Logic. We explore legal CBR, focusing on inconsistencies and incomplete knowledge within case bases, and emphasize the importance of normative explanations to ensure transparency and justification in legal decision-making. By reconstructing CBR and deontic explanations, we provide a formal mechanism for validating AI-based judicial predictions where cases are represented using a fine-grained deontic language.

Principles of law (PoLs) offer a framework for case interpretation and ensure legal consistency, especially in areas lacking specific legislation. Courts use PoLs to establish binding precedents that guide decision-making. However, PoLs are expressed in a non-standard way in rulings, making them difficult to identify at a glance without interpretative reading. Our study tested ChatGPT, Claude, and DeepSeek in extracting PoLs, verifying their results with Regular Expressions (RegEx). While Large Language Models (LLMs) showed promise, their outputs required significant expert oversight, revealing limitations in legal research, particularly in terms of accuracy and quantity.

Autonomous vehicles (AVs) must abide by the Highway Code. An AV agent would make plans which incorporate legal reasoning. Such plans must account for contingencies wherein the agent chooses between following a current plan that would lead to a violation of the law or providing an alternative plan which would not lead to a violation - a diversion. The paper utilises Defeasible Deontic Logic representing norms and encoded in Answer Set Programming (ASP) which is integrated with planning in ASP. The paper introduces diversions to address contingencies ith respect to legal reasoning.

Abstract In the setting of Defeasible Logic, we deal with the problem of revising and contracting a non-monotonic theory while minimizing the number of rules to be removed from the theory itself. The process is based on the notions of a set of rules being necessary and sufficient in order to prove a claim. The substantial difference among classical and non-monotonic reasoning processes makes this issue significant in order to achieve the correct revision processes. We show that the process is however computationally hard, and can be solved in polynomial time on non-deterministic machines.

We study weak permissions in criminal trials, which require judicial determination due to the absence of explicit prohibitions. We thus sketch a dialogue game to address this issue, analyzing argumentative dynamics with common and private knowledge. By applying various argumentation semantics, we clarify the procedural implications for weak permissions.

What happens if the way in which we handle a genuine deontic conflict ---i.e., a deontic ambiguity--- matters regarding the application of other norms that are not directly affected by that conflict? We argue that the law requires sometimes propagating the ambiguity to other norms and sometimes confining it to some norms only. We explore this issue and model different reasoning patterns. The problem is addressed in a new variant of Defeasible Deontic Logic. The contribution of this paper is threefold: (a) we extend the treatment of ambiguity blocking and propagation to Defeasible Deontic Logic; (b) we discuss reasoning patterns in the law, especially in criminal law, where we need to deal with both ambiguity blocking and ambiguity propagation in the same legal system and logic; (c) we devise an annotated variant of Defeasible Deontic Logic where we distinguish literals that must be obtained through an ambiguity-blocking mechanism from those that are derived using an ambiguity-propagating mechanism.

The EU AI Act is the first step toward a comprehensive legal framework for AI. It introduces provisions for AI systems based on their risk levels in relation to fundamental rights. Providers of AI systems must conduct Conformity Assessments before market placement. Recent amendments added Fundamental Rights Impact Assessments for high-risk AI system users, focusing on compliance with EU and national laws, fundamental rights, and potential impacts on EU values. The paper suggests that automating business process compliance can help standardize these assessments and outlines some methodological guidelines.

We present the architecture of Houdini-2.0, a reasoning system that computes the extension of a defeasible deontic theory given as input, the process of computing the consequences of the rules expressed in the theory itself. The decision process is a sceptical, non-monotonic, and it allows us to determine which prescriptive behaviours are in force (obligations, permissions, prohibitions) along with propositional ones. The system is based on pre-existing algorithmic solutions, and it is implemented as an online platform to deploy the results of a computation in several use cases, including those that pertain legal domain.

Event logs capture the execution of business processes, such that each task is represented by an event and each individual execution is a chronological sequence of events, called an event trace. Event logs allow after-the-act and runtime analysis of deployed business processes to verify whether their execution complies with regulations and business requirements. Checking the compliance of a single sequence of events in a trace is straightforward and a number of approaches have been proposed to address this. However, some regulations or business rules span multiple process instances, requiring a cross-instance analysis. In order to check whether such requirements are maintained at all times, multiple traces need to be analysed together, which can result in a combinatorial computational complexity. In this article, we present a novel approach that efficiently checks runtime regulatory compliance based on event logs, while supporting cross-instance rule evaluation and extensible function evaluation over sequences of attribute data values. The efficiency and applicability of the proposed method is tested in a two-pronged evaluation, showing a significant improvement over existing techniques with respect to capabilities as well as computational complexity. The approach presented in this paper is subject to a patent application, with patent number WO2021/248201.

Modelling the concept of explanation is a central matter in AI systems, as it provides methods for developing eXplainable AI (XAI). When explanation applies to normative reasoning, XAI aims at promoting normative trust in the decisions of AI systems: in fact, such a trust depends on understanding whether systems predictions correspond to legally compliant scenarios. This paper extends to normative reasoning a work by Governatori et al. (2022) on the notion of stable explanations in a non-monotonic setting: when an explanation is stable, it can be used to infer the same normative conclusion independently of other facts that are found afterwards.

Abstract We introduce a modular and transparent approach for augmenting the ability of reinforcement learning agents to comply with a given norm base. The normative supervisor module functions as both an event recorder and real-time compliance checker w.r.t. an external norm base. We have implemented this module with a theorem prover for defeasible deontic logic, in a reinforcement learning agent that we task with playing a “vegan” version of the arcade game Pac-Man.

Legal documents often contain references to either other documents, or other parts (of the same document). The use of references is meant to reduce the complexity of the documents; however, they pose serious concerns for the formal (logical) representation of the norms stipulated in the document itself. We propose an approach to directly model the references in a logic language and to resolve them during the computation of the legal effects in force in a case. The approach is proved to be computationally feasible and to have an efficient algorithmic implementation.

A critical challenge in "Rules as Code" ("RaC") initiatives is enhancing legal accuracy. In this paper, we present the preliminary results of a two-week, first of its kind experiment that aims to shed light on how different legally trained people interpret and convert Australian Commonwealth legislation into machine-executable code. We find that coders collaboratively agreeing on key legal terms, or atoms, before commencing independent coding work can significantly increase the similarity of their encoded rules. Participants nonetheless made a range of divergent interpretive choices, which we argue are most likely due to: (1) the complexity of statutory interpretation, (2) encoded provisions having varying levels of granularity, and (3) the functionality of our coding language. Based on these findings, we draw an important distinction between processes for technical validation of encoded rules, which focus on ensuring rules adhere to select coding languages and conventions, and processes of legal alignment, which we conceptualise as enhancing congruence between the encoded provisions and the true meaning of the statutory text in line with the modern approach to statutory interpretation. We argue that these processes are distinct but both critically important in enhancing the accuracy of encoded rules. We conclude by emphasising the need in RaC initiatives for multi-disciplinary expertise across specific legal subject matters, statutory interpretation and technical programming.

This paper develops a new comprehensive computational framework for reasoning about private international law that encompasses the reasoning patterns modeled by previous works [3,8,9]. The framework is a multi-modal extension of [10] preserving some nice properties of the original system, including some efficient algorithms to compute the extensions of normative theories representing legal systems.

Organisations have to cope with large numbers of business rules and existing regulations governing the business in which they operate. Such rules are difficult to maintain due to their size and complexity, and it is increasingly challenging to ensure that each business process adheres to those rules. As such, automated extraction of business processes from rules has three clear advantages: (1) visualisation of all possible executions allowed by the rules, (2) automated execution and compliance by design, (3) identification of “inefficiencies” in the business rules. Existing approaches, however, only allow for the generation of partial traces based on input specifications and cannot handle many different input cases resulting in a full process. This paper presents a formal method to visualise and operationalise such sets of rules as a verifiable business process that is compliant by design, which allows us to analyse all possible execution paths. Additionally, we formally prove correctness of the business processes generated by our method. The approach is implemented in a tool and evaluated on both performance and correctness, showing that even for highly complex sets of rules the approach performs well and outperforms a well-known state-of-the-art approach. Evaluation on a real-life process shows the feasibility of the presented approach.

In this paper, we propose a methodology to verify the regulatory compliance of a composition of multiple interacting business process models. The proposed solution is based on providing a compliance certification for the components of the composition, and evaluating the compliance of the encompassing composition by aggregating the information shared by the certifications, going beyond existing techniques merely checking compliance on message flows. An advantage of adopting such methodology is that the computational details of the inner process models are not needed to verify compliance of the composition, so that companies can decide to not disclose such details while still being able to show that adopting their services would lead to compliant solutions in all possible scenarios.

Automatically assessing driving behaviour against traffic rules is a challenging task for improving the safety of Automated Vehicles (AVs). There are no AV specific traffic rules against which AV behaviour can be assessed. Moreover current traffic rules can be imprecisely expressed and are sometimes conflicting making it hard to validate AV driving behaviour. Therefore, in this paper, we propose a Defeasible Deontic Logic (DDL) based driving behaviour assessment methodology for AVs. DDL is used to effectively handle rule exceptions and resolve conflicts in rule norms. A data-driven experiment is conducted to prove the effectiveness of the proposed methodology.

Free Choice Permission is one of the challenges for the formalisation of norms. In this paper, we follow a novel approach that accepts Free Choice Permission in a restricted form. The intuition behind the guarded form is strongly aligned with the idea of defeasibility. Accordingly, we investigate how to model the guarded form in Defeasible Deontic Logic extended with disjunctive permissions.

This paper presents a framework for modelling legislative deliberation in the form of dialogues. Roughly, in legislative dialogues coalitions can dynamically change and propose rule-based theories associated with different utility functions, depending on the legislative theory the coalitions are trying to determine.

An approach for legal compliance representation and checking within a Linked Open Data framework is presented.It is based on modeling deontic norms in terms of ontology and ontology property restrictions.It is also shown how the approach can handle norm defeasibility.Such methodology is implemented by decidable fragments of OWL 2, while legal reasoning is implemented by available decidable reasoners.

We identify some legal reasoning patterns concerning deontic closure and conflicts in defeasible deontic logics.First, whether the logic allows the derivation of permissions from conflicting norms.Second, whether the logic treats norms as closed under logical implication.We suggest appropriate approaches for legal settings.

This paper extends previous work by presenting a framework for modelling legislative deliberation in the form of dialogues with incomplete information.Roughly, in such legislative dialogues coalitions are initially equipped with different theories which constitute their private knowledge.Under this assumption they can dynamically change and propose new legislation associated with different utility functions.

We introduce a computational model based on Deontic Defeasible Logic to handle the issue of Pragmatic Oddity. The key idea is that a conjunctive obligation is allowed only when each individual obligation is independent of the violation of the other obligations. The solution makes essential use of the constructive proof theory of the logic.

Representation and reasoning over legal rules is an important application domain and a number of related approaches have been developed. In this work, we investigate legal reasoning in practice based on three use cases of increasing complexity. We consider three representation and reasoning approaches: (a) Answer Set Programming, (b) Argumentation and (c) Defeasible Logic. Representation and reasoning approaches are evaluated with respect to semantics, expressiveness, efficiency, complexity and support.

In the last fifteen years, Semantic Web technologies have been successfully applied to the legal domain. By composing all those techniques and theoretical methods, we propose an integrated framework for modelling legal documents and legal knowledge to support legal reasoning, in particular checking compliance. This paper presents a proof-of-concept applied to the GDPR domain, with the aim to detect infringements of privacy compulsory norms or to prevent possible violations using BPMN and Regorous engine.

We study how the non-classical n-ary operator ⊗, originally intended to capture the concept of reparative obligation, can be used in the context of social choice theory to model preferences. A novel possible-world model-theoretic semantics, called sequence semantics, was proposed for the operator. In this paper, we propose a sound and complete axiomatisation of a minimal modal logic for the operator, and we extend it with axioms suitable to model social choice consistency principles such as extension consistency and contraction consistency. We provide completeness results for such extensions.

Organisations typically have to cope with large numbers of business rules and existing regulations governing the business in which they operate. Due to the size and complexity of those rules, maintenance is difficult and it is increasingly complicated to ensure that each business process adheres to those rules. As such, automated extraction of business processes from rules has a number of clear advantages: (1) visualisation of all possible executions allowed by the rules, (2) automated execution and compliance by design, (3) identification of "inefficiencies" in the business rules. Existing approaches, however, only allow to generate partial traces based on input specifications and cannot handle many different input cases resulting in a full process. This paper presents a formal method to visualise and operationalise such sets of rules as a verifiable business process that is compliant by design and allows us to analyse all possible execution paths. In addition, it maintains information of all distinct input cases, to preserve dependencies between consecutive exclusive paths.

In this paper, we propose a proof of concept for the ontological representation of normative requirements as Linked Data on the Web. Starting from the LegalRuleML ontology, we present an extension of this ontology to model normative requirements and rules. Furthermore, we define an operational formalization of the deontic reasoning over these concepts on top of the Semantic Web languages.

This paper presents a belief revision operator for legal systems that considers time intervals. This model relates techniques about belief revision formalisms and time intervals with temporalised rules for legal systems. Our goal is to formalise a temporalised belief base and corresponding timed derivation, together with a proper revision operator. This operator may remove rules when needed or adapt intervals of time when contradictory norms are added in the system.

Abstract Defeasible logics provide several linguistic features to support the expression of defeasible knowledge. There is also a wide variety of such logics, expressing different intuitions about defeasible reasoning. However, the logics can only combine in trivial ways. This limits their usefulness in contexts where different intuitions are at play in different aspects of a problem. In particular, in some legal settings, different actors have different burdens of proof, which might be expressed as reasoning in different defeasible logics. In this paper, we introduce annotated defeasible logic as a flexible formalism permitting multiple forms of defeasibility, and establish some properties of the formalism.

Dung-like argumentation framework ASPIC+and Defeasible Logic (DL) arebothwell-studiedrule-basedformalismsfordefeasiblereasoning.Wecomparethe two frameworks and establish a linkage between an instantiation of ASPIC+and a DL variant, which leads to a better understanding and cross-fertilization – in particular our work sheds light on features such as ambiguity propagating/blocking, team defeat and strict rules for argumentation, while emphasizing the argumentation-theoretic features of DL.

In computational models of argumentation, argument justification has attracted more attention than statement justification, and significant sensitivity losses are identifiable when dealing with the justification of statements by otherwise appealing formalisms. This paper reappraises statement justification as a formalism-independent component in argument-based reasoning. We introduce a novel general model of argument-based reasoning based on multiple stages of labellings, the last one being devoted to statement justification, identify two alternative paths from argument acceptance to statement justification, and compare their expressiveness. We then show that this model encompasses several prominent literature proposals as special cases, thereby enabling a systematic comparison of existing approaches to statement justification, evidencing their merits and limits. Finally we illustrate our model by specifying a generic ignorance-aware statement justification and showing how it can be seamlessly integrated into different formalisms.

In this paper we extend a formal framework presented in [6] to model reasoning across legal systems. In particular, we propose a logical system that encompasses the various interpretative interactions occurring between legal systems in the context of private international law. This is done by introducing meta-rules to reason with interpretive canons.

Abstract The paper proposes a fresh look at the concept of goal and advances that motivational attitudes like desire, goal and intention are just facets of the broader notion of (acceptable) outcome. We propose to encode the preferences of an agent as sequences of “alternative acceptable outcomes”. We then study how the agent's beliefs and norms can be used to filter the mental attitudes out of the sequences of alternative acceptable outcomes. Finally, we formalise such intuitions in a novel Modal Defeasible Logic and we prove that the resulting formalisation is computationally feasible.

In the past few years several business process compliance frameworks based on temporal logic have been proposed. In this paper we investigate whether the use of temporal logic is suitable for the task at hand: namely to check whether the specifications of a business process are compatible with the formalisation of the norms regulating the business process. We provide an example inspired by real life norms where the use of linear temporal logic produces a result that is not compatible with the legal understanding of the norms in the example.

In this paper we discuss some reasons why temporal logic might not be suitable to model real life norms. To show this, we present a novel deontic logic contrary-to-duty/derived permission paradox based on the interaction of obligations, permissions and contrary-to-duty obligations. The paradox is inspired by real life norms.

We propose an architecture for a rule-based online management systems (RuleOMS). Typically, many domain areas face the problem that stakeholders maintain databases of their business core information and they have to take decisions or create reports according to guidelines, policies or regulations. To address this issue we propose the integration of databases, in particular relational databases, with a logic reasoner and rule engine. We argue that defeasible logic is an appropriate formalism to model rules, in particular when the rules are meant to model regulations. The resulting RuleOMS provides an efficient and flexible solution to the problem at hand using defeasible inference. A case study of an online child care management system is used to illustrate the proposed architecture.

This paper offers a new logical machinery for reasoning about interpretive canons. We identify some options for modelling reasoning about interpretations and show that interpretative argumentation has a distinctive structure where the claim that a legal text ought or may be interpreted in a certain way can be supported or attacked by arguments, whose conflicts may have to be assessed according to further arguments.

It this paper we address the issue of what it means to comply with or violate norms, and we propose a computationally oriented approach to reason about such notions.

Permissions are special case of deontic effects and play important role compliance. Essentially they are used to determine the obligations or prohibitions to contrary. A formal language e.g., temporal logic, event-calculus et., not able to represent permissions is doomed to be unable to represent most of the real-life legal norms. In this paper we address this issue and extend deontic-event-calculus (DEC) with new predicates for modelling permissions enabling it to elegantly capture the intuition of real-life cases of permissions.

Verifying whether a business process is compliant with a regulatory framework is a difficult task. In the present paper we prove the hardness of the business process regulatory compliance problem by taking into account a sub-problem of the general problem. This limited problem allows to verify only the compliance of structured processes with respect to a regulatory framework composed of a set of conditional obligations including a deadline. Experimental evidence from existing studies shows that compliance is a difficult task. In this paper, despite considering a sub-problem of the general problem, we provide some theoretical evidence of the difficulty of the task. In particular we show that the source of the complexity lies in the core language of verifying conditional obligations with a deadline. We prove that for this simplified case verifying partial compliance belongs to the class of NP-complete problems, and verifying full compliance belongs to the class of coNP-complete problems. Thus by proving the difficulty of a simplified compliance problem we prove that the general problem of verifying business process regulatory compliance is hard.

We study the complexity of the Strategic Argumentation Problem for 2-player dialogue games where a player should decide what move (set of rules) to play at each turn in order to prove (disprove) a given thesis. We show that this is an NP-complete problem.

In strategic argumentation players exchange arguments to prove or reject a claim. This paper discusses and reports on research about two basic issues regarding the game-theoretic understanding of strategic argumentation games in the law: whether such games can be reasonably modelled as zero-sum games and as games with complete information.

Michael Fisher, Leendert van der Torre, Mehdi Dastani, Guido Governatori; Preface to the Special Issue on Computational Logic in Multi-Agent Systems (CLIMA

In this paper we present the motivation, use cases, design principles, abstract syntax, and initial core of LegalRuleML. The LegalRuleML-core is sufficiently rich for expressing legal sources, time, defeasibility, and deontic operators. An example is provided. LegalRuleMLis compared to related work.

This paper systematically investigates how to model legal contraction in an expressive variant of Defeasible Deontic Logic. We argue that legal contraction is an umbrella concept that includes operations which are conceptually and technically different: removing rules, adding exceptions, and modifying rule priorities. The peculiarities of deleting legal conclusions show that an extension of those operations is sometimes needed, which works on the indirect conclusions from which the target effect of the contraction is obtained. The proposed techniques are discussed in the context of a new version for the logic of AGM postulates of contraction.

We report on the development of Regorous, a business process compliance checker, based on the compliance-by-design methodology proposed by Governatori and Sadiq [8]. For a screencast see http://www.youtube.com/watch?v=gFmDQJNai_4r

The Web of Data is assisting to a growth of interest with respect to the open challenge of representing and reasoning in an automated way over licenses and copyright. In this paper, we deal with the problem of checking the composing together a set of licensing terms associated to a single query result on the Web of Data to create a so called composite license. More precisely, we analyze two composition heuristics, AND-composition and OR-composition, showing how they can be used to combine the deontic components specified by the licenses, i.e., permissions, obligations, and prohibitions, and which are the most suitable combinations depending on the starting licenses. Such heuristics are evaluated using the SPINdle logic reasoner.

In the domain of Linked Open Data a need is emerging for developing automated frameworks able to generate the licensing terms associated to data coming from heterogeneous distributed sources. This paper proposes and evaluates a deontic logic semantics which allows us to define the deontic components of the licenses, i.e., permissions, obligations, and prohibitions, and generate a composite license compliant with the licensing items of the composed different licenses. Some heuristics are proposed to support the data publisher in choosing the licenses composition strategy which better suits her needs w.r.t. the data she is publishing. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

This article shows how a non-monotonic rule based system (defeasible logic) can be integrated with numerical computation engines, and how this can be applied to solve the Vehicle Routing Problem. To this end, we have simulated a physical system from which we can obtain numerical information. The physical system perceives information from its environment and generates predicates that can be reasoned by a defeasible logic engine. The conclusions/decisions derived will then be realized by the physical system as it takes actions based on the conclusion derived. Here we consider a scenario where a ‘flock’ of Unmanned Autonomous Vehicles (UAVs) have to navigate within an urban canyon environment. The UAVs are self-autonomous without centralized control. The goal of the UAVs is to navigate to their desired destinations without colliding with each other. In case of possible collision, the UAVs concerned will communicate with each other and use their background knowledge or travel guidelines to resolve the conflicts.

We propose a framework for reconstructing the arguments supporting the restrictive interpretations of legal provisions. The idea is that the interpretation of legal concepts may require to change the counts-as rules defining them. Some connections with revision theory techniques are considered.

We study the formal relationships between the inferential aspects of Carneades (a general argumentation framework) and Defeasible Logic. The outcome of the investigation is that the current proof standards proposed in the Carneades framework correspond to some variants of Defeasible Logic.

Legal reasoning involves multiple temporal dimensions but the existing state of the art of legal representation languages does not allow us to easily combine expressiveness, performance and legal reasoning requirements. Moreover we also aim at the combination of legal temporal reasoning with the defeasible logic approach, maintaining a computable complexity. The contribution of this work is to extend LKIF-rules with temporal dimensions and defeasible tools, extending our previous work [17].

In this paper we propose an extension of Defeasible Logic to represent different concepts of defeasible permission. Special attention is paid in particular to permissive norms that work as exceptions to opposite obligations.

Defeasible logic is a non-monotonic formalism that deals with incomplete and conflicting information, whereas modal logic deals with the concepts of necessity and possibility. These types of logics play a significant role in the emerging Semantic Web, which enriches the available Web information with meaning, leading to better cooperation between end-users and applications. Defeasible and modal logics, in general, and, particularly, deontic logic provide means for modeling agent communities, where each agent is characterized by its cognitive profile and normative system, as well as policies, which define privacy requirements, access permissions, and individual rights. Toward this direction, this article discusses the extension of DR-DEVICE, a Semantic Web-aware defeasible reasoner, with a mechanism for expressing modal logic operators, while testing the implementation via deontic logic operators, concerned with obligations, permissions, and related concepts. The motivation behind this work is to develop a practical defeasible reasoner for the Semantic Web that takes advantage of the expressive power offered by modal logics, accompanied by the flexibility to define diverse agent behaviours. A further incentive is to study the various motivational notions of deontic logic and discuss the cognitive state of agents, as well as the interactions among them.

This paper introduces a new approach to designing smart control chips that enables automatic synthesis of real-time control systems from agent specifications. An agent specification is compiled into a hardware description format, such as RTL-VHDL (Register Transfer Level-VLSI Hardware Description Language) or RTL Verilog, which is synthesized using computer-assisted tools to develop ASIC masks or FPGA configurations. A rule-based specification language called Layered Argumentation System (LAS) is defined and a sound and complete mapping to Verilog is developed. LAS combines fuzzy reasoning and nonmonotonic reasoning. This enables chip designers to capture commonsense knowledge and concepts having varying degrees of confidence collaboratively and incrementally.

We shall argue that burdens of proof are relevant also to monological reasoning, i.e., for deriving the conclusions of a knowledge-base allowing for conflicting arguments. Reasoning with burdens of proof can provide a useful extension of current argument-based non-monotonic logics, at least a different perspective on them. Firstly we shall provide an objective characterisation of burdens of proof, assuming that burdens concerns rule antecedents (literals in the body of rules), rather than agents. Secondly, we shall analyse the conditions for a burden to be satisfied, by considering credulous or skeptical derivability of the concerned antecedent or of its complement. Finally, we shall develop a method for developing inferences out of a knowledge base merging rules and proof burdens in the framework of defeasible logic.

Typically legal reasoning involves multiple temporal dimensions. The contribution of this work is to extend LKIF-rules (LKIF is a proposed mark-up language designed for legal documents and legal knowledge in ESTRELLA Project [3]) with temporal dimensions. We propose an XML-schema to model the various aspects of the temporal dimensions in legal domain, and we discuss the design choices. We illustrate the use of the temporal dimensions in rules with the help of real life examples.

The eight papers in this special section focus on the state-of-the-art approaches, solutions, and applications in the area of rule representation, reasoning, and interchange in the context of distributed, (partially) open, heterogeneous environments, such as the semantic Web, intelligent multiagent systems, event-driven architectures. and service-oriented computing.

Defeasible reasoning is a computationally simple nonmonotonic reasoning approach that has attracted significant theoretical and practical attention. It comprises a family of logics that capture different intuitions, among them ambiguity propagation versus ambiguity blocking, and the adoption or rejection of team defeat. This article provides a compact presentation of the defeasible logic variants, and derives an inclusion theorem which shows that different notions of provability in defeasible logic form a chain of levels of proof.

Policy languages (such as privacy and rights) have had little impact on the wider community. Now that Social Networks have taken off, the need to revisit Policy languages and realign them towards Social Networks requirements has become more apparent. One such language is explored as to its applicability to the Social Networks masses. We also argue that policy languages alone are not sufficient and thus they should be paired with reasoning mechanisms to provide precise and unambiguous execution models of the policies. To this end we propose a computationally oriented model to represent, reason with and execute policies for Social Networks.

This paper provides a novel mechanism to check whether business processes are compliant with business rules regulating them. The key point is that compliance is a relationship between two sets of specifications: the specifications for executing a business process and the specifications regulating it.

We present a model of past interaction trust model based on compliance of expected behaviours.

This paper proposes some variants of Temporal Defeasible Logic (TDL) to reason about normative modifications. These variants make it possible to differentiate cases in which, for example, modifications at some time change legal rules but their conclusions persist afterwards from cases where also their conclusions are blocked.

Argumentation is modelled as a game where the payoffs are measured in terms of the probability that the claimed conclusion is, or is not, defeasibly provable, given a history of arguments that have actually been exchanged, and given the probability of the factual premises. The probability of a conclusion is calculated using a standard variant of Defeasible Logic, in combination with standard probability calculus. It is a new element of the present approach that the exchange of arguments is analysed with game theoretical tools, yielding a prescriptive and to some extent even predictive account of the actual course of play. A brief comparison with existing argument-based dialogue approaches confirms that such a prescriptive account of the actual argumentation has been almost lacking in the approaches proposed so far.

In stream authentication protocols used for large-scale data dissemination in autonomous systems, authentication is based on the timing of the publication of keys, and depends on trust of the receiver in the sender and belief on whether an intruder can have prior knowledge of a key before it is published by a protocol. Many existing logics and approaches have successfully been applied to specify other types of authentication protocols, but most of them are not appropriate for analysing stream authentication protocols. We therefore consider a fibred modal logic that combines a belief logic with a linear-time temporal logic which can be used to analyse time-varying aspects of certain problems. With this logical system one is able to build theories of trust for analysing stream authentication protocols, which can deal with not only agent beliefs but also the timing properties of an autonomous agent-based system

It is a typical scenario that many organisations have their business processes specified independently of their business contracts. This is because of the lack of guidelines and tools that facilitate derivation of processes from contracts but also because of the traditional mindset of treating contracts separately from business processes. This paper provides a solution to one specific problem that arises from this situation, namely the lack of mechanisms to check whether business processes are compliant with business contracts. The central part of the paper is logic based formalism for describing both the semantics of contract and the semantics of compliance checking procedures

This paper presents a formal system for reasoning about violations of obligations in contracts. The system is based on the formalism for the representation of contrary-to-duty obligations. These are the obligations that take place when other obligations are violated as typically applied to penalties in contracts. The paper shows how this formalism can be mapped onto the key policy concepts of a contract specification language, called Business Contract Language (BCL), previously developed to express contract conditions for run time contract monitoring. The aim of this mapping is to establish a formal underpinning for this key subset of BCL.

Defeasible reasoning is a simple but efficient approach to nonmonotonic reasoning that has recently attracted considerable interest and that has found various applications. Defeasible logic and its variants are an important family of defeasible reasoning methods. So far no relationship has been established between defeasible logic and mainstream nonmonotonic reasoning approaches. In this paper we establish close links to known semantics of logic programs. In particular, we give a translation of a defeasible theory , instead.

This paper presents a formal system for reasoning about violations of obligations in contracts. The system is based on the formalism for the representation of contrary-to-duty obligations. These are the obligations that take place when other obligations are violated as typically applied to penalties in contracts. The paper shows how this formalism can be mapped onto the key policy concepts of a contract specification language. This language, called Business Contract Language (BCL) was previously developed to express contract conditions of relevance for run time contract monitoring. The aim of this mapping is to establish a formal underpinning for this key subset of BCL.

We propose a computationally oriented non-monotonic multi-modal logic arising from the combination of temporalised agency and temporalised normative positions. We argue about the defeasible nature of these notions and then we show how to represent and reason with them in the setting of Defeasible Logic.

This paper presents an approach for the specification and implementation of translating contracts from a human-oriented form into an executable representation for monitoring. This will be done in the setting of RuleML. The task of monitoring contract execution and performance requires a logical account of deontic and defeasible aspects of legal language; currently such aspects are not covered by RuleML; accordingly we show how to extend it to cover such notions. From its logical form, the contract will thus be transformed into a machine readable rule notation and eventually implemented as executable semantics via any mark-up languages depending on the client's preference, for contract monitoring purposes.

Defeasible reasoning is a simple but efficient rule-based approach to nonmonotonic reasoning. It has powerful implementations and shows promise to be applied in the areas of legal reasoning and the modelling of business rules. This paper establishes significant links between defeasible reasoning and argumentation. In particular, Dung-like argumentation semantics is provided for two key defeasible logics, of which one is ambiguity propagating and the other ambiguity blocking. There are several reasons for the significance of this work: (a) establishing links between formal systems leads to a better understanding and cross-fertilization, in particular our work sheds light on the argumentation-theoretic features of defeasible logic; (b) we provide the first ambiguity blocking Dung-like argumentation system; (c) defeasible reasoning may provide an efficient implementation platform for systems of argumentation; and (d) argumentation-based semantics support a deeper understanding of defeasible reasoning, especially in the context of the intended applications.

Defeasible Logic is a promising representation for legal knowledge that appears to overcome many of the deficiencies of previous approaches to representing legal knowledge. Unfortunately, an immediate application of technology to the challenges of generating theories in the legal domain is an expensive and computationally intractable problem. So, in light of the potential benefits, we seek to find a practical algorithm that uses heuristics to discover an approximate solution. As an outcome of this work, we have developed an algorithm that integrates defeasible logic into a decision support system by automatically deriving its knowledge from databases of precedents. Experiments with the new algorithm are very promising -- delivering results comparable to and exceeding other approaches.

This paper presents an approach to develop bidding agents that participate in multiple alternative auctions, with the goal of obtaining an item at the lowest price. The approach consists of a prediction method and a planning algorithm. The prediction method exploits the history of past auctions in order to build probability functions capturing the belief that a bid of a given price may win a given auction. The planning algorithm computes the lowest price, such that by sequentially bidding in a subset of the relevant auctions, the agent can obtain the item at that price with an acceptable probability. The approach addresses the case where the auctions are for substitutable items with different values. Experimental results are reported, showing that the approach increases the payoff of their users and the welfare of the market.

In this paper we present a labelled proof method for computing nonmonotonic consequence relations in a conditional logic setting. The method exploits the strong connection between these deductive relations and conditional logics, and it is based on the usual possible world semantics devised for the latter. The label formalism KEM, introduced to account for the semantics of normal modal logics, is easily adapted to the semantics of conditional logic by simply indexing labels with formulas. The basic inference rules are provided by the propositional system KE+—a tableau‐like analytic proof system devised to be used both as a refutation method and a direct method of proof—that is the classical core of KEM which is thus enlarged with suitable elimination rules for the conditional connective. The resulting algorithmic framework is able to compute cumulative consequence relations in so far as they can be expressed as conditional implications.

We propose a formal and executable framework for expressing protocols and strategies for automated (legal) negotiation. In this framework a party involved in a negotiation is represented through a software agent composed of four modules: (i) a communication module which manages the interaction with the other agents; (ii) a control module; (iii) a reasoning module specified as a defeasible theory; and (iv) a knowledge base which bridges the control and the reasoning modules, while keeping track of past decisions and interactions. The choice of defeasible logic is justified against a set of desirable criteria for negotiation automation languages. Moreover, the suitability of the framework is illustrated through two case studies.

The importance of transformations and normal forms in logic programming, and generally in computer science, is well documented. This paper investigates transformations and normal forms in the context of Defeasible Logic, a simple but efficient formalism for nonmonotonic reasoning based on rules and priorities. The transformations described in this paper have two main benefits: on one hand they can be used as a theoretical tool that leads to a deeper understanding of the formalism, and on the other hand they have been used in the development of an efficient implementation of defeasible logic.