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.
Sequent-type proof systems constitute an important and widely-used class of calculi well-suited for analysing proof search. In this paper, we introduce a sequent-type calculus for a variant of default logic employing ...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
Sequent-type proof systems constitute an important and widely-used class of calculi well-suited for analysing proof search. In this paper, we introduce a sequent-type calculus for a variant of default logic employing Lukasiewicz's three-valued logic as the underlying base logic. this version of default logic has been introduced by Radzikowska addressing some representational shortcomings of standard default logic. More specifically, our calculus axiomatises brave reasoning for this version of default logic, following the sequent method first introduced in the context of nonmonotonic reasoning by Bonatti, which employs a complementary calculus for axiomatising invalid formulas, taking care of expressing the consistency condition of defaults.
We address the problem of computing and representing answers of constraint abduction problems over the Herbrand domain. this problem is of interest when performing type inference involving generalized algebraic data t...
详细信息
ISBN:
(纸本)9783540894384
We address the problem of computing and representing answers of constraint abduction problems over the Herbrand domain. this problem is of interest when performing type inference involving generalized algebraic data types. We show that simply recognizing a maximally general answer or fully maximal answer is co-NP complete. However we present an algorithm that computes the (finite) set of fully maximal answers of an abduction problem. the maximally general answers are generally infinite in number but we show how to generate a finite representation of them when only, unary function symbols are present.
Many applications of automated deduction require reasoning modulo some form of integer arithmetic. Unfortunately, theory reasoning support for the integers in current theorem provers is sometimes too weak for practica...
详细信息
ISBN:
(纸本)9783540894384
Many applications of automated deduction require reasoning modulo some form of integer arithmetic. Unfortunately, theory reasoning support for the integers in current theorem provers is sometimes too weak for practical purposes. In this paper we propose a novel calculus for a large fragment of first-order logic modulo Linear Integer Arithmetic (LIA) that overcomes several limitations of existing theory reasoning approaches. the new calculus - based on the Model Evolution calculus, a first-order logic version of the propositional DPLL procedure - supports restricted quantifiers, requires only a decision procedure for LIA-validity instead of a complete LIA-unification procedure, and is amenable to strong redundancy criteria. We present a basic version of the calculus and prove it sound and (refutationally) complete.
In this paper we describe Imogen. a theorem prover for intuitionistic propositional logic Using the focused inverse method. We represent fine-grained control of the search behavior by polarizing the input formula. In ...
详细信息
ISBN:
(纸本)9783540894384
In this paper we describe Imogen. a theorem prover for intuitionistic propositional logic Using the focused inverse method. We represent fine-grained control of the search behavior by polarizing the input formula. In manipulating the polarity of atoms and subformulas, we call often improve the search time by several orders of magnitude. We tested Our method against seven other systems on the propositional fragment of the ILTP library. We found that Our prover Outperforms all other provers on a Substantial subset Of the library.
the deployment of Description logics (DLs) and Answer Set programming (ASP), which are well-known knowledge representation and reasoning formalisms. to a growing range of applications has created the need for novel re...
详细信息
ISBN:
(纸本)9783540894384
the deployment of Description logics (DLs) and Answer Set programming (ASP), which are well-known knowledge representation and reasoning formalisms. to a growing range of applications has created the need for novel reasoning, algorithms and methods. Recently, knots have been introduced as a tool to facilitate reasoning tasks in extensions of ASP with functions symbols. they were then also fruitfully applied for query answering in Description logics, hinging on the forest-shaped model property of knowledge bases. this paper briefly reviews the knot idea at a generic level and recalls some of the results obtained withthen). It also discusses features of knots and relations to other reasoning techniques, and presents issues for further research.
We propose a unifying view of negation as failure, integrity constraints, and epistemic queries in nonmonotonic reasoning. Specifically, we study the relationship between satisfiability and logical implication in nonm...
详细信息
ISBN:
(纸本)0262510987
We propose a unifying view of negation as failure, integrity constraints, and epistemic queries in nonmonotonic reasoning. Specifically, we study the relationship between satisfiability and logical implication in nonmonotonic logics, showing that, in many nonmonotonic formalisms, it is possible and easy to reduce logical implication to satisfiability. this result not only allows for establishing new complexity results for the satisfiability problem in nonmonotonic logics, but also establishes a clear relationship between the studies on epistemic queries and integrity constraints in monotonic knowledge bases withthe work on negation by default in nonmonotonic reasoning and logicprogramming. From the perspective of the design of knowledge representation systems, such a reduction allows for defining both a simple method for answering epistemic queries in knowledge bases with nonmonotonic abilities, and a procedure for identifying integrity constraints in the knowledge base, which can be employed for optimizing reasoning in such systems.
Although parity constraints are at the heart of many relevant reasoning modes like sampling or model counting, little attention has so far been paid to their integration into ASP systems. We address this shortcoming a...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
Although parity constraints are at the heart of many relevant reasoning modes like sampling or model counting, little attention has so far been paid to their integration into ASP systems. We address this shortcoming and investigate a variety of alternative approaches to implementing parity constraints, ranging from rather basic ASP encodings to more sophisticated theory propagators (featuring Gauss-Jordan elimination). All of them are implemented in the xorro system by building on the theory reasoning capabilities of the ASP system dingo. Our comparative empirical study investigates the impact of the number and size of parity constraints on performance and indicates the merits of the respective implementation techniques. Finally, we benefit from parity constraints to equip xorro with means to sample answer sets, paving the way for new applications of ASP.
We show that problems arising in static analysis of XML specifications and transformations can be dealt with using techniques similar to those developed for static analysis of programs. Many properties of interest in ...
详细信息
ISBN:
(纸本)9783540894384
We show that problems arising in static analysis of XML specifications and transformations can be dealt with using techniques similar to those developed for static analysis of programs. Many properties of interest in the XML context are related to navigation, and can be formulated in temporal logics for trees. We choose a logicthat admits a simple single-exponential translation into unranked tree automata, in the spirit of the classical LTL-to-Buchi automata translation. Automata arising from this translation have a number of additional properties;in particular, they are convenient for reasoning about unary node-selecting queries, which are important in the XML context. We give two applications of such reasoning: one deals with a classical XML problem of reasoning about navigation in the presence of schemas, and the other relates to verifying security properties of XML views.
Probabilistic inductive logicprogramming, sometimes also called statistical relational learning, addresses one of the central questions of artificialintelligence: the integration of probabilistic reasoning with firs...
详细信息
ISBN:
(纸本)3540233563
Probabilistic inductive logicprogramming, sometimes also called statistical relational learning, addresses one of the central questions of artificialintelligence: the integration of probabilistic reasoning with first order logic representations and machine learning. A rich variety of different formalisms and learning techniques have been developed. In the present paper, we start from inductive logicprogramming and sketch how it can be extended with probabilistic methods. More precisely, we outline three classical settings for inductive logicprogramming, namely learning from entailment, learning from interpretations, and learning from proofs or traces, and show how they can be used to learn different types of probabilistic representations.
暂无评论