this paper gives a summary of the First Answer Set programming System Competition that was held in conjunction withthe Ninthinternationalconference on logicprogramming and Nonmonotonic reasoning. the aims of the c...
详细信息
ISBN:
(纸本)9783540721994
this paper gives a summary of the First Answer Set programming System Competition that was held in conjunction withthe Ninthinternationalconference on logicprogramming and Nonmonotonic reasoning. the aims of the competition were twofold: first, to collect challenging benchmark problems, and second, to provide a platform to assess a broad variety of Answer Set programming systems. the competition was inspired by similar events in neighboring fields, where regular benchmarking has been a major factor behind improvements in the developed systems and their ability to address practical applications.
the proceedings contain 15 papers. the topics discussed include: animated logic: correct functional conversion to conjunctive normal form;learning precedences from simple symbol features;layered clause selection for s...
the proceedings contain 15 papers. the topics discussed include: animated logic: correct functional conversion to conjunctive normal form;learning precedences from simple symbol features;layered clause selection for saturation-based theorem proving;simplifying casts and coercions;evaluation of axiom selection techniques;equality preprocessing in connection calculi;give reasoning a Trie;directed graph networks for logical reasoning;efficient implementation of large-scale watchlists;cutting down the TPTP language (and others);and Boolean reasoning in a higher-order superposition prover.
In recent years, various crises arise frequently and cause tremendous economic and life losses. Meanwhile, current emergency decision models and decision support systems still need further improvement. this paper firs...
详细信息
In recent years, various crises arise frequently and cause tremendous economic and life losses. Meanwhile, current emergency decision models and decision support systems still need further improvement. this paper first proposes a new emergency decision model based on the combination of a new case retrieval algorithm for Case-Based reasoning (CBR) and logicreasoning, and then address a sample flood disaster emergency decision process to explain the application of the model in practice.
logicprogramming has been used as a natural framework to automate deduction in the logic of order-of-magnitude reasoning. Specifically, we introduce a Prolog implementation of the Rasiowa-Sikorski proof system associ...
详细信息
logicprogramming has been used as a natural framework to automate deduction in the logic of order-of-magnitude reasoning. Specifically, we introduce a Prolog implementation of the Rasiowa-Sikorski proof system associated withthe relational translation Re(OM) of the multi-modal logic of order-of-magnitude qualitative reasoning OM.
the dependency pair approach is one of the most powerful techniques for automated termination proofs of term rewrite systems. Up to now, it was regarded as one of several possible methods to prove termination. In this...
详细信息
ISBN:
(纸本)3540252363
the dependency pair approach is one of the most powerful techniques for automated termination proofs of term rewrite systems. Up to now, it was regarded as one of several possible methods to prove termination. In this paper, we show that dependency pairs can instead be used as a general concept to integrate arbitrary techniques for termination analysis. In this way, the benefits of different techniques can be combined and their modularity and power are increased significantly. We refer to this new concept as the "dependency pair framework" to distinguish it from the old "dependency pair approach". Moreover, this framework facilitates the development of new methods for termination analysis. To demonstrate this, we present several new techniques within the dependency pair framework which simplify termination problems considerably. We implemented the dependency pair framework in our termination prover AProVE and evaluated it on large collections of examples.
In this paper we propose a method for modeling social influence within the STIT approach to action. Our proposal consists in extending the STIT language with special operators that allow us to represent the consequenc...
详细信息
In this paper we propose a method for modeling social influence within the STIT approach to action. Our proposal consists in extending the STIT language with special operators that allow us to represent the consequences of an agent's choices over the rational choices of another agent.
In this paper we propose to extend the current capabilities of automatedreasoning systems by making use of techniques from integer programming. We describe the architecture of an automatedreasoning system based on a...
详细信息
ISBN:
(纸本)3540613773
In this paper we propose to extend the current capabilities of automatedreasoning systems by making use of techniques from integer programming. We describe the architecture of an automatedreasoning system based on a Herbrand procedure (enumeration of formula instances) on clauses. the input are arbitrary sentences of first-order logic. the translation into clauses is done incrementally and is controlled by a semantic tableau procedure using unification. this amounts to an incremental polynomial CNF transformation which st the same time encodes part of the tableau structure and, therefore, tableau-specific refinements that reduce the search space. Checking propositional unsatisfiability of the resulting sequence of clauses can either be done with a symbolic inference system such as the Davis-Putnam procedure or it can be done using integer programming. If the latter is used a number of advantages become apparent.
暂无评论