A general framework for revision of nonmonotonic theories is presented. this framework can be applied if the intended nonmonotonic semantics is not (weakly) cumulative. For weaker-semantics, it is shown that revision ...
详细信息
ISBN:
(纸本)3540632557
A general framework for revision of nonmonotonic theories is presented. this framework can be applied if the intended nonmonotonic semantics is not (weakly) cumulative. For weaker-semantics, it is shown that revision by contraction is not possible whenever the intended semantics satisfies Weak Cut and revision by expansion fails whenever Weak (Cautious) Monotony fails. Furthermore, it turns out that revision by expansion can be used to test whether the framework can be applied successfully and we analyse the case for logicprogramming.
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.
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.
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 33 papers. the special focus in this conference is on Static Analysis. the topics include: On sparse evaluation representations;the effects of the precision of pointer analysis;fast and effecti...
ISBN:
(纸本)9783540634683
the proceedings contain 33 papers. the special focus in this conference is on Static Analysis. the topics include: On sparse evaluation representations;the effects of the precision of pointer analysis;fast and effective procedure inlining;set-sharing is redundant for pair-sharing;an algebraic approach to sharing analysis of logic programs;logical optimality of groundness analysis;towards a cost-effective estimation of uncaught exceptions in SML programs;program analysis using mixed term and set constraints;set-based analysis for logicprogramming and tree automata;denotational abstract interpretation of functional logic programs;termination analysis for mercury;type-based analysis of communication for concurrent programming languages;true concurrency via abstract interpretation;static analysis of interaction nets for distributed implementations;type-directed flow analysis for typed intermediate languages;exact flow analysis;satisfying subtype inequalities in polynomial space;effective specialization of realistic programs via use sensitivity;coalescing conditional branches into efficient indirect jumps;automatic termination analysis for partial functions using polynomial orderings;automatically proving termination of programs in a non-strict higher-order functional language;semantic analyzer of modula-programs;abstract interpretation for improving wam code;attribute grammars and functional programming deforestation;data dependences as abstract interpretations;abstract interpretation based static analysis parameterized by semantics and practical compile-time analysis.
the proceedings contain 20 papers. the special focus in this conference is on algebraic and logicprogramming. the topics include: Concurrent constraint programming;specifications using multiple-conclusion logic progr...
ISBN:
(纸本)9783540584315
the proceedings contain 20 papers. the special focus in this conference is on algebraic and logicprogramming. the topics include: Concurrent constraint programming;specifications using multiple-conclusion logic programs;viewing a program transformation system at work;proving implications by algebraic approximation;sufficient completeness and parameterized proofs by induction;proving behavioural theorems with standard first-order logic;compositional analysis for equational horn programs;equation solving in projective planes and planar ternary rings;concurrent logicprogramming as uniform linear proofs;three-valued completion for abductive logic programs;a sequential reduction strategy;on modularity of termination and confluence properties of conditional rewrite systems;syntactical analysis of total termination;logic programs as term rewriting systems;higher-order minimal function graphs;reasoning about layered, wildcard and product patterns;preserving universal termination through unfold/fold and a logic for variable aliasing in logic programs.
暂无评论