the research on systems of logicprogramming with modules has followed two mainstreams, programming-in-the-large, where compositional operators are provided for combining separate and independent modules, and programm...
详细信息
ISBN:
(纸本)3540632557
the research on systems of logicprogramming with modules has followed two mainstreams, programming-in-the-large, where compositional operators are provided for combining separate and independent modules, and programming-in-the-small, which aims at enhancing logicprogramming with new logical connectives. In this paper, we present a general model theoretic approach to modular logicprogramming which combines programming in-the-large and in-the-small in a satisfactory way. Rather than inventing completely new constructs, however, we resort to a well-known concept in formal logic: generalized quantifiers. We show how generalized quantifiers can be incorporated into logic programs, both for Horn logic programs as well as in the presence of negation. Our basic observation is then that a logic program can be seen as a generalized quantifier, and we obtain a semantics for modular logic programs this way. Generalized quantifiers in logic programs gives rise to interesting classes of logic programs. We present a taxonomy of natural such classes, and investigate their properties. In particular, their expressive power over finite structures is analyzed.
A numerical model for the solute transport and dispersion in saturated porous media has been developed. the partial differential equations for water flow and solute transport are discretized using the finite differenc...
详细信息
A numerical model for the solute transport and dispersion in saturated porous media has been developed. the partial differential equations for water flow and solute transport are discretized using the finite difference technique and the resulting system of algebraic equations is solved using a dynamic programming method. the advantage of this method is that the problem is converted from solving an algebraic system of order NC(NL-1)×NC(NL-1) into that of solving a difference equation of order NC×NC over NL-1 steps and involving NL-1 matrix inversions of order NC×NC. the accuracy and precision of the solutions are shown by calculation of mass balance and comparing the results with MOC model developed by USGS.
Limiting the number of times a variable appears in either the head or the body of a rule, we identify two classes of normal propositional logic programs. these classes have the desirable property that stable models, i...
详细信息
ISBN:
(纸本)3540632557
Limiting the number of times a variable appears in either the head or the body of a rule, we identify two classes of normal propositional logic programs. these classes have the desirable property that stable models, if they exist, can be found in linear time (worst case). We also identify a related class containing;programs for which the well-founded model can be acquired in linear time, yet for which computing the stable model(s) remains NP-complete. We show in this class how, by relaxing one constraint, previously linear complexity is increased to intractability.
We present an implementation platform for query-answering in default logics. the overall approach along with its implementation, the XRay system, allows for query-answering from default theories supporting local proof...
详细信息
ISBN:
(纸本)3540632557
We present an implementation platform for query-answering in default logics. the overall approach along with its implementation, the XRay system, allows for query-answering from default theories supporting local proof procedures. the deductive power of XRay stems from its usage of Prolog Technology theorem Proving Techniques (PTTP) supported by further enhancements, such as default lemma handling and regularity-based truncations of the underlying search space. the generality of the approach, allowing for a (simultaneous) treatment of different default logics, stems from a novel model-based approach to consistency checking.
In automatic mapping of parallel programs to target parallel machines the efficiency of the compile-time cost estimation needed to steer the optimization process is highly dependent on the choice of programming model....
详细信息
In automatic mapping of parallel programs to target parallel machines the efficiency of the compile-time cost estimation needed to steer the optimization process is highly dependent on the choice of programming model. Recently a new parallel programming model, called SPC, has been introduced that specifically aims at the efficient computation of reliable cost estimates, paving the way for automatic mapping. In SPC all algorithm level parallelism is explicitly specified, relying on compile-time transformation of the possibly unbounded algorithm level (data) parallelism to that of the actual target machine. In this paper we present SPC's process-algebraic framework in terms of which we demonstrate that the transformations needed to efficiently support unbounded process parallelism at program level are straightforward.
the advantages of FLORID as a deductive object-oriented databaSe system are the rich object-oriented modeling facilities of its language Flogic. the focus of this paper is on FLORID’S multiple inheritance mechanism w...
详细信息
We present a spectrum of default logics, using powerdoma~ns to encode default constraints. the resulting non-monotonic entailment relations all satisfy the law of reasoning by cases. this result is a consequence of tw...
详细信息
the Smodels system is a C++ implementation of the well-founded and stable model semantics for range-restricted function-free normal programs. the system includes two modules: (i) smodels which implements the two seman...
详细信息
ISBN:
(纸本)3540632557
the Smodels system is a C++ implementation of the well-founded and stable model semantics for range-restricted function-free normal programs. the system includes two modules: (i) smodels which implements the two semantics for ground programs and (ii) parse which computes a grounded version of a range-restricted function-free normal program. the latter module does not produce the whole set of ground instances of the program but a subset that is sufficient in the sense that no stable models ate lost. the implementation of the stable model semantics for ground programs is based on bottom-up backtracking search where a powerful pruning method is employed. the pruning method exploits an approximation technique for stable models which is closely related to the well-founded semantics. One of the advantages of this novel technique is that it can be implemented to work in linear space. this makes it possible to apply the stable model semantics also in areas where resulting programs are highly non-stratified and can possess a large number of stable models. the implementation has been tested extensively and compared with a state of the art implementation of the stable model semantics, the SLG system. In tests involving ground programs it clearly outperforms SLG.
the proceedings contain 42 papers. the special focus in this conference is on logical Foundations of Computer Science. the topics include: Topological Semantics for Hybrid Systems;Domain-Free Pure Type Systems;Generic...
ISBN:
(纸本)3540630457
the proceedings contain 42 papers. the special focus in this conference is on logical Foundations of Computer Science. the topics include: Topological Semantics for Hybrid Systems;Domain-Free Pure Type Systems;Generic Queries over Quasi-o-minimal Domains;Towards Computing Distances Between Programs via Scott Domains;A Safe Recursion Scheme for Exponential Time;Finite Model theory, Universal Algebra and Graph Grammars;Complexity of Query Answering in logic Databases with Complex Values;Recognition of Deductive Data Base Stability;the Concurrency Complexity for the Horn Fragment of Linear logic;Studying Algorithmic Problems for Free Semi-groups and Groups;Learning Small Programs with Additional Information;Cut Elimination for the Second Order Propositional logic with Hilbert ' s e-symbol, Extensionality, and Full Comprehension;Finite Bases of Admissible Rules for the logic S52C;An algebraic Correctness Criterion for Intuitionistic Proof-Nets;Towards a theory of Recursive Structures;On the Complexity of Prefix Formulas in Modal logic of Subset Spaces;the Undecidability of Second Order Linear Affine logic;Operational logic of Proofs with Functionality Condition on Proof Predicate;On Linear Ordering of Strongly Extensional Finitely-Branching Graphs and Non-well-founded Sets;Functions for the General Solution of Parametric Word Equations;A Proof Procedure for Hereditary Harrop Formulas with Free Equality;Basic Forward Chaining Construction for logic Programs;Decidability and Undecidability of the Halting Problem on Turing Machines, a Survey;Additive Linear logic and Lattices;Some Decision Problems for Traces and Existential Instantiation and Strong Normalization.
暂无评论