this paper is a sequel to Leitgeb(7). We show that certain networks called 'inhibition nets' may be regarded as mechanisms drawing nonmonotonic inferences if only an interpretation of net states as states of b...
详细信息
this paper is a sequel to Leitgeb(7). We show that certain networks called 'inhibition nets' may be regarded as mechanisms drawing nonmonotonic inferences if only an interpretation of net states as states of belief is introduced. We prove that each of the cumulative logical systems studied by Kraus et al.(6) are sound and complete with respect to certain classes of such interpreted inhibition nets. thus, there is an adequate cognitive network semantics for the systems C, CL, P, CM, and M of (nonmonotonic) logic.
Disjunctive logicprogramming (DLP) with stable model semantics is a powerful nonmonotonic formalism for knowledge representation and reasoning. reasoning with DLP is harder than with normal (boolean OR-free) logic pr...
详细信息
Disjunctive logicprogramming (DLP) with stable model semantics is a powerful nonmonotonic formalism for knowledge representation and reasoning. reasoning with DLP is harder than with normal (boolean OR-free) logic programs, because stable model checking-deciding whether a given model is a stable model of a propositional DLP program-is co-NP-complete, while it is polynomial for normal logic programs. this paper proposes a new transformation Gamma(M) (P), which reduces stable model checking to UNSAT-i.e., to deciding whether a given CNF formula is unsatisfiable. the stability of a model M of a program P thus can be verified by calling a Satisfiability Checker on the CNF formula Gamma(M) (P). the transformation is parsimonious (i.e., no new symbol is added), and efficiently computable, as it runs in logarithmic space (and therefore in polynomial time). Moreover, the size of the generated CNF formula never exceeds the size of the input (and is usually much smaller). We complement this transformation with modular evaluation results, which allow for efficient handling of large real-world reasoning problems. the proposed approach to stable model checking has been implemented in DLV-a state-of-the-art implementation of DLP. A number of experiments and benchmarks have been run using SATZ as Satisfiability checker. the results of the experiments are very positive and confirm the usefulness of our techniques. (C) 2003 Elsevier B.V. All rights reserved.
Prioritized logic programs (PLPs) have a mechanism of representing priority knowledge in logic programs. the declarative semantics of a PLP is given as preferred answer sets which are used for representing nonmonotoni...
详细信息
ISBN:
(数字)9783540398134
ISBN:
(纸本)3540201017
Prioritized logic programs (PLPs) have a mechanism of representing priority knowledge in logic programs. the declarative semantics of a PLP is given as preferred answer sets which are used for representing nonmonotonicreasoning as well as preference abduction. From the computational viewpoint, however, its implementation issues have little been studied and no sound procedure is known for computing preferred answer sets of PLPs. In this paper, we present a sound and complete procedure to compute all preferred answer sets of a PLP in answer set programming. the procedure is based on a program transformation from a PLP to a logic program and is realized on top of any procedure for answer set programming. the proposed technique also extends PLPs to handle dynamic preference and we address its application to legal reasoning.
Default logic is one of the best known and most studied of the approaches to nonmonotonicreasoning. Subsequently, several variants of default logic have been proposed to give systems with properties differing from th...
详细信息
ISBN:
(纸本)3540404945
Default logic is one of the best known and most studied of the approaches to nonmonotonicreasoning. Subsequently, several variants of default logic have been proposed to give systems with properties differing from the original. In this paper we show that these variants are in a sense superfluous, in that for any of these variants of default logic, we can exactly mimic the behaviour of a variant in standard default logic. We accomplish this by translating a default theory under a variant interpretation into a second default theory wherein the variant interpretation is respected.
this paper presents an Arabic Morphological Analyzer and its implementation in clp(FD), a constraint logicprogramming language. the Morphological Analyzer (MA) represents a component of an architecture which can proc...
详细信息
ISBN:
(纸本)3540408037
this paper presents an Arabic Morphological Analyzer and its implementation in clp(FD), a constraint logicprogramming language. the Morphological Analyzer (MA) represents a component of an architecture which can process unrestricted text from a source such as Internet. the morphological analyzer uses a constraint-based model to represent the morphological rules for verbs and nouns, a matching algorithm to isolate the affixes and the root of a given word-form, and a linguistic knowledge base consisting in lists of markers. the morphological rules fall into two categories: the regular morphological rules of the Arabic grammar and the exception rules that represent the language exceptions. clp(FD) is particularly suitable for the implementation of our system thanks to its double reasoning: symbolic reasoning expresses the logic properties of the problem and facilitates the implementation of a the linguistic knowledge base, and heuristics, while constraint satisfaction reasoning on finite domains uses constraint propagation to keep the search space manageable.
Many data integration systems provide transparent access to heterogeneous data sources through a unified view of all data in terms of a global schema, which may be equipped with integrity constraints on the data. Sinc...
详细信息
ISBN:
(纸本)3540206426
Many data integration systems provide transparent access to heterogeneous data sources through a unified view of all data in terms of a global schema, which may be equipped with integrity constraints on the data. Since these constraints might be violated by the data retrieved from the sources, methods for handling such a situation are needed. To this end, recent approaches model query answering in data integration systems in terms of nonmonotoniclogic programs. However, while the theoretical aspects have been deeply analyzed, there are no real implementations of this approach yet. A problem is that the reasoning tasks modeling query answering are computationally expensive in general, and that a direct evaluation on deductive database systems is infeasible for large data sets. In this paper, we investigate techniques which make user query answering by logic programs effective. We develop pruning and localization methods for the data which need to be processed in a deductive system, and a technique for the recombination of the results on a relational database engine. Experiments indicate the viability of our methods and encourage further research of this approach.
this paper investigates the relationship between automata-and tableau-based inference procedures for Description logics. To be more precise, we develop an abstract notion of what a tableau-based algorithm is, and then...
详细信息
ISBN:
(数字)9783540398134
ISBN:
(纸本)3540201017
this paper investigates the relationship between automata-and tableau-based inference procedures for Description logics. To be more precise, we develop an abstract notion of what a tableau-based algorithm is, and then show, on this abstract level, how tableau-based algorithms can be converted into automata-based algorithms. In particular, this allows us to characterize a large class of tableau-based algorithms that imply an ExpTime upper-bound for reasoning in the description logics for which such an algorithm exists.
First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic firs...
详细信息
ISBN:
(数字)9783540398134
ISBN:
(纸本)3540201017
First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments including the guarded fragment with equality. In this paper, we specialise the monodic resolution method to the guarded monodic fragment with equality and first-order temporal logic over expanding domains. We introduce novel resolution calculi that can be applied to formulae in the normal form associated withthe clausal resolution method, and state correctness and completeness results.
In this paper we give a short introduction to logicprogramming approach to knowledge representation and reasoning. the intention is to help the reader to develop a 'feel' for the field's history and some ...
详细信息
In this paper we give a short introduction to logicprogramming approach to knowledge representation and reasoning. the intention is to help the reader to develop a 'feel' for the field's history and some of its recent developments. the discussion is mainly limited to logic programs under the answer set semantics. For understanding of approaches to logicprogramming built on well-founded semantics, general theories of argumentation, abductive reasoning, etc., the reader is referred to other publications. (C) 2002 Elsevier Science B.V. All rights reserved.
the idea of answer set programming is to represent a given computational problem by a logic program whose answer sets correspond to solutions, and then use an answer set solver, such as SMODELS or DLV, to find an answ...
详细信息
the idea of answer set programming is to represent a given computational problem by a logic program whose answer sets correspond to solutions, and then use an answer set solver, such as SMODELS or DLV, to find an answer set for this program. Applications of this method to planning are related to the line of research on the frame problem that started withthe invention of formal nonmonotonicreasoning in 1980. (C) 2002 Elsevier Science B.V. All rights reserved.
暂无评论