Proof-search (the basis of logicprogramming) with multiplicative inference rules, such as linear logic's xR and (sic)L, is problematic because of the required non-deterministic splitting of resources. Similarly, ...
详细信息
ISBN:
(纸本)3540631046
Proof-search (the basis of logicprogramming) with multiplicative inference rules, such as linear logic's xR and (sic)L, is problematic because of the required non-deterministic splitting of resources. Similarly, searching with additive rules such as &L and +R requires a nondeterministic choice between two formulae. Many strategies which resolve such non-determinism, either locally or globally, are available. We present a characterization of a range of strategies for distributing and selecting resources in linear sequent calculus proof-search via a sequent calculus annotated with Boolean constraints. Strategies are characterized by calculations of solutions of sets of Boolean equations generated by searches. Our characterization encompasses lazy (or local), eager (or global) and intermediate (mixed local and global) strategies.
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 a Prolog program that implements a sound and complete theorem prover for first-order intuitionistic logic. It is based on free-variable semantic tableaux extended by an additional string unification to ensu...
详细信息
ISBN:
(纸本)3540629203
We present a Prolog program that implements a sound and complete theorem prover for first-order intuitionistic logic. It is based on free-variable semantic tableaux extended by an additional string unification to ensure the particular restrictions in intuitionistic logic. Due to the modular treatment of the different logical connectives the implementation can easily be adapted to deal with other non-classical logics.
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 proceedings contain 17 papers. the special focus in this conference is on logic Program Synthesis and Transformation. the topics include: A multi-level approach to program synthesis;programs without failures;gener...
ISBN:
(纸本)3540650741
the proceedings contain 17 papers. the special focus in this conference is on logic Program Synthesis and Transformation. the topics include: A multi-level approach to program synthesis;programs without failures;generalised logic program transformation schemas;logic program schemas, constraints and semi-unification;implicit program synthesis by a reversible metainterpreter;termination analysis for tabled logicprogramming;on correct program schemas;analysis of logic programs with delay;constraint-based partial evaluation of rewriting-based functional logic programs;preserving termination of tabled logic programs while unfolding;unfolding the mystery of mergesort;towards a logic for reasoning about logic programs transformation;a higher order reconstruction of stepwise enhancement;development of correct transformation schemata for prolog programs;constrained regular approximation of logic programs;a logic framework for the incremental inductive synthesis of datalog theories and to parse or not to parse.
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 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...
详细信息
the objective of control generation in logicprogramming is to automatically derive a computation rule for a program that is efficient and yet does not compromise program correctness. Progress in solving this importan...
详细信息
We investigate how abduction and induction can be integrated into a common learning framework through the notion of Abductive Concept Learning (ACL). ACL is an extension of Inductive logicprogramming (ILP) to the cas...
详细信息
暂无评论