We present KLMLean 2.0, a theorem prover for propositional KLM logics of nonmonotonic reasoning. KLMLean 2.0 implements some analytic tableaux calculi for these logics recently introduced. KLMLean 2.0 is inspired by t...
详细信息
ISBN:
(纸本)9783540730989
We present KLMLean 2.0, a theorem prover for propositional KLM logics of nonmonotonic reasoning. KLMLean 2.0 implements some analytic tableaux calculi for these logics recently introduced. KLMLean 2.0 is inspired by the "lean" methodology, it is implemented in SICStus I Prolog and it also contains a graphical interface written in Java.
Subintuitionistic logics are a class of logics defined by using Kripke models with more general conditions than those for intuitionistic logic. In this paper we study predicate logics of this kind by the method of tre...
详细信息
ISBN:
(纸本)9783540730989
Subintuitionistic logics are a class of logics defined by using Kripke models with more general conditions than those for intuitionistic logic. In this paper we study predicate logics of this kind by the method of tree-sequent calculus (a special form of Labelled Deductive System). After proving the completeness with respect to some classes of Kripke models, we introduce Hilbert-style axiom systems and prove their completeness through a translation from the tree-sequent calculi. this gives a solution to the problem posed by Restall.
the recently proposed notion of an elementary set yielded a refinement of the theorem on loop formulas, telling us that the stable models of a disjunctive logic program can be characterized by the loop formulas of its...
详细信息
ISBN:
(纸本)9783540721994
the recently proposed notion of an elementary set yielded a refinement of the theorem on loop formulas, telling us that the stable models of a disjunctive logic program can be characterized by the loop formulas of its elementary sets. Based on the notion of an elementary set, we propose the notion of head-elementary-set-free (HEF) programs, a more general class of disjunctive programs than head-cycle-free (HCF) programs proposed by Ben-Eliyahu and Dechter, that can still be turned into nondisjunctive programs in polynomial time and space by "shifting" the head atoms into the body. We show several properties of HEF programs that generalize earlier results on HCF programs. Given an HEF program, we provide an algorithm for finding an elementary set whose loop formula is not satisfied, which has a potential for improving stable model computation by answer set solvers.
Global Abduction (GA) is a recently proposed logical formalism for agent oriented programming which allows an agent to collect information about the world and update this in a nonmonotonic: way when changes in the wor...
详细信息
ISBN:
(纸本)9783540696186
Global Abduction (GA) is a recently proposed logical formalism for agent oriented programming which allows an agent to collect information about the world and update this in a nonmonotonic: way when changes in the world are observed. A distinct feature of Global Abduction is that in case the agent needs to give up one plan, it may start a new one, or continue a suspended plan, while its beliefs learned about the world in the failed attempts persist. this paper describes an implementation of GA in the high-level language of Constraint Handling Rules (CHR). It appears to be a first attempt to a full implementation of GA, which also confirms CHR as a powerful meta-programming language for advanced reasoning. the construction gives rise a discussion of important issues of the semantics and pragmatics of Global Abduction, leading to proposals for a specific procedural semantics and architecture that seem well suited for real-time applications.
We introduce the logic-based planning language K-c as an extension of K [5]. K-c has two advantages upon K. First, the introduction of external function calls in the rules of a planning description allows the knowledg...
详细信息
ISBN:
(纸本)9783540721994
We introduce the logic-based planning language K-c as an extension of K [5]. K-c has two advantages upon K. First, the introduction of external function calls in the rules of a planning description allows the knowledge engineer to describe certain planning domains, e.g. involving complex action effects, in a more intuitive fashion then is possible in K. Secondly, in contrast to the conformant planning framework K, K-c is formalized as a conditional planning system, which enables K-c to solve planning problems that are impossible to express in K, e.g. involving sensing actions. A prototype implementation of conditional planning with K-c is build on top of the DLVK system, and we illustrate its use by some small examples.
the proceedings contain 86 papers. the topics discussed include: from fuzzy beliefs to goals;information entropy and co-entropy of crisp and fuzzy granulations;possibilistic linear programming in blending and transpor...
详细信息
ISBN:
(纸本)9783540733997
the proceedings contain 86 papers. the topics discussed include: from fuzzy beliefs to goals;information entropy and co-entropy of crisp and fuzzy granulations;possibilistic linear programming in blending and transportation planning problem;measuring the interpretive cost in fuzzy logic computations;a fixed-point theorem for multi-valued functions with an application to multilattice-based logicprogramming;contexualized possibilistic networks with temporal framework for knowledge base reliability improvement;reconstruction of the matrix of casual dependencies for the fuzzy inductive reasoning method;derivative information from fuzzy models;the genetic development of uninorm-based neurons;using visualization tools to guide consensus in group decision making;reconstruction methods for incomplete fuzzy preference relations: a numerical comparison;web user profiling using fuzzy clustering;and exploring the application of fuzzy logic and data fusion mechanisms in QAS.
the addition of aggregates has been one of the most relevant enhancements to the language of answer set programming (ASP). they strengthen the modelling power of ASP in terms of natural and concise problem representat...
详细信息
ISBN:
(纸本)9783540721994
the addition of aggregates has been one of the most relevant enhancements to the language of answer set programming (ASP). they strengthen the modelling power of ASP in terms of natural and concise problem representations. In this paper, we carry out an in-depth study of the computational complexity of the language. the analysis pays particular attention to the impact of syntactical restrictions on programs in the form of limited use of aggregates, disjunction, and negation. While the addition of aggregates does not affect the complexity of the full language with negation and disjunction, it turns out that their presence does increase the complexity of non-disjunctive ASP programs up to the second level of the polynomial hierarchy. Interestingly, under cautious reasoning non-monotone aggregates are even harder than disjunction (Pi(P)(2)-complete vs co-NP-complete on positive programs). However, we show that there are large classes of aggregates the addition of which does not cause any complexity gap even for normal programs, including the fragment allowing for arbitrary monotone, arbitrary antimonotone, and stratified (i.e., non-recursive) nonmonotone aggregates. Moreover, we also prove that for positive programs with arbitrary monotone, stratified antimonotone, and stratified nonmonotone aggregates the complexity remains polynomial. this analysis provides some useful indications on the possibility to implement aggregates in existing reasoning engines.
An approximate Herbrand theorem is proved and used to establish Skolemization for first-order Lukasiewicz logic. Proof systems are then defined in the framework of hypersequents. In particular, extending a hypersequen...
详细信息
ISBN:
(纸本)9783540730989
An approximate Herbrand theorem is proved and used to establish Skolemization for first-order Lukasiewicz logic. Proof systems are then defined in the framework of hypersequents. In particular, extending a hypersequent calculus for propositional Lukasiewicz logic with usual Gentzen quantifier rules gives a calculus that is complete with respect to interpretations in safe MV-algebras, but lacks cut-elimination. Adding an infinitary rule to the cut-free version of this calculus gives a system that is complete for the full logic. Finally, a cut-free calculus with finitary rules is obtained for the one-variable fragment by relaxing the eigenvariable condition for quantifier rules.
Recent research in answer-set programming (ASP) is concerned withthe problem of finding faithful transformations of logic programs under the stable semantics. this is in particular relevant in practice when programs ...
详细信息
ISBN:
(纸本)9783540721994
Recent research in answer-set programming (ASP) is concerned withthe problem of finding faithful transformations of logic programs under the stable semantics. this is in particular relevant in practice when programs with variables are considered, where such transformations play a basic role in (offline) simplifications of logic programs. So far, such transformations of non-ground programs have been considered under the implicit assumption that the domain (i.e., the set of constants of the underlying language) is always suitably extensible. However, this may not be a desired scenario, e.g., if one needs to deal with a fixed number of objects. In this paper, we investigate how an explicit restriction of the domain influences the applicability of program transformations and we study in detail computational aspects for the concepts of tautological rules and rule sub-sumption. More precisely, we provide a full picture of the complexity to decide whether a non-ground rule is tautological or subsumed by another rule under several restrictions.
It is recognised that institutions are potentially powerful means for making agent interactions effective and efficient, but institutions will only really be useful when, as in other safety-critical scenarios, it is p...
详细信息
ISBN:
(纸本)9783540696186
It is recognised that institutions are potentially powerful means for making agent interactions effective and efficient, but institutions will only really be useful when, as in other safety-critical scenarios, it is possible to prove that particular properties do or do not hold for all possible encounters. In contrast to symbolic model-checking, answer set programming permits the statement of problems and queries in domain-specific terms as executable logic programs, thus eliminating the gap between specification and verification language. Furthermore, results are presented in the same terms. In this paper we describe the use of answer set programs as an institutional modelling technique. We demonstrate that our institutional model can be intuitively be mapped into an answer set program such that the ordered event traces of the former can be obtained as the answer sets of the latter, allowing for an easy way to query properties of models.
暂无评论