logic for programming and automatedreasoning : 6thinternationalconference, lpar'99, Tbilisi, Georgia, September 6-10, 1999 : Proceedings by lpar '99 (1999 : Tʻbilisi, Georgia); Ganzinger, H. (Harald), 1950-...
详细信息
logic for programming and automatedreasoning : 6thinternationalconference, lpar'99, Tbilisi, Georgia, September 6-10, 1999 : Proceedings by lpar '99 (1999 : Tʻbilisi, Georgia); Ganzinger, H. (Harald), 1950-; McAllester, David A; Voronkov, A. (Andreĭ), 1959-; published by Berlin ; New York : Springer
the proceedings contain 23 papers. the topics discussed include: on the complexity of counting the Hilbert basis of a linear diophantine system;solving combinatorial problems with regular local search algorithms;evide...
ISBN:
(纸本)3540664920
the proceedings contain 23 papers. the topics discussed include: on the complexity of counting the Hilbert basis of a linear diophantine system;solving combinatorial problems with regular local search algorithms;evidence algorithm and sequent logical inference search;first order linear temporal logic over finite time structures;transforming conditional rewrite systems with extra variables into unconditional systems;cancellative superposition decides the theory of divisible torsion-free Abelian groups;regular sets of descendants for constructor-based rewrite systems;practical reasoning for expressive description logics;abstracting properties in concurrent constraint programming;a fixpoint semantics for reasoning about finite failure;extensions to the estimation calculus;Beth definability for the guarded fragment;and simplification of horn clauses that are clausal forms of guarded formulas.
Our aim is to define a new fixpoint semantics which correctly models finite failure. In order to achieve this goal a new fixpoint operator is derived from a "suitable" concrete semaoitics by defining a Galoi...
详细信息
ISBN:
(纸本)3540664920
Our aim is to define a new fixpoint semantics which correctly models finite failure. In order to achieve this goal a new fixpoint operator is derived from a "suitable" concrete semaoitics by defining a Galois insertion modeling finite failure. the corresponding abstract fixpoint semantics correctly models finite failure and is and-compositional.
TLA (the Temporal logic of Actions) is a linear temporal logic for specifying and reasoning about reactive systems. We define a subset of TLA whose formulas are amenable to validation by animation, withthe intent to ...
详细信息
ISBN:
(纸本)3540664920
TLA (the Temporal logic of Actions) is a linear temporal logic for specifying and reasoning about reactive systems. We define a subset of TLA whose formulas are amenable to validation by animation, withthe intent to facilitate the communication between domain and solution experts in the design of reactive systems.
We present a denotational semantics for concurrent constraint programming based on derivations containing sequences of interactions of a process withthe environment. Our semantic is then used as collecting semantics ...
详细信息
ISBN:
(纸本)3540664920
We present a denotational semantics for concurrent constraint programming based on derivations containing sequences of interactions of a process withthe environment. Our semantic is then used as collecting semantics for abstracting properties of computations by applying techniques of abstract interpretation.
the TPTP World is a well established infrastructure supporting research, development, and deployment of automatedtheorem Proving systems. Recently, the TPTP World has been extended to include a typed first-order logi...
详细信息
ISBN:
(纸本)9783642287176
the TPTP World is a well established infrastructure supporting research, development, and deployment of automatedtheorem Proving systems. Recently, the TPTP World has been extended to include a typed first-order logic, which in turn has enabled the integration of arithmetic. this paper describes these developments.
Proving failure of queries for definite logic progrfims can be done by constructing a finite model of the program in which the query is false. A general purpose model generator for first order logic can be used for th...
详细信息
ISBN:
(纸本)3540664920
Proving failure of queries for definite logic progrfims can be done by constructing a finite model of the program in which the query is false. A general purpose model generator for first order logic can be used for this. A recent paper presented at PLILP98 shows how the peculiarities of definite progrcims can be exploited to obtain a better solution. there a procedure is described which combines abduction with tabulation and uses a meta-interpreter for heuristic control of the search. the current paper shows how similcir results Ccin be obtained by direct execution under the standard tabulation of the XSB-Prolog system. the loss of control is compensated for by better intelligent beicktracking cind more accurate failure analysis.
In this work, we develop a partial evaluation technique for residuating functional logic programs, which generalize the concurrent computation models for logic programs with delays to functional logic prograjns. We sh...
详细信息
ISBN:
(纸本)3540664920
In this work, we develop a partial evaluation technique for residuating functional logic programs, which generalize the concurrent computation models for logic programs with delays to functional logic prograjns. We show how to lift the nondeterministic choices from run time to specialization time. We ascertain the conditions under which the original and the trainsformed prograjn have the same answer expressions for the considered class of queries as well as the same floundering behavior. All these results are relevjint for prograim optimization in Curry, a functional logic language which is intended to become a staindard in this area. Preliminary empiriccil evaluation of the specialized Curry programs demonstrates that our technique also works well in practice and leads to substantial performance improvements. To our knowledge, this work is the first attempt to formally define and prove correct a generaJ scheme for the partisd evaluation of functional logic programs with delays.
Linear logic [4] has radsed a lot of interest in computer research, especially because of its resource sensitive nature. One hne of research studies proof construction procedures and their interpretation as computatio...
详细信息
ISBN:
(纸本)3540664920
Linear logic [4] has radsed a lot of interest in computer research, especially because of its resource sensitive nature. One hne of research studies proof construction procedures and their interpretation as computationil models, in the "logicprogramming" tradition. An efficient proof search procedure, based on a proof normalization result called "Focusing", has been described in [2]. Pocusing is described in terms of the sequent system of commutative Linear logic, which it refines in two steps. It is shown here that Pocusing Ccin also be interpreted in the proof-net formalism, where it appecirs, at least in the multiplicative fragment, to be a simple refinement of the "Splitting lemma" for proof-nets. this change of perspective allows to generalize the Focusing result to (the multiplicative fragment of) any logic where the "Splitting lemma" holds. this is, in particular, the CEise of the Non-Commutative logic of [1], and all the computational exploitation of Pocusing which has been performed in the commutative case can thus be revised and adapted to the non commutative case.
Linear logic provides a logical framework to express ftindamentEd computationcil concepts in a declcirative style. As a consequence, it has been used as a sound foundation for the design of expressive progreimming and...
详细信息
ISBN:
(纸本)3540664920
Linear logic provides a logical framework to express ftindamentEd computationcil concepts in a declcirative style. As a consequence, it has been used as a sound foundation for the design of expressive progreimming and specification languages. Unfortunately, linearity is as convenient for specifying as difficult to implement. In particular, the successful implementation of linear logic Ismguages Eind provers involving context splitting strongly depends on the efficiency of the method computing a suitable split. A number of solutions have been proposed, referred to as lazy splitting or resource management systems. In this paper, we present a new resource management system for the Lolli linear logic Icinguage. We show that the choice of the structure employed to represent the contexts has a strong influence on the overall performcince of the resource mzinagement system. We also estimate the performsmce of previous proposals, and compare them to our new system.
暂无评论