the proceedings contain 15 papers. the topics discussed include: on optimising shape-generic array programs using symbolic structural information;index vector elimination-making index vectors affordable;functional-bas...
详细信息
ISBN:
(纸本)9783540741299
the proceedings contain 15 papers. the topics discussed include: on optimising shape-generic array programs using symbolic structural information;index vector elimination-making index vectors affordable;functional-based synthesis of a systolic array for GCD computation;comparing alternative evaluation strategies for stream-based parallel functional languages;parallel coordination made explicit in a functional setting;a conference management system based on the iData toolkit;a pattern logic for prompt lazy assertions in Haskell;IVOR,a proof engine;proving program properties specified with subtype marks;uniqueness typing redefined;heuristics for type error discovery and recovery;testing properties of generic functions;worst-case execution times for a purely functional language;and automatic partial inversion of inductively sequential functions.
the need for a more autonomous management of distributed systems and networks has driven research and industry to look for management frameworks that go beyond the direct manipulation of network devices and systems. O...
详细信息
ISBN:
(纸本)9783540721994
the need for a more autonomous management of distributed systems and networks has driven research and industry to look for management frameworks that go beyond the direct manipulation of network devices and systems. One approach towards this aim is to build policy-based management systems. Policy-based computing refers to a software paradigm developed around the concept of building autonomous systems that provide system administrators and decision makers with interfaces that let them set general guiding principles and policies to govern the behavior and interactions of the managed systems. Although many of the tasks are still carried out manually and ad hoc, instances of limited policy-based systems can be found in areas such as Internet service management, privacy, security and access management, management of quality of service and service level agreements in networks. Policies can be specified at many levels of abstraction, from natural language specifications to more elementary condition-action rule specifications. From these specifications policy systems need to come up with implementations. Some of these implementations can be done automatically, others require manual steps. In some cases policies impose legal commitments and systems should be able to demonstrate compliance. there are also situations in which policies are in conflict with each other and a system cannot implement them simultaneously without providing methods for conflict resolution. In this presentation I will review a few policy systems, applications and specification languages. then I will provide a more formal characterization of policies and their computational model. I will show a simple policy language in the style of the action description language A. I will discuss current solutions to policy conflicts, discuss the problem of policy refinement, i.e. transformations from high level specifications to lower level specifications, current approaches to refinement and provide a partial formal
the proceedings contain 36 papers. the topics discussed include: a decomposition rule for decision procedures by resolution-based calculi;combining lists with non-stably infinite theories;abstract model generation for...
详细信息
ISBN:
(纸本)3540252363
the proceedings contain 36 papers. the topics discussed include: a decomposition rule for decision procedures by resolution-based calculi;combining lists with non-stably infinite theories;abstract model generation for preprocessing clause sets;flat and one-variable clauses: complexity of verifying cryptographic protocols with single blind copying;applications of general exact satisfiablility in propositional logic modeling;suitable graphs for answer set programming;how to fix it: using fixpoints in different contexts;reasoning about systems with transition fairness;the inverse method for the logic of bunched implications;and implementing efficient resource management for linear logicprogramming.
the proceedings contain 50 papers. the topics discussed include: independently checkable proofs from decision procedures: issues and progress;Zap: automated theorem proving for software analysis;scaling up: computers ...
详细信息
the proceedings contain 50 papers. the topics discussed include: independently checkable proofs from decision procedures: issues and progress;Zap: automated theorem proving for software analysis;scaling up: computers vs. common sense;a new constraint solver for 3D lattices and its application to the protein folding problem;disjunctive constraint lambda calculi;optimizing the runtime processing of types in polymorphic logicprogramming languages;the four sons of penrose;termination of fair computations in term rewriting;matching with regular constraints;automating coherent logic;regular derivations in basic superposition-based calculi;on the specification on sequent systems;experimental evaluation of classical automata constructions;reasoning about incompletely defined programs;a unified memory model for pointers;pushdown module checking;functional correctness proofs of encryption algorithms;and algebraic intruder deductions.
Two popular approaches to formalize adequate reasoning with vague propositions are usually deemed incompatible: On the one hand, there is supervaluation with respect to precisification spaces, which consist in collect...
详细信息
ISBN:
(纸本)3540482814
Two popular approaches to formalize adequate reasoning with vague propositions are usually deemed incompatible: On the one hand, there is supervaluation with respect to precisification spaces, which consist in collections of classical interpretations that represent admissible ways of making vague atomic statements precise. On the other hand, t-norm based fuzzy logics model truth functional reasoning, where reals in the unit interval [0, 1] are interpreted as degrees of truth. We show that both types of reasoning can be combined within a single logic SL, that extends both: Lukasiewicz logic L and (classical) S5, where the modality corresponds to '... is true in all complete precisifications'. Our main result consists in a game theoretic interpretation of SL, building on ideas already introduced by Robin Giles in the 1970s to obtain a characterization of L in terms of a Lorenzen style dialogue game combined with bets on the results of binary experiments that may show dispersion. In our case the experiments are replaced by random evaluations with respect to a given probability distribution over permissible precisifications.
In this paper we present a method of integrating theory reasoning into the instantiation framework. this integration is done in the black-box style, which allows us to integrate different theories in a uniform way. We...
详细信息
ISBN:
(纸本)3540482814
In this paper we present a method of integrating theory reasoning into the instantiation framework. this integration is done in the black-box style, which allows us to integrate different theories in a uniform way. We prove completeness of the resulting calculus, provided that the theory reasoner is answer-complete and complete for reasoning with ground clauses. One of the distinctive features of our approach is that it allows us to employ off-the-shelf satisfiability solvers for ground clauses modulo theories, as a part of general first-order reasoning. As an application of this approach, we show how it is possible to combine the instantiation calculus with other calculi, such as ordered resolution and paramodulation.
Decision procedures are widely used in automated reasoning tools in order to reason about data structures. In applications, many conjectures fall outside the theory handled by a decision procedure. Often, reasoning ab...
详细信息
ISBN:
(纸本)3540482814
Decision procedures are widely used in automated reasoning tools in order to reason about data structures. In applications, many conjectures fall outside the theory handled by a decision procedure. Often, reasoning about user-defined functions on those data structures is needed. For this, inductive reasoning has to be employed. In this work, classes of function definitions and conjectures are identified for which inductive validity can be automatically decided using implicit induction methods and decision procedures for an underlying theory. the class of equational conjectures considered in this paper significantly extends the results of Kapur & Subramaniam (CADE, 2000) [15], which were obtained using explicit induction schemes. Firstly, nonlinear conjectures can be decided automatically. Secondly, function definitions can use other defined functions in their definitions, thus allowing mutually recursive functions and decidable conjectures about them. thirdly, conjectures can have general terms from the decidable theory on inductive positions. these contributions are crucial for successfully integrating inductive reasoning into decision procedures, thus enabling their use in push-button mode in applications including verification and program analysis.
In logic programs, negation-as-failure has been used both for representing negative information and for providing default non-monotonic inference. In this paper we argue that this twofold role is not only unnecessary ...
详细信息
ISBN:
(纸本)3540482814
In logic programs, negation-as-failure has been used both for representing negative information and for providing default non-monotonic inference. In this paper we argue that this twofold role is not only unnecessary for the expressiveness of the language, but it also plays against declarative programming, especially if further negation symbols such as strong negation are also available. We therefore propose a new logicprogramming approach in which negation and default inference are independent, orthogonal concepts. Semantical characterization of this approach is given in the style of answer sets, but other approaches are also possible. Finally, we compare them withthe semantics for logic programs with two kinds of negation.
Modular cut-elimination is a particular notion of "cut-elimination in the presence of non-logical axioms" that is preserved under the addition of suitable rules. We introduce syntactic necessary and sufficie...
详细信息
ISBN:
(纸本)3540482814
Modular cut-elimination is a particular notion of "cut-elimination in the presence of non-logical axioms" that is preserved under the addition of suitable rules. We introduce syntactic necessary and sufficient conditions for modular cut-elimination for standard calculi, a wide class of (possibly) multiple-conclusion sequent calculi with generalized quantifiers. We provide a "universal" modular cut-elimination procedure that works uniformly for any standard calculus satisfying our conditions. the failure of these conditions generates counterexamples for modular cut-elimination and, in certain cases, for cut-elimination.
Many modern applications of description logics (DLs) require answering queries over large data quantities, structured according to relatively simple ontologies. For such applications, we conjectured that reusing ideas...
详细信息
ISBN:
(纸本)3540482814
Many modern applications of description logics (DLs) require answering queries over large data quantities, structured according to relatively simple ontologies. For such applications, we conjectured that reusing ideas of deductive databases might improve scalability of DL systems. Hence, in our previous work, we developed an algorithm for reducing a DL knowledge base to a disjunctive datalog program. To test our conjecture, we implemented our algorithm in a new DL reasoner KAON2, which we describe in this paper. Furthermore, we created a comprehensive test suite and used it to conduct a performance evaluation. Our results show that, on knowledge bases with large ABoxes but with simple TBoxes, our technique indeed shows good performance;in contrast, on knowledge bases with large and complex TBoxes, existing techniques still perform better. this allowed us to gain important insights into strengths and weaknesses of both approaches.
暂无评论