We investigate revision programming, a logic-based mechanism for describing changes in databases and enforcing certain type of integrity constraints. We show that revisions justified by an initial database and a revis...
详细信息
the proceedings contain 33 papers. the special focus in this conference is on Optimization and Nonmonotonic Semantics I. the topics include: Parallel database systems;languages for polynomial-time queries;distributed ...
ISBN:
(纸本)3540589074
the proceedings contain 33 papers. the special focus in this conference is on Optimization and Nonmonotonic Semantics I. the topics include: Parallel database systems;languages for polynomial-time queries;distributed query optimization in loosely coupled multidatabase systems;on the complexity of generating optimal left-deep processing trees with cross products;querying disjunctive databases through nonmonotonic logics;on the kolmogorov expressive power of boolean query languages;on two forms of structural recursion;partial strictness in two-phase locking;unified transaction model for semantically rich operations;domain-independent queries on databases with external functions;an algebra for pomsets;on the power of stratified logic programs with value invention for expressing database transformations;a stable model semantics for behavioral inheritance in deductive object oriented languages;a rewriting technique for the analysis and the optimization of active databases;sorts in higher-order logic data languages;uniformly-distributed random generation of join orders;a probabilistic view of datalog parallelization;a first step towards implementing dynamic algebraic dependencies;constraint-generating dependencies;optimization using tuple subsumption;deterministic and non-deterministic stable model semantics for unbound DATALOG queries;revision programming, database updates and integrity constraints;some positive results for boundedness of multiple recursive rules;increment boundedness and nonrecursive incremental evaluation of datalog queries;approximation in databases;datalog queries of set constraint databases and space usage in functional query languages.
HiLog enhances the modeling capabilities of deductive data bases and logicprogramming with higher-order and meta-data constructs, complex objects, and schema browsing. Its distinctive feature, a higher-order syntax w...
详细信息
ISBN:
(纸本)3540589074
HiLog enhances the modeling capabilities of deductive data bases and logicprogramming with higher-order and meta-data constructs, complex objects, and schema browsing. Its distinctive feature, a higher-order syntax with a first-order semantics, allows for efficient implementation with speeds comparable to Prolog. In fact, HiLog implementation in XSB [29, 25] together with tabulated query evaluation offers impressive performance with negligible penalty for higher-order syntax, thereby bringing the modeling capabilities of HiLog to practical realization. the lack of sorts in HiLog, however, is somewhat of a problem in database applications, which led to a number of HiLog dialects such as DataHiLog [24]. this paper develops a comprehensive theory of sorts for HiLog. It supports HiLog's flexible higher-order syntax via a polymorphic and recursive sort structure, and it offers an easy and convenient mechanism to control the rules of well-formedness. By varying the sort structure we obtain a full spectrum of languages, ranging from classical predicate logic to the original (non-sorted) HiLog. In between, there is a number of interesting higher-order extensions of Datalog with various degrees of control over the syntax, including second-order predicate calculus with Henkin-style semantics, as described in [10]. We also discuss the benefits of using Sorted HiLog for modeling complex objects and for meta programming. Finally, Sorted HiLog can be easily incorporated into XSB, which makes its practical realization feasible.
the proceedings contain 46 papers. the special focus in this conference is on Architectures;Platforms;Tools;Arithmetic and Signal Processing. the topics include: the Design of a New FPGA Architecture;Migraton of a Dua...
ISBN:
(纸本)3540602941
the proceedings contain 46 papers. the special focus in this conference is on Architectures;Platforms;Tools;Arithmetic and Signal Processing. the topics include: the Design of a New FPGA Architecture;Migraton of a Dual Granularity Globally Interconnected PLD Architecture to a 0.5 µm TLM Process;Self-Timed FPGA Systems;XC6200 Fastmap ™ Processor Interface;the Teramac Configurable Computer Engine;Telecommunication-Oriented FPGA and Dedicated CAD System;A Configurable logic Processor for Machine Vision;Extending DSP-Boards wih FPGA-Based Structures of Interconnection;High-Speed Region Detection and Labeling Using an FPGA Based Custom Computing Platform;Using FPGAs as Control Support in MIMD Executions;Customised Hardware Based on the REDOC III Algorithm for High-Performance Date Ciphering;Using Reconfigurable Hardware to Speed up Product Development and Performance;Creation of Hardware Objects in a Reconfigurable Computer;Rapid Hardware Prototyping of Digital Signal Processing Systems Using FPGAs;Delay Minimal Mapping of RTL Structures onto LUT Based FPGAs;Some Notes Qn Power Management on FPGA-Based Systems;An Automatic Technique for Realising User Interaction Processing in PLD Based Systems;the Proper Use of Hierarchy in HDL-Based High Density FPGA Design;Compiling Regular Arrays onto FPGAs;Compiling Ruby into FPGAs;the CSYN Verilog Compiler and Other Tools;A VHDL Design Methodolgy for FPGAs;VHDL-Based Rapid Hardware Prototyping Using FPGA Technology;Integer programming for Partitioning in Software Oriented Codesign;Test Standard Serves Dual Role as On-Board programming Solution;Advanced Method for Industry Related Education with an FPGA Design Self-Learning Kit.
Producing optimal left-deep trees is known to be NP-complete for general join graphs and a quite complex cost function counting disk accesses for a special block-wise nested-loop join [2]. Independent of any cost func...
详细信息
ISBN:
(纸本)3540589074
Producing optimal left-deep trees is known to be NP-complete for general join graphs and a quite complex cost function counting disk accesses for a special block-wise nested-loop join [2]. Independent of any cost function is the dynamic programming approach to join ordering. the number of alternatives this approach generates is known as well [5]. Further, it is known that for some cost functions - those fulfilling the ASI property [4] - the problem can be solved in polynomial time for acyclic query graph, i.e., tree queries [2, 3]. Unfortunately, some cost functions like sort merge could not be treated so far. We do so by a slight detour showing that this cost function (and others too) are optimized if and only if the sum of the intermediate result sizes is minimized. this validates the database folklore that minimizing intermediate result sizes is a good heuristic. then we show that summarizing the intermediate result sizes has the ASI property. It further motivates us to restrict the subsequent investigations to this cost function called C-out for which we show that the problem remains NP-complete in the general case. then, we concentrate on the main topic of the paper: the complexity of producing left-deep processing trees possibly containing cross products. Considering cross products is known to possibly result in cheaper plans [5]. More specifically, we show that the problem (LD-X-Star) of generating optimal left-deep processing trees possibly containing cross products is NP-complete for star queries. Further, we give an algorithm for treating star queries which is more efficient than dynamic programming. the NP-completeness of LD-X-Star immediately implies the NP-completeness for the more general tree queries.
the proceedings contain 24 papers. the special focus in this conference is on logicprogramming and Automated Reasoning. the topics include: Generalization and reuse of tactic proofs;program tactics and logic tactics;...
ISBN:
(纸本)9783540582168
the proceedings contain 24 papers. the special focus in this conference is on logicprogramming and Automated Reasoning. the topics include: Generalization and reuse of tactic proofs;program tactics and logic tactics;proof plans for the correction of false conjectures;on the value of antiprenexing;implementing a finite-domain CLP-language on top of prolog;logical closures;higher-order rigid e-unification;program extraction in a logical framework setting;higher-order abstract syntax with induction in coq;towards efficient calculi for resource-oriented deductive planning;a logicprogramming framework for the abductive inference of intentions in cooperative dialogues;constraint logicprogramming in the sequent calculus;on conditional rewrite systems with extra variables and deterministic logic programs;a bottom-up reconstruction of the well-founded semantics for disjunctive logic programs;an efficient computation of the extended generalized closed world assumption by support-for-negation sets;multi-SLD resolution;on anti-links;a generic declarative diagnoser for normal logic programs;a kind of achievement by parts method and projection in temporal logicprogramming.
McMillan (1992) described a technique for deadlock detection based on net unfoldings. We extend its applicability to the properties of a temporal logic with a possibility operator. the new algorithm is shown to be pol...
详细信息
McMillan (1992) described a technique for deadlock detection based on net unfoldings. We extend its applicability to the properties of a temporal logic with a possibility operator. the new algorithm is shown to be polynomial in the size of the net for 1-safe conflict-free Petri nets, while the algorithms of the literature require exponential time.
In this paper, a logic program synthesis method from first-order logic specifications is described. the specifications are described by Horn clauses extended by universally quantified implicational formulas. these for...
详细信息
In this paper, a logic program synthesis method from first-order logic specifications is described. the specifications are described by Horn clauses extended by universally quantified implicational formulas. these formulas are transformed into definite clause programs by unfold/fold transformation. We show that some classes of first-order formulas can be successfully transformed into definite clauses by unfold/fold transformation.
the problem of composing assumption-commitment specifications arises in the hierarchical development of reactive or concurrent systems. Abadi and Lamport's composition principle has been proposed as a logic-indepe...
详细信息
the problem of composing assumption-commitment specifications arises in the hierarchical development of reactive or concurrent systems. Abadi and Lamport's composition principle has been proposed as a logic-independent solution to that problem. In this paper, we apply it to derive a parallel rule for UNITY-like assumption-commitment specifications. For that purpose, we first interpret UNITY formulas in Abadi and Lamport's compositional model. then, the premises of the parallel rule are reduced to proof obligations that can be carried with rules inherited from the UNITY logic. the approach is illustrated by an example.
this paper proposes a constructive logic in which a concurrent System can be defined as a proof of a specification. the logic is defined by adding stream types and several rules for them to a simple constructive logic...
详细信息
this paper proposes a constructive logic in which a concurrent System can be defined as a proof of a specification. the logic is defined by adding stream types and several rules for them to a simple constructive logic based on intuitionism. the unique feature of the obtained system is in the (MPST) rule, which is a kind of structural induction on streams. the (MPST) rule is based on the idea of Brouwer's theory of choice sequences in intuitionism and it allows to define a concurrent process, which is actually a Purge's mapstream function, as a proof of a specification with a good intuition on computation. Several techniques for defining stream-based concurrent programs are also presented through various examples.
暂无评论