We present tableau calculi for some logics of default reasoning, as defined by Kraus, Lehmann and Magidor. We give a tableau proof procedure for preferential and cumulative logics. Our calculi are obtained by introduc...
详细信息
ISBN:
(纸本)354030553X
We present tableau calculi for some logics of default reasoning, as defined by Kraus, Lehmann and Magidor. We give a tableau proof procedure for preferential and cumulative logics. Our calculi are obtained by introducing suitable modalities to interpret conditional assertions. Moreover, they give a decision procedure for the respective logics and can be used to establish their complexity.
We present a framework for a declarative approach to spatio-temporal reasoning on geographical data, based on the constraint logical language STACLP, which offers deductive and inductive capabilities. It can be exploi...
详细信息
ISBN:
(纸本)3540255605
We present a framework for a declarative approach to spatio-temporal reasoning on geographical data, based on the constraint logical language STACLP, which offers deductive and inductive capabilities. It can be exploited for a deductive rule-based approach to represent domain knowledge on data. Furthermore, it is well suited to model trajectories of moving objects, which can be analysed by using inductive techniques, like clustering, in order to find common movement patterns. A sketch of a case study on behavioural ecology is presented.
Circumscription is one of the most important and well studied formalisms in the realm of nonmonotonic reasoning. the inference problem for propositional circumscription has been extensively studied from the viewpoint ...
详细信息
ISBN:
(纸本)3540252363
Circumscription is one of the most important and well studied formalisms in the realm of nonmonotonic reasoning. the inference problem for propositional circumscription has been extensively studied from the viewpoint of computational complexity. We prove that there exists a trichotomy for the complexity of the inference problem in propositional variable circumscription. More specifically we prove that every restricted case of the problem is either Pi(P)(2)-complete, coNP-complete, or in P.
ACMI is a decision support system for the checking of medical invoices in a German health insurance company. We present a brief overview of the system and its implementation in DLV.
ISBN:
(纸本)3540285385
ACMI is a decision support system for the checking of medical invoices in a German health insurance company. We present a brief overview of the system and its implementation in DLV.
Answer Set programming (ASP) has been demonstrated as an effective tool in various application areas, including formal verification. In this paper we present Bounded Model Checking (BMC) of Abstract State Machines (AS...
详细信息
ISBN:
(纸本)354030553X
Answer Set programming (ASP) has been demonstrated as an effective tool in various application areas, including formal verification. In this paper we present Bounded Model Checking (BMC) of Abstract State Machines (ASMs) based on ASP. We show how to succinctly translate an ASM and a temporal property into a logic program and solve the BMC problem for the ASM by computing an answer set for the corresponding program. Experimental results for our method using the answer set solvers SMODELS and CMODELS are also given.
this paper studies equivalence issues in inductive logicprogramming. A background theory B-1 is inductively equivalent to another background theory B-2 if B-1 and B-2 induce the same hypotheses for any given set of e...
详细信息
ISBN:
(纸本)3540281770
this paper studies equivalence issues in inductive logicprogramming. A background theory B-1 is inductively equivalent to another background theory B-2 if B-1 and B-2 induce the same hypotheses for any given set of examples. Inductive equivalence is useful to compare inductive capabilities among agents having different background theories. Moreover, it provides conditions for optimizing background theories through appropriate program transformations. In this paper, we consider three different classes of background theories: clausal theories, Horn logic programs, and nonmonotonic extended logic programs. We show that logical equivalence is the necessary and sufficient condition for inductive equivalence in clausal theories and Horn logic programs. In nonmonotonic extended logic programs, on the other hand, strong equivalence is necessary and sufficient for inductive equivalence in general. Interestingly, however, we observe that several existing induction algorithms require weaker conditions of equivalence under restricted problem settings. We also discuss connection to equivalence in abductive logic and conclude that the notion of strong equivalence is useful to characterize equivalence of non-deductive reasoning.
the main construction in this paper is an encoding of default logic into an "only knowing" logic with degrees of confidence. By imposing simple and natural constraints on the encoding we show that the "...
详细信息
ISBN:
(纸本)3540285385
the main construction in this paper is an encoding of default logic into an "only knowing" logic with degrees of confidence. By imposing simple and natural constraints on the encoding we show that the "only knowing" logic can accommodate ordered default theories and that the constrained encoding implements a prescriptive interpretation of preference between defaults. An advantage of the encoding is that it provides a transparent formal rendition of such a semantics. A feature of the construction is that the generation of extensions can be carried out within the "only knowing" logic, using object level concepts alone.
Given two classes of logic programs, we may be interested in modular translations from one class into the other that are sound with respect to the answer set semantics. the main theorem of this paper characterizes the...
详细信息
ISBN:
(纸本)3540285385
Given two classes of logic programs, we may be interested in modular translations from one class into the other that are sound with respect to the answer set semantics. the main theorem of this paper characterizes the existence of such a translation in terms of strong equivalence. the theorem is used to study the expressiveness of several classes of programs, including the comparison of cardinality constraints with monotone cardinality atoms.
First-order coherent logic (CL) extends resolution logic in that coherent formulas allow certain existential quantifications. A substantial number of reasoning problems (e.g., in confluence theory, lattice theory and ...
详细信息
ISBN:
(纸本)354030553X
First-order coherent logic (CL) extends resolution logic in that coherent formulas allow certain existential quantifications. A substantial number of reasoning problems (e.g., in confluence theory, lattice theory and projective geometry) can be formulated directly in CL without any clausification or Skolemization. CL has a natural proof theory, reasoning is constructive and proof objects can easily be obtained. We prove completeness of the proof theory and give a linear translation from FOL to CL that preserves logical equivalence. these properties make CL well-suited for providing automated reasoning support to logical frameworks. the proof theory has been implemented in Prolog, generating proof objects that can be verified directly in the proof assistant Coq. the prototype has been tested on the proof of Hessenberg's theorem, which could be automated to a considerable extent. Finally, we compare the prototype to some automated theorem provers on selected problems.
there is now an incredible wealth of data about individuals, businesses and organisations. this data is freely available over the Internet to almost anyone willing to pay for it, independently of whether they are iden...
详细信息
ISBN:
(纸本)354030553X
there is now an incredible wealth of data about individuals, businesses and organisations. this data is freely available over the Internet to almost anyone willing to pay for it, independently of whether they are identity thieves or credit card scam artists or legitimate users. this has led to a growing need for privacy. In this paper, we first present a simple logical model of privacy. We then show that the problem of privacy may be reduced to that of brave reasoning in default logictheories, thus reducing this important problem to a well understood reasoning paradigm. By leveraging this reduction, we are able to develop an efficient privacy preservation algorithm and a set of complexity results for privacy preservation. Efficient systems based on answer set programming are available to implement our algorithm.
暂无评论