Abstract: This paper provides a computational framework, based on Defeasible Logic, to capture some aspects of institutional agency. Our background is Kanger-Lindahl-Pörn account of organised interaction, which describes this interaction within a multi-modal logical setting. This work focuses in particular on the notions of counts-as link and on those of attempt and of personal and direct action to realise states of affairs. We show how standard Defeasible Logic can be extended to represent these concepts: the resulting system preserves some basic properties commonly attributed to them. In addition, the framework enjoys nice computational properties, as it turns out that the extension of any theory can be computed in time linear to the size of the theory itself.
Abstract: This paper reports on a system for automated agent negotiation, based on a formal and executable approach to capture the behavior of parties involved in a negotiation. It uses the JADE agent framework, and its major distinctive feature is the use of declarative negotiation strategies. The negotiation strategies are expressed in a declarative rules language, defeasible logic, and are applied using the implemented system DR-DEVICE. The key ideas and the overall system architecture are described, and a particular negotiation case is presented in detail.
Abstract: 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.
Abstract: In this paper we present a Gentzen system for
reasoning with contrary-to-duty obligations. The
intuition behind the system is that a
contrary-to-duty is a special kind of normative
exception. The logical machinery to formalise this
idea is taken from substructural logics and it is
based on the definition of a new non-classical
connective capturing the notion of reparational
obligation. Then the system is tested against
well-known contrary-to-duty paradoxes.
Abstract: 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 $D$ into a
meta-program $P(D)$. We show that under a condition
of decisiveness, the defeasible consequences of $D$
correspond exactly to the sceptical conclusions of
$P(D)$ under the stable model semantics. Without
decisiveness, the result holds only in one direction
(all defeasible consequences of $D$ are included in
all stable models of $P(D)$). If we wish a complete
embedding for the general case, we need to use the
Kunen semantics of $P(D)$, instead.
Abstract: This paper presents an approach to develop bidding agents that participate in multiple alternative auctions, with the goal of obtaining an item with a given probability. 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 a price, such that by sequentially bidding in a subset of the relevant auctions, the agent can obtain the item at that price with the desired probability. The approach addresses the case where the auctions are for substitutive items with different values. Experimental results show that the approach increases the payoff of their users and the welfare of the market.
Abstract: 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 be thus 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.
Abstract: In this paper we show that the Hilbert system of agency and ability presented by Dag Elgesem is incomplete with respect to the intended semantics. We argue that completeness result may be easily regained. Finally, we shortly discuss some issues related to the philosophical intuition behind his approach. This is done by examining Elgesemâs modal logic of agency and ability using semantics with different flavours.
Abstract: 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 modeling 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.
Abstract: In this paper we provide a formal analysis of the idea of normative co-ordination. We argue that this idea is based on the assumption that agents can achieve flexible co-ordination by conferring normative positions to other agents. These positions include duties, permissions, and powers. In particular, we explain the idea of declarative power, which consists in the capacity of the power-holder of creating normative positions, involving other agents, simply by âproclaimingâ such positions. In addition, we account also for the concepts of representation, namely the representativeâs capacity of acting in the name of his principal, and of mandate, which is the mandateeâs duty to act as the mandator has requested. Finally, we show how the framework can be applied to represent the contract-net protocol. Some brief remarks on future research and applications conclude this contribution.
Abstract: 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.
Abstract: This paper presents a formal and executable approach to capture the behaviour of parties involved in a negotiation. A party is modeled as a negotiating agent composed of a communication module, a control module, a reasoning module, and a knowledge base. The control module is expressed as a emphstatechart, and the reasoning module as a emphdefeasible logic program. A strategy specification therefore consists of a statechart, a set of defeasible rules, and a set of initial facts. Such a specification can be dynamically plugged into an agent shell incorporating a statechart interpreter and a defeasible logic inference engine, in order to yield an agent capable of participating in a given type of negotiations. The choice of statecharts and defeasible logic with respect to other formalisms is justified against a set of desirable criteria, and their suitability is illustrated through concrete examples of bidding and multi-lateral bargaining scenarios.
Abstract: 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.
Abstract: During his philosophical career Popper sought to characterize natural laws alternately as strictly universal and as ânaturallyâ or âphysicallyâ necessary statements. In this paper we argue that neither characterization does what Popper claimed and sketch a reconstruction of his views that avoids some of their major drawbacks.
Abstract: In this paper we provide a formal framework for developing the idea of normative co-ordination. We argue that this idea is based on the assumption that agents can achieve flexible co-ordination by conferring normative positions to other agents. These positions include duties, permissions, and powers. In particular, we introduce the idea of declarative power, which consists in the capacity of the power-holder of creating normative positions, involving other agents, simply by âproclaimingâ such positions. In addition, we account also for the concepts of representation, consisting in the representativeâs capacity of acting in the name of his principal, and of mandate, which corresponds the mandateeâs duty to act as the mandator has requested. Finally, we show how the above framework can be applied to the contract-net protocol.
Abstract: We describe a general and uniform tableau methodology for multi-modal logics arising from Gabbayâs methodology of fibring and Governatoriâs labelled tableau system \KEM.
Abstract: In this paper, following Scottâs advice, we argue that normative reasoning can be represented in a multi-setting framework; in particular in a multi-modal one, where modalities are indexed. Indexed modalities can model several aspects involved in normative reasoning. Systems are combined using Gabbayâs fibring methodology which provides complete semantics that can be used to model a labelled tableau-like proofs system.
Abstract: In this paper we describe a modal proof system arising from the combination of a tableau-like classical system, which incorporates a restricted (âanalyticalâ) version of the cut rule, with a label formalism which allows for a speicialised, logic dependant unification algorithm. The system provides a uniform proof-theoretical treatment of first-order (normal) modal logics with identity, with and without Barcan formula and/or its converse
Abstract: In this paper we follow the BOID (Belief, Obligation, Intention, Desire) architecture to describe agents and agent types in Defeasible Logic. We argue, in particular, that the introduction of obligations can provide a new reading of the concepts of intention and intentionality. Then we examine the notion of social agent (i.e., an agent where obligations prevail over intentions) and discuss some computational and philosophical issues related to it. We show that the notion of social agent either requires more complex computations or has some philosophical drawbacks.
Abstract: The \emphpossible worlds semantics is a fruitful approach used in Artificial Intelligence (AI) for both \emphmodelling as well as \emphreasoning about knowledge in agent systems via modal logics. In this work our main idea is not to model/reason about knowledge but to provide a theoretical framework for \emphknowledge assessment (KA) with the help of \emphMonatague-Scott (MS) semantics of modal logic. In KA questions \emphasked and answers \emphcollected are the central elements and knowledge notions will be defined from these (i.e., possible states of knowledge of subjects in a population with respect to a field of information).
Abstract: In agent communication languages, the inferences that can be made on the basis of a communicative action are inherently conditional, and non-monotonic. For example, a proposal only leads to a commitment, on the condition that it is accepted. And in a persuasion dialogue, assertions may later be retracted. In this paper we therefore present a defeasible logic that can be used to express a semantics for agent communication languages, and to efficiently make inferences on the basis of communicative actions. The logic is non-monotonic, allows nested rules and mental attitudes as the content of communicative actions, and has an explicit way of expressing persistence over time. Moreover, it expresses that mental attitudes are publicly attributed to agents playing roles in the dialogue. To illustrate the usefulness of the logic, we reformalize the meta-theory underlying the FIPA semantics for agent communication, focusing on inform and propose. We show how composed speech acts can be formalized, and extend the semantics with an account of persuasion.
Abstract: In this paper, we extend defeasible logic (a computationally-oriented non-monotonic logic) in order to deal with temporalised rules. In particular, we extend the logic to cope with durative facts, as well as with delays between the antecedent and the consequent of rules. We showed that the extended temporalised framework is suitable to model different types of causal relations which have been identified by the specialised literature. Finally, we also demonstrate that the computational properties of the original logic are still retained by the extended approach.
Abstract: 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.
Abstract: While some recent frameworks on cognitive agents addressed the combination of mental attitudes with deontic concepts, they commonly ignore the representation of time. We propose in this paper a variant of Temporal Modal Defeasible Logic to deal in particular with temporal intervals.
Abstract: 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.
Abstract: Trust is a vital feature for the Semantic Web: If users (humans and agents) are to use and integrate system answers, they must trust them. Thus, systems should be able to explain their actions, sources, and beliefs, and this issue is the topic of the proof layer in the design of the Semantic Web. This paper presents the design of a system for proof explanation on the Semantic Web, based on defeasible reasoning. The basis of this work is the DR-DEVICE system that is extended to handle proofs. A critical aspect is the representation of proofs in an XML language, which is achieved by a RuleML language extension.
Abstract: Business process management (BPM) has emerged as a dominant technology in current enterprise systems and business solutions. However, the technology continues to face challenges in coping with dynamic business environments where requirements and goals are constantly changing. In this paper, we present a modelling framework for business processes that is conducive to dynamic change and the need for flexibility in execution. This framework is based on the notion of process constraints. Process constraints may be specified for any aspect of the process, such as task selection, control flow, resource allocation, etc. Our focus in this paper is on a set of scheduling constraints that are specified through a temporal constraint network. We will demonstrate how this specification can lead to increased flexibility in process execution, while maintaining a desired level of control. A key feature and strength of the approach is to use the power of constraints, while still preserving the intuition and visual appeal of graphical languages for process modelling.
Abstract: We present an extension of the argumentation semantics for defeasible logic to cover the temporalisation of defeasible logic with permanent and immanent temporal literals
Abstract: We present a non-monotonic logic tailored for specifying compact autonomous agent systems. The language is a consistent instantiation of a logic based argumentation system extended with Brooksâ subsumption concept and varying degree of belief. Particularly, we present a practical implementation of the language by developing a meta-encoding method that translates logical specifications into compact general logic programs. The language allows n-ary predicate literals with the usual first-order term definitions. We show that the space complexity of the resulting general logic program is linear to the size of the original theory
Abstract: This paper provides a framework based on temporal defeasible logic to reason about deliberative rule-based cognitive agents. Compared to previous works in this area our framework has the advantage that it can reason about temporal rules. We show that for rule-based cognitive agents deliberation is more than just deriving conclusions in terms of their mental components. Our paper is an extension of \citeai05,lpar05 in the area of cognitive agent programming
Abstract: In \citejelia-02,vineetphd we showed how to combine propositional \BDI logics using Gabbayâs \emphfibring methodology. In this paper we extend the above mentioned works by providing a tableau-based decision procedure for the combined/fibred logics. We show how to uniformly construct a tableau calculus for the combined logic using Governatoriâs labelled tableau system \KEM
Abstract: Business process management (BPM) has emerged as a dominant technology in current enterprise systems and business solutions. However, business processes are always evolving in current dynamic business environments where requirements and goals are constantly changing. Whereas literature reports on the importance of domain experts in process modelling and adaptations, current solutions have not addressed this issue effectively. In this paper, we present a framework that utilizes successful work practice to support business process evolution. The framework on one hand provides the ability to use domain expert knowledge and experience to tailor individual process instances according to case specific requirements; and on the other, provides a means of using this knowledge through learning techniques to guide subsequent process changes.
Abstract: In stream authentication protocols used for large-scale data dissemination in autonomuous 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.
Abstract: The introduction of Native XML databases opens many research questions related to the data models used to represent and manipulate data, including temporal data in XML. Increasing use of XML for Valid Web pages warrants an adequate treatment of \emphnow in Native XML databases. In this study, we examined how to represent and manipulate \emphnow-relative temporal data. We identify different approaches being used to represent current time in XML temporal databases, and introduce the notion of storing variables such as ânowâ or âUCâ as strings in XML native databases. All approaches are empirically evaluated on a query that time-slices the timeline at the current time. The experimental results indicate that the proposed extension offers several advantages over other approaches: better semantics, less storage space and better response time.
Abstract: In this paper, we propose that, in order to improve customer satisfaction, we need to incorporate communication modes (e.g., speech act) in the current standards of web services specifications. We show that with the communication modes, we can estimate various affects on service consumers during their interactions with web services. With this information, a web-service management system can automatically prevent and compensate potential negative affects, and even take advantage of positive affect
Abstract: Current enterprise systems rely heavily on the modelling and enactment of business processes. One of the key criteria for a business process is to represent not just the behaviours of the participants but also how the contractual relationships among them evolve over the course of an interaction. In this paper we provide a framework in which one can define policies/ business rules using deontic assignments to represent the contractual relationships. To achieve this end we use a combination of deontic/normative concepts like \emphproclamation, \emphdirected obligation and \emphdirect action to account for a deontic theory of commitment which in turn can be used to model business processes in their organisational settings. In this way we view a business process as a \emphsocial interaction process for the purpose of doing business. Further, we show how to extend the $i^\ast$ framework, a well known organisational modelling technique, so as to accommodate our notion of deontic dependency.
Abstract: Query answering over OWLs and RDFs on the Semantic Web is, in general, a deductive process. To this end, OWL, a family of web ontology languages based on description logic, has been proposed as the language for the Semantic Web. However, reasoning even on $\mathcalALC$, a description logic weaker than OWL, faces efficiency problem. To obviate this problem, at least for $\mathcalALC$, we propose a partition approach that improves the efficiency by splitting the search space into independent Aboxes. Each partition class, i.e., an Abox, can be queried independently. The answer to a query is the simple combination of the answers from each Abox. We prove the correctness of this approach and we outline how to represent compactly the content of each independent Abox. This work can be seen as an optimization for querying a deductive semi-structured database.
Abstract: We outline meta-encoding schemas for compiling nonmonotonic logic theories into Verilog HDL (Hardware Description Language) descriptions. These descriptions can be synthesized into gate level specifications for direct fabrication of silicon chips. The method is applied for designing agent chips incorporating similar features found in the BDI (Belief, Desire, and Intention) and Brooksâ subsumption architectures.
Abstract: To develop theories to specify and reason about various aspects of multi-agent systems, many researchers have proposed the use of modal logics such as belief logics, logics of knowledge, and logics of norms. As multi-agent systems operate in dynamic environments, there is also a need to model the evolution of multi-agent systems through time. In order to introduce a temporal dimension to a belief logic, we combine it with a linear-time temporal logic using a powerful technique called fibring for combining logics. We describe a labelled modal tableaux system for a fibred belief logic (FL) which can be used to automatically verify correctness of inter-agent stream authentication protocols. With the resulting fibred belief logic and its associated modal tableaux, one is able to build theories of trust for the description of, and reasoning about, multi-agent systems operating in dynamic environments.
Abstract: In [15,19] we showed how to combine propositional multimodal logics using GabbayâÂÂs fibring methodology. In this paper we extend the above mentioned works by providing a tableau-based proof technique for the combined/ fibred logics. To achieve this end we first make a comparison between two types of tableau proof systems, (graph & path), with the help of a scenario (The FriendâÂÂs Puzzle). Having done that we show how to uniformly construct a tableau calculus for the combined logic using GovernatoriâÂÂs labelled tableau system KEM. We conclude with a discussion on KEMâÂÂs features.
Abstract: In this paper we follow the BOID (Belief, Obligation, Intention, Desire) architecture to describe agents and agent types in Defeasible Logic. We argue that the introduction of obligations can provide a new reading of the concepts of intention and intentionality. Then we examine the notion of social agent (i.e., an agent where obligations prevail over intentions) and discuss some computational and philosophical issues related to it. We show that the notion of social agent either requires more complex computations or has some philosophical drawbacks.
Abstract: In order to apply nonmonotonic logics for specifying industrial automation controllers, we define (1) a method to extend atemporal nonmonotonic logics with temporal operators and (2) a mapping of these new temporal nonmonotonic logics into a Metric Temporal Logic. This mapping provides a formal specification method for real-time temporal reasoning digital circuits for the temporal nonmonotonic logics. We present our method in the context of synthesizing custom digital hardware (called \emphagent chip) automatically from high level agent specifications.
Abstract: 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 are logic based formalism for describing both the semantics of contract and the semantics of compliance checking procedures.
Abstract: One of Semantic Web strengths is the ability to address incomplete knowledge. However, at present, it cannot handle incomplete knowledge directly. Also, it cannot handle non-monotonic reasoning. In this paper, we extend $\mathcalALC^-$ Defeasible Description Logic with existential quantifier, i.e., $\mathcalALE$ Defeasible Description Logic. Also, we modify some parts of the logic, resulting in an increasing efficiency in its reasoning.
Abstract: This paper presents a logic of knowledge, belief and certainty, which allows us to explicitly express the knowledge, belief and certainty of an agent. A computationally grounded model, called interpreted $KBC$ systems, is given for interpreting this logic. The relationships between knowledge, belief and certainty are explored. In particular, certainty entails belief; and to the agent what it is certain of appears to be the knowledge. To formalize those agents that are able to introspect their own belief and certainty, we identify a subclass of interpreted $KBC$ systems, called introspective $KBC$ systems. We provide sound and complete axiomatizations for the logics. We show that the validity problem for the interpreted $KBC$ systems is PSPACE-complete, and the same problem for introspective $KBC$ systems is co-NP complete, thus no harder than that of the propositional logic.
Abstract: We are interested in programming languages for cognitive agents with preferences. We define rule-based agent theories and inference procedures in defeasible logic, and in this setting we discuss patterns of agent behavior called agent types.
Abstract: We present a new computational model of BDI-agents, called the observation-based BDI-model. The key point of this BDI-model is to express agentsâ beliefs, desires and intentions as a set of runs (computing paths), which is exactly a system in the interpreted system model, a well-known agent model due to Halpern and his colleagues. Our BDI-model is computationally grounded in that we are able to associate the BDI-agent model with a computer program, and formulas, involving agentsâ beliefs, desires (goals) and intentions, can be understood as properties of program computations. We present a sound and complete proof system with respect to our BDI-model and explore how symbolic model checking techniques can be applied to model checking BDI-agents. In order to make our BDI-model more flexible and practically realistic, we generalize it so that agents can have multiple sources of beliefs, goals and intentions.
Abstract: We continue the study, started in [5], on the formal relationships between a domain specific contract language (BCL) and the logic of violation (FCL) proposed in [6,7]. We discuss the use of logical methods for the representation and analysis of business contracts. The proposed analysis is based on the notions of normal and canonical forms of contracts expressed in FCL. Finally we present a mapping from FCL to BCL that can be used to provide an executable model of a formal representation of a contract.
Abstract: 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.
Abstract: This paper reports on a system for automated agent negotiation. It uses the JADE agent framework, and its major distinctive feature is the use of declarative negotiation strategies. The negotiation strategies are expressed in a declarative rules language, defeasible logic and are applied using the implemented defeasible reasoning system DR-DEVICE. The choice of defeasible logic is justified. The overall system architecture is described, and a particular negotiation case is presented in detail.
Abstract: 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.
Abstract: In this paper we present an architecture to represent and reason on e-Contracts based on the DR-device architecture supplemented with a deontic defeasible logic of violation. We motivate the choice for the logic and we show how to extend RuleML to capture the notions relevant to describe e-contracts for a monitoring perspective in Defeasible Logic.
Abstract: Defeasible Logic is extended to programming languages for cognitive agents with preferences and actions for planning. We define rule-based agent theories that contain preferences and actions, together with inference procedures. We discuss patterns of agent types in this setting. Finally, we illustrate the language by an example of an agent reasoning about web-services.
Abstract: 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.
Abstract: We introduce the DR-CONTRACT architecture to represent and reason on e-Contracts. The architecture extends the DR-device architecture by a deontic defeasible logic of violation. We motivate the choice for the logic and we show how to extend \RuleML to capture the notions relevant to describe e-contracts for a monitoring perspective in Defeasible Logic.
Abstract: We introduce a multimodal logic of belief, desire and intention, called OBDI logic, where the changes and computation of agentsâ beliefs, desires, and desires are based on agentsâ observations (i.e. local states), and we propose a model checking techniques for the logic based on interpreted systems.
Abstract: This paper presents a logic of knowledge, belief and certainty, which allows us to explicitly express the knowledge, belief and certainty of an agent. A computationally grounded model, called interpreted $KBC$ systems, is given for interpreting this logic. The relationships between knowledge, belief and certainty are explored. In particular, certainty entails belief; and to the agent what it is certain of appears to be the knowledge. To formalize those agents that are able to introspect their own belief and certainty, we identify a subclass of interpreted $KBC$ systems, called introspective $KBC$ systems. We provide sound and complete axiomatizations for the logics. We show that the validity problem for the interpreted $KBC$ systems is PSPACE-complete, and the same problem for introspective $KBC$ systems is co-NP complete, thus no harder than that of the propositional logic.
Abstract: Defeasible Logic is a rule-based non-monotonic logic with tractable reasoning services. In this paper we extend Defeasible Logic with nested rules. We consider a new Defeasible Logic, called DL$^ns$, where we allow one level of nested rules. A nested rule is a rule where the antecedent or the consequent of the rule are rules themselves. The inference conditions for DL$^ns$ are based on reflection on the inference structures (rules) of the particular theory at hand. Accordingly DL$^ns$ can be considered an amalgamated reflective system with implicit reflection mechanism. Finally we outline some possible applications of the logic.
Abstract: This paper proposes a framework based on Defeasible Logic (DL) to reason about normative modifications. We show how to express them in DL and how the logic deals with conflicts between temporalised normative modifications. Some comments will be given with regard to the phenomenon of retroactivity.
Abstract: Answering a query over a group of RDF data pages is a trivial process. However, in the Semantic Web, there is a need for ontology technology. Consequently, OWL, a family of web ontology languages based on description logic, has been proposed for the Semantic Web. Answering a query over the SemanticWeb is thus not trivial, but a deductive process. However, the reasoning on OWL with data has an efficiency problem. Thus, we introduce optimization techniques for the inference algorithm. This work demonstrates the techniques for instance checking and instance retrieval problems with respect to $\mathcalALC$ description logic which covers certain parts of OWL.
Abstract: In this paper we show that the Hilbert system of agency and ability presented by Dag Elgesem is incomplete with respect to the intended semantics. We argue that completeness result may be easily regained. Finally, we shortly discuss some issues related to the philosophical intuition behind his approach. This is done by examining Elgesemâs modal logic of agency and ability using semantics with different flavours.
Abstract: We propose a computationally oriented non-monotonic multi-modal logic arising from the combination of agency, intention and obligation. 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.
Abstract: Current collaborative work environments are characterized by dynamically changing organizational structures. Although there have been several efforts to refine work distribution, especially in workflow management, most literature assumes a static database approach which captures organizational roles, groups and hierarchies and implements a dynamic roles based agent assignment protocol. However, in practice only partial information may be available for organizational models, and in turn a large number of exceptions may emerge at the time of work assignment. In this paper we present an organizational model based on a policy based normative system. The model is based on a combination of an intensional logic of agency and a flexible, but computationally feasible, non-monotonic formalism (Defeasible Logic). Although this paper focuses on the model specification, the proposed approach to modelling agent societies provides a means of reasoning with partial and unpredictable information as is typical of organizational agents in workflow systems.
Abstract: Forms are the most common way to interface users and Web-based applications. Traditional forms cannot provide the functionality needed to fulfil the requirements of complex applications. As such, there is a need for a more advanced format of forms to support Web-based application. We argued that XForms easily fit into this criterion of forms. In addition, we observed that there is a need for a tool to reason about the forms with respect to user needs and application requirements. We propose to use Description Logic \ALCQI to reason about forms generated by XForms.
Abstract: This paper investigates how we can precisely define what process designers are ought achieve for what they have promised and more importantly in a way that satisfies human users. Toward these goals, an interaction model for processes and an Affect Monitoring Framework (AMF) are proposed based on our analysis on speech act theory and cognitive-based emotion models. The Affect Monitoring Framework is to detect and predict negative affects on users and to resolve caused or predicted causes of negative affects automatically.
Abstract: We propose to extend description logic with defeasible rules, and to use the inferential mechanism of defeasible logic to reason with description logic constructors.
Abstract: This paper presents an approach for the specification and implementation of e-contracts for Web monitoring. This is done in the setting of \emphRuleML. We argue that monitoring contract execution requires also a logical account of deontic concepts and of violations. Accordingly, \emphRuleML is extended to cover these aspects.
Abstract: Defeasible logic is a non-monotonic logic with applications in rule-based domains such as law. To ease the development and improve the accuracy of expert systems based on defeasible logic, it is desirable to automatically induce a theory of the logic from a training set of precedent data. Empirical evidence suggests that minimal theories that describe the training set tend to be more faithful representations of reality. We show via transformation from the hitting set problem that this global minimization problem is intractable, belonging to the class of NP optimisation problems. Given the inherent difficulty of finding the optimal solution, we instead use heuristics and demonstrate that a best-first, greedy, branch and bound algorithm can be used to find good theories in short time. This approach displays significant improvements in both accuracy and theory size as compared to recent work in the area that post-processed the output of an Aprori association rule-mining algorithm, with comparable execution times.
Abstract: The market for intelligent legal information systems remains relatively untapped and while this might be interpreted as an indication that it is simply impossible to produce a system that satisfies the needs of the legal community, an analysis of previous attempts at producing such systems reveals a common set of deficiencies that in-part explain why there have been no overwhelming successes to date. Defeasible logic, a logic with proven successes at representing legal knowledge, seems to overcome many of these deficiencies and is a promising approach to representing legal knowledge. Unfortunately, an immediate application of technology to the challenges in this domain is an expensive and computationally intractable problem. So, in light of the 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.
Abstract: We investigate the relative complexity of two free-variable labelled modal tableaux (\KEM and Single Step Tableaux, \SST). We discuss the reasons why p-simulation is not a proper measure of the relative complexity of tableaux-like proof systems, and we propose an improved comparison scale (p-search-simulation). Finally we show that \KEM p-search-simulates \SST while \SST cannot p-search-simulate \KEM.
Abstract: Most of the theories on formalising intention interpret it as a unary modal operator in Kripkean semantics, which gives it a monotonic look. We argue that policy-based intentions \citebratman1 exhibit non-monotonic behaviour which could be captured through a non-monotonic system like defeasible logic. To this end we outline a defeasible logic of intention. The proposed technique alleviates most of the problems related to logical omniscience. The proof theory given shows how our approach helps in the maintenance of intention-consistency in agent systems like BDI.
Abstract: The market for intelligent legal information systems remains relatively untapped and while this might be interpreted as an indication that it is simply impossible to produce a system that satisfies the needs of the legal community, an analysis of previous attempts at producing such systems reveals a common set of deficiencies that in-part explain why there have been no overwhelming successes to date. Defeasible logic, a logic with proven successes at representing legal knowledge, seems to overcome many of these deficiencies and is a promising approach to representing legal knowledge. Unfortunately, an immediate application of technology to the challenges in this domain is an expensive and computationally intractable problem. So, in light of the 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.
Abstract: A non-monotonic logic of institutional agency is defined combining a computationally oriented non-monotonic system (Defeasible Logic) and intensional notions of agency.
Abstract: We develop a labelled tableaux system for the modal logic $KD45^i-j_n$ extended with epistemic notions. This logic characterises a particular type of interpreted systems used to represent and reason about states of correct and incorrect functioning behaviour of the agents in a system, and of the system as a whole. The resulting tableaux system provides a simple decision procedure for the logic. We discuss these issues and we illustrate them with the help of simple examples
Abstract: This study examines BDI logics in the context of Gabbayâs \emphfibring semantics. We show that \emphdovetailing (a special form of fibring) can be adopted as a semantic methodology to combine BDI logics. We develop a set of interaction axioms that can capture static as well as dynamic aspects of the mental states in BDI systems, using Catachâs \emphincestual schema $G^a, b, c, d$. Further we exemplify the constraints required on fibring function to capture the semantics of interactions among modalities. The advantages of having a fibred approach is discussed in the final section.
Abstract: 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
Abstract: Most of the theories on formalising intention interpret it as a unary modal operator in Kripkean semantics, which gives it a monotonic look. We argue that policy-based intentions \citebratman1 exhibit non-monotonic behaviour which could be captured through a non-monotonic system like defeasible logic. The proposed technique alleviates most of the problems related to logical omniscience.
Abstract: In this paper we present a Gentzen system for reasoning with contrary-to-duty obligations. The intuition behind the system is that a contrary-to-duty is a special kind of normative exception. The logical machinery to formalize this idea is taken from substructural logics and it is based on the definition of a new non-classical connective capturing the notion of reparational obligation. Then the system is tested against well-known contrary-to-duty paradoxes.
Abstract: This paper addresses the issue of developing agents capable of participating in several potentially simultaneous auctions of different kinds (English, First-Price, Vickrey), with the goal of finding the best price for an item on behalf of their users. Specifically, a multi-agent architecture is proposed, in which a manager agent cooperates with several expert agents, each specialised in a specific kind of auction. The expert agents communicate their knowledge to the manager agent in the form of probability functions, capturing the likelihood that a bid of a given price may win an auction. Given a set of such functions, the manager agent builds a bidding plan that it executes in concert with the expert agents.
Abstract: 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
Abstract: In this paper we analyse some logical notions relevant for representing the dynamics of institutionalised organisations. In particular, some well-known action concepts introduced in the Kanger-Lindahl-Pörn logical theory of agency are discussed and integrated. Secondly, moving from the work of Jones and Sergot, a logical characterisation is provided of the ideas of institutional links, âcounts-asâ connections, and institutional facts. This approach is then enriched by a new modal operator $\mathitproc$, intended to account for the autonomous and decentralised creation of new institutional facts and normative positions within institutions.
Abstract: 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.
Abstract: 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.
Abstract: In this paper we investigate the feasibility of Knowledge Discovery from Database (KDD) in order to facilitate the discovery of defeasible rules that represent the ratio decidendi underpinning legal decision making. Moreover we will argue in favour of Defeasible Logic as the appropriate formal system in which the extracted principles should be encoded.
Abstract: In this paper the application of defeasible logic for automated negotiation is investigated. Defeasible logic is flexible enough to be adapted to several possible negotiation strategies, has efficient implementations, and provides a formal basis for analysis (e.g.\ to explain why a negotiation was not successful). Two case studies, one small and one more comprehensive, will be described and the feasibility of approaches based on defeasible logic will be discussed.
Abstract: The relative computational complexity of two free-variable labelled modal tableaux (\KEM and Single Step Tableaux, \SST) is investigated. We discuss the reasons why p-simulation is not a proper measure to compare tableaux-like proof systems, and we propose an improved comparison scale (p-search-simulation). It shown that \KEM p-search-simulates \SST while \SST cannot p-search-simulate \KEM.
Abstract: The Belief, Desire, Intention (BDI) architecture is increasingly being used in a wide range of complex applications for agents. Many theories and models exists which support this architecture and the recent version is that of Capability being added as an additional construct. In all these models the concept of action is seen in an endogenous manner. We argue that the Result of an action performed by an agent is extremely important when dealing with composite actions and hence the need for an explicit representation of them. The Capability factor is supported using a RES construct and it is shown how the components of a composite action is supported using these two. Further, we introduce an OPP (opportunity) operator which in alliance with Result and Capability provides a better semantics for practical reasoning in BDI.
Abstract: Logics for knowledge representation suffer from over-specialization: while each logic may provide an ideal representation formalism for some problems, it is less than optimal for others. A solution to this problem is to choose from several logics and, when necessary, combine the representations. In general, such an approach results in a very difficult problem of combination. However, if we can choose the logics from a uniform framework then the problem of combining them is greatly simplified. In this paper, we develop such a framework for defeasible logics. It supports all defeasible logics that satisfy a strong negation principle. We use logic meta-programs as the basis for the framework.
Abstract: Defeasible logic is an efficient non-monotonic logic that is defined only proof-theoretically. It has potential application in some legal domains. We present here argumentation semantics for variants of defeasible logic that will be useful in these applications.
Abstract: Defeasible reasoning is a direction in nonmonotonic reasoning that is based on the use of rules that may be defeated by other rules. It is a simple, but often more efficient approach than other nonmonotonic reasoning systems. This paper presents a family of defeasible reasoning formalisms built around Nuteâs defeasible logic. We describe the motivations of these formalisms and derive some basic properties and interrelationships. We also describe a query answering system that supports these formalisms and is available on the World Wide Web.
Abstract: Defeasible logic is an efficient non-monotonic logic that is defined only proof-theoretically. It has potential application in some legal domains. We present here an argumentation semantics for defeasible logic that will be useful in these applications. Our development differs at several points from existing argumentation frameworks since there are several features of defeasible logic that have not been addressed in the literature.
Abstract: In this paper we present a labelled proof method for computing nonmonotonic consequence relations in a conditional logic setting. The method is based on the usual possible world semantics for conditional logic. The label formalism $\mathitKEM$, 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 inference rules are provided by the propositional system $\mathitKE^+$ â-a tableau-like analytic proof system devised to be used both as a refutation and a direct method of proofâ- 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.
Abstract: Negotiation plays a fundamental role in e-commerce. In this paper, the application of defeasible logic for automated negotiation is investigated. Defeasible logic is flexible enough to be adapted to several possible negotiation strategies, has efficient implementations, and provides a formal basis for analysis (e.g.\ to explain why a negotiation was not successful). Two case studies, one small and one more comprehensive, will be described and the feasibility of approaches based on defeasible logic will be discussed.
Abstract: In this paper we present a new labelled sequent calculus for modal logic. The proof method works with a more âliberalâ modal language which allows inferential steps where different formulas refer to different labels without moving to a particular world and there computing if the consequence holds. World-paths can be composed, decomposed and manipulated through unification algorithms and formulas in different worlds can be compared even if they are sub-formulas which do not depend directly on the main connective. Accordingly, such a sequent system can provide a general definition of modal consequence relation. Finally, we briefly sketch a proof of the soundness and completeness results.
Abstract: Logics for knowledge representation suffer from over-specialization: while each logic may provide an ideal representation formalism for some problems, it is less than optimal for others. A solution to this problem is to choose from several logics and, when necessary, combine the representations. In general, such an approach results in a very difficult problem of combination. However, if we can choose the logics from a uniform framework then the problem of combining them is greatly simplified. In this paper, we develop such a framework for defeasible logics. It supports all defeasible logics that satisfy a strong negation principle. We use logic meta-programs as the basis for the framework.
Abstract: In this paper we show how to extend \KEM, a tableau-like proof system for normal modal logic, in order to deal with classes of non-normal modal logics, such as monotonic and regular, in a uniform and modular way.
Abstract: In this paper we show how to extend \KEM, a tableaux-like proof system for normal modal logic, in order to deal with classes of non-normal modal logic, such as monotonic and regular, in a uniform and modular way.
Abstract: We present two models of hierarchical structured multi-agents, and we describe how to obtain a modal knowledge base from distributed sources. We then propose a computationally oriented revision procedure for modal knowledge bases. This procedure is based on a labelled tableaux calculi supplemented with a formalism to record the dependencies of the formulae. The dependencies are then used to reconstruct the minimal inconsistent sets, and the sub-formulae responsible for the inconsistencies are revised according to well-defined chains of modal functions.
Abstract: We present three approaches to revision of belief bases, which are also examined in the case in which the sentences in the base are partitioned between those which can and those which cannot be changed; the approaches are shown to be semantically equivalent. A new approach is then presented, based on the modification of individual rules, instead of deletion. The resulting base is semantically equivalent to that generated by the other approaches, in the sense that it has the same models, but the rule part alone has fewer models, that is, is subjected to a smaller change.
Abstract: The revision and transformation of knowledge is widely recognized as a key issue in knowledge representation and reasoning. Reasons for the importance of this topic are the fact that intelligent systems are gradually developed and refined, and that often the environment of an intelligent system is not static but changes over time. Traditionally belief revision has been concerned with revising first order theories. Nonmonotonic reasoning provides rigorous techniques for reasoning with incomplete information. Until recently the dynamics of nonmonotonic reasoning approaches has attracted little attention. This paper studies the dynamics of defeasible logic, a simple and efficient form of nonmonotonic reasoning based on defeasible rules and priorities. We define revision and contraction operators, propose postulates motivated by the form or the intuition of the AGM postulates for classical belief revision, and verify that the operators satisfy the postulates.
Abstract: We investigate defeasible logics using a technique which decomposes the semantics of such logics into two parts: a specification of the structure of defeasible reasoning and a semantics for the meta-language in which the specification is written. We show that Nuteâs Defeasible Logic corresponds to Kunenâs semantics, and develop a defeasible logic from the well-founded semantics of Van Gelder, Ross and Schlipf. We also obtain a new defeasible logic which extends an existing language by modifying the specification of Defeasible Logic. Thus our approach is productive in analysing, comparing and designing defeasible logics.
Abstract: We present three approaches to belief base revision, which are examined also in the case in which the sentences in the base are partitioned between those which can and those which cannot be changed; the approaches are shown to be semantically equivalent. A new approach is then presented, based on the modification of individual rules, instead of deletion. The resulting base is semantically equivalent to that generated by the other approaches, in the sense that it has the same models, but the rule part alone has less models, that is, is subjected to a smaller change.
Abstract: Regulations are a wide-spread and important part of government and business. They codify how products must be made and processes should be performed. Such regulations can be difficult to understand and apply. In an environment of growing complexity of, and change in, regulation, automated support for reasoning with regulations is becoming increasingly necessary. In this paper we report on ongoing work which aims at providing automated support for the drafting and use of regulations using logic modelling techniques. We highlight the support that can be provided by logic modelling, describe the technical foundation of our project, and report on the status of the project and the next steps.
Abstract: Recently there has been increased interest in logic programming-based default reasoning approaches which are not using negation-as-failure in their object language. Instead, default reasoning is modelled by rules and a priority relation among them. Historically the first logic in this class was Defeasible Logic. In this paper we will study its relationship to other approaches which also rely on the idea of using logic rules and priorities. In particular we will study sceptical LPwNF, courteous logic programs, and priority logic.
Abstract: In this paper we present a theorem proving methodology for a restricted but significant fragment of the conditional language made up of (boolean combinations of) conditional statements with unnested antecedents. The method is based on the possible world semantics for conditional logics. The label formalism introduced in \citecade,jelia to account for the semantics of normal modal logics is easily adapted to the semantics of conditional logics by simply indexing labels with formulas. The inference rules are provided by the propositional system $KE^+$ â- a tableau-like analytic proof system devised to be used both as a refutation and a direct method of proof â- enlarged with suitable elimination rules for the conditional connective. The theorem proving methodology we are going to present can be viewed as a first step towards developing an appropriate algorithmic framework for several conditional logics for (defeasible) conditional obligation.
Abstract: We describe a general and uniform tableau methodology for multi-modal logics arising from Gabbayâs methodology of fibring and Governatoriâs labelled tableau system \KEM.
Abstract: In this paper we describe an algorithmic framework for a multi-modal logic arising from the combination of the system of modal (epistemic) logic devised by Meyer and van der Hoek for dealing with nonmonotonic reasoning with a deontic logic of the Jones and Pörn-type. The idea behind this (somewhat eclectic) formal set-up is to have a modal framework expressive enough to model certain kinds of deontic defeasibility, in particular by taking into account preferences on norms. The appropriate inference mechanism is provided by a tableau-like modal theorem proving system which supports a proof method closely related to the semantics of modal operators. We argue that this system is particularly well-suited for mechanizing nonmonotonic forms of inference in a monotonic multi-modal setting.
Abstract: In this paper we suggest ways in which logic and law may usefully relate; and we present an analytic proof system dealing with the Jones Pörnâs deontic logic of Ideality and Subideality, which offers some suggestions about how to embed legal systems in label formalism.
Abstract: In this paper we describe a modal proof system arising from the combination of a tableau-like classical system, which incorporates a restricted (âanalyticâ) version of the cut rule, with a label formalism which allows for a specialised, logic-dependent unification algorithm. The system provides a uniform proof-theoretical treatment of first-order (normal) modal logics with and without the Barcan Formula and/or its converse.
Abstract: In this paper we present a tableau-like proof system for multi-modal logics based on DâAgostino and Mondadoriâs classical refutation system $KE$. The proposed system, that we call $KEM$, works for the logics $S5A$ and $S5P_(n)$ which have been devised by Mayer and van der Hoek for formalizing the notions of actuality and preference. We shall also show how $KEM$ works with the normal modal logics $K45, D45$, and $S5$ which are frequently used as bases for epistemic operators â knowledge, belief, and we shall briefly sketch how to combine knowledge and belief in a multi-agent setting through $KEM$ modularity.
Abstract: In this paper, we describe a Prolog implementation of a new theorem prover for (normal propositional) modal and multiâmodal logics. The theorem prover, which is called $KEM$, arises from the combination of a classical refutation system which incorporates a restricted (âanalyticaâ) version of the cut rule with a label formalism which allows for a specialised logicâdependent unification algorithm. An essential feature of $KEM$ is that it yields a rather simple and efficient proof search procedure which offers many computational advantages over the usual tableau-based proof search methods. This is due partly to the use of linear 2âpremise β rules in place of the branching β rules of the standard tableau method, and partly to the crucial role played by the analytic cut (the only branching rule) in eliminating redundancy from the search space. It turns out that $KEM$ method of proof search is not only computationally more efficient but also intuitivelly more natural than other (e.g.\ resolution-based) methods leading to simple and easy implementable procedures (two $KEM$ Theorem Prover-like systems have been implemented: an LPA interpreter on Macintosh, and a Quintus compiler on Sun-Sparcstation) which make it well suited for efficient automated proof search in modal logic.
