We describe the design of the OLPS system, an implementation of the preferred answer set semantics for ordered logic programs. the basic algorithm we propose computes the extended answer sets of a simple program using...
详细信息
ISBN:
(纸本)3540243623
We describe the design of the OLPS system, an implementation of the preferred answer set semantics for ordered logic programs. the basic algorithm we propose computes the extended answer sets of a simple program using an intuitive 9-valued lattice, called T-9. During the computation, this lattice is employed to keep track of the status of the literals and the rules while evolving to a solution. It turns out that the basic algorithm needs little modification in order to be able to compute the preferred answer sets of an ordered logic program. We illustrate the system using an example from diagnostic reasoning and we present some preliminary benchmark results comparing OLPS with existing answer set solvers such as SMODELS and DLV.
the inverse method, due to Maslov, is a forward theorem proving method for cut-free sequent calculi that relies on the subformula property. the logic of Bunched Implications (BI), due to Pyrn and O'Hearn, is a log...
详细信息
ISBN:
(纸本)3540252363
the inverse method, due to Maslov, is a forward theorem proving method for cut-free sequent calculi that relies on the subformula property. the logic of Bunched Implications (BI), due to Pyrn and O'Hearn, is a logic which freely combines the familiar connectives of intuitionistic logic with multiplicative linear conjunction and its adjoint implication. We present the first formulation of an inverse method for propositional BI without units. We adapt the sequent calculus for BI into a forward calculus. the soundness and completeness of the calculus are proved, and a canonical form for bunches is given.
this paper focuses on improving network management by the adoption of artificial intelligence techniques. We propose a distributed multi-agent architecture for network management, where a logical reasoner acts as a ma...
详细信息
ISBN:
(纸本)0769522556
this paper focuses on improving network management by the adoption of artificial intelligence techniques. We propose a distributed multi-agent architecture for network management, where a logical reasoner acts as a managing entity capable of directing, coordinating, and triggering monitoring and management actions in the proposed architecture. the logical inference system has been devised to enable automated isolation, diagnosis, and to repair network anomalies, thus enhancing the reliability, performance, and security of the network. the measurements of network events are captured by programmable sensors deployed on the network devices and are collected by the network management entity where they are merged with general domain knowledge, with a view to identifying the root causes of anomalies, and to decide on reparative actions. the relevant results inferred by the logical reasoner and the significant events occurred on the network are stored both in a global DB and in local distributed DBs, in order to enable successive analyses of network events. In order to illustrate the advantages and potential benefits deriving from the reasoning capabilities of our management system, the results of preliminaries experiments are analyzed.
there is a trend to study extended variants of propositional logic which have explicit means to represent cardinality constraints. that is accomplished using so-called c-atoms. We show that c-atoms can be efficiently ...
详细信息
ISBN:
(纸本)3540252363
there is a trend to study extended variants of propositional logic which have explicit means to represent cardinality constraints. that is accomplished using so-called c-atoms. We show that c-atoms can be efficiently reduced to a general form of Exact Satisfiability. the general X(i)SAT problem is to find an assignment for a CNF such that exactly i literals are true in each clause for any i >= 1. We show that this problem is solvable in time O(1.4143(n)) (where n is the number of variables) regardless of i if we allow exponential space. For polynomial space, we present an algorithm solving X(i)SAT for all i strictly better than the trivial O(2(n)) bound. For i = 2, i = 3 and i = 4 we obtain upper time bounds in O(1.5157(n)), O(1.6202(n)) and O(1.6844(n)), respectively. We also present a dedicated X(2)SAT algorithm running in polynomial space and time O(1.4511(n)).
this paper theorizes the use of a hybrid expert system to support a complete audit of financial statements for an enterprise. the expert system proposed would support the audit process by using two types of artificial...
详细信息
ISBN:
(纸本)9728865198
this paper theorizes the use of a hybrid expert system to support a complete audit of financial statements for an enterprise. the expert system proposed would support the audit process by using two types of artificial intelligence technologies: case-based reasoning and fuzzy logic technologies. the case base and automatedreasoning recommendations would give the auditing firm another insight on the audit. Unlike previous audit expert systems, this system is intended to focus broadly on an enterprise's entire financial statement audit process;it combines a case based knowledge representation with fuzzy logic processing. the attempt at capturing a wide domain is necessary to support organizational decision-making. Focusing on narrow decision points within an audit process limits the users and usefulness of the system.
We present the CoRE calculus for contextual reasoning which supports reasoning directly at the assertion level, where proof steps are justified in terms of applications of definitions, lemmas, theorems, or hypotheses ...
详细信息
ISBN:
(纸本)3540280057
We present the CoRE calculus for contextual reasoning which supports reasoning directly at the assertion level, where proof steps are justified in terms of applications of definitions, lemmas, theorems, or hypotheses (collectively called "assertions") and which is an established basis to generate proof presentations in natural language. the calculus comprises a uniform notion of a logical context of subformulas as well as replacement rules available in a logical context. Replacement rules operationalize assertion level proof steps and technically are generalized resolution and paramodulation rules, which in turn should suit the implementation of automatic reasoning procedures.
this paper combines work done in the areas of Artificial Intelligence, Multimedia Systems and Coordination programming to derive a framework for Distributed Multimedia Systems based on asynchronous timed computations ...
详细信息
this paper combines work done in the areas of Artificial Intelligence, Multimedia Systems and Coordination programming to derive a framework for Distributed Multimedia Systems based on asynchronous timed computations expressed in a certain coordination formalism. More to the point, we propose the development of multimedia programming frameworks based on the declarative logicprogramming setting and in particular the framework of object-oriented timed concurrent constraint programming (OO-TCCP). the real-time extensions that have been proposed for the concurrent constraint programming framework are coupled withthe object-oriented and inheritance mechanisms that have been developed for logic programs yielding an integrated declarative environment for multimedia objects modelling, composition and synchronisation. Furthermore, we show how the framework can be implemented in the general-purpose coordination language MANIFOLD without the need for using special architectures or real-time languages. (c) 2004 Elsevier B.V. All rights reserved.
the extended answer set semantics for simple logic programs, i.e. programs with only classical negation, allows for the defeat of rules to resolve contradictions. In addition, a partial order relation on the program&#...
详细信息
ISBN:
(纸本)3540252363
the extended answer set semantics for simple logic programs, i.e. programs with only classical negation, allows for the defeat of rules to resolve contradictions. In addition, a partial order relation on the program's rules can be used to deduce a preference relation on its extended answer sets. In this paper, we propose a "quantitative" preference relation that associates a weight with each rule in a program. Intuitively, these weights define the "cost" of defeating a rule. An extended answer set is preferred if it minimizes the sum of the weights of its defeated rules. We characterize the expressiveness of the resulting semantics and show that it can capture negation as failure. Moreover the semantics can be conveniently extended to sequences of weight preferences, without increasing the expressiveness. We illustrate an application of the approach by showing how it can elegantly express subgraph isomorphic approximation problems, a concept often used in intelligence analysis to find specific regions of interest in a large graph of observed activities.
the hybrid logic H(@) is obtained by adding nominals and the satisfaction operator @ to the basic modal logic. the resulting logic gains expressive power without increasing the complexity of the satisfiability problem...
详细信息
ISBN:
(纸本)3540252363
the hybrid logic H(@) is obtained by adding nominals and the satisfaction operator @ to the basic modal logic. the resulting logic gains expressive power without increasing the complexity of the satisfiability problem, which remains within PSpace. A resolution calculus for H(@) was introduced in [5], but it did not provide strategies for ordered resolution and selection functions. Additionally, the problem of termination was left open. In this paper we address both issues. We first define proper notions of admissible orderings and selection functions and prove the refutational completeness of the obtained ordered resolution calculus using a standard "candidate model" construction [10]. Next, we refine some of the nominal-handling rules and show that the resulting calculus is sound, complete and can only generate a finite number of clauses, establishing termination. Finally, the theoretical results were tested empirically by implementing the new strategies into HyLoRes [6,18], an experimental prototype for the original calculus described in [5]. Both versions of the prover were compared and we discuss some preliminary results.
We present a program logic for verifying the heap consumption of low-level programs. the proof rules employ a uniform assertion format and have been derived from a general purpose program logic [1]. In a proof-carryin...
详细信息
ISBN:
(纸本)3540252363
We present a program logic for verifying the heap consumption of low-level programs. the proof rules employ a uniform assertion format and have been derived from a general purpose program logic [1]. In a proof-carrying code scenario, the inference of invariants is delegated to the code provider, who employs a certifying compiler that generates a certificate from program annotations and analysis. the granularity of the proof rules matches that of the linear type system presented in [6], which enables us to perform verification by replaying typing derivations in a theorem prover, given the specifications of individual methods. the resulting verification conditions are of limited complexity, and are automatically discharged. We also outline a proof system that relaxes the linearity restrictions and relates to the type system of usage aspects presented in [2].
暂无评论