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.
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 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.
Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of the form for all x.A (for quantifier-...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of the form for all x.A (for quantifier-free A) to a method generating lemmas of the form for all x(1) ... for all x(n).A. Moreover, we extend the original method to predicate logic with equality. the new method was implemented and applied to the TSTP proof database. It is shown that the extension of the method to handle equality and quantifier-blocks leads to a substantial improvement of the old algorithm.
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.
We present the first terminating tableau calculus for basic hybrid logic withthe difference modality and converse modalities. the language under consideration is basic multi-modal logic extended with nominals, the sa...
详细信息
ISBN:
(纸本)9783540710691
We present the first terminating tableau calculus for basic hybrid logic withthe difference modality and converse modalities. the language under consideration is basic multi-modal logic extended with nominals, the satisfaction operator, converse, global and difference modalities. All of the constructs are handled natively. To obtain termination, we extend chain-based blocking for logics with converse by a complete treatment of difference. Completeness of our calculus is shown via a model existence theorem that refines previous constructions by distinguishing between modal and equational state equivalence.
the goal of this article is to formalize Object Role Modeling (ORM) using the DLR description logic. this would enable automatedreasoning on the formal properties of ORM diagrams, such as detecting constraint contrad...
详细信息
ISBN:
(纸本)9783540755623
the goal of this article is to formalize Object Role Modeling (ORM) using the DLR description logic. this would enable automatedreasoning on the formal properties of ORM diagrams, such as detecting constraint contradictions and implications. In addition, the expressive, methodological, and graphical capabilities of ORM make it a good candidate for use as a graphical notation for most description logic languages. In this way, industrial experts who are not IT savvy will still be able to build and view axiomatized theories (such as ontologies, business rules, etc.) without needing to know the logic or reasoning foundations underpinning them. Our formalization in this paper is structured as 29 formalization rules, that map all ORM primitives and constraints into DLR, and 2 exceptions of complex cases. To this end, we illustrate the implementation of our formalization as an extension to DogmaModeler, which automatically maps ORM into DIG and uses Racer as a background reasoning engine to reason about ORM diagrams.
Efficient, automated climination of cuts is a prerequisite for proof analysis. the method CERES, based on Skolemization and resolution has been successfully developed for classical logic for this purpose. We generaliz...
详细信息
ISBN:
(纸本)9783540894384
Efficient, automated climination of cuts is a prerequisite for proof analysis. the method CERES, based on Skolemization and resolution has been successfully developed for classical logic for this purpose. We generalize this method to Godel logic, an important intermediate logic, which is also one of the main formalizations of fuzzy logic.
暂无评论