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.
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 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.
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.
the temporal structure of legal norms is analyzed and a corresponding computable representation is developed. the aim is conceptualize satisfactorily some significant features of legal language, and provide a correct ...
详细信息
the temporal structure of legal norms is analyzed and a corresponding computable representation is developed. the aim is conceptualize satisfactorily some significant features of legal language, and provide a correct translation of this conceptualization into the framework of event calculus. Some notions are provided which may be useful for investigating the relation between time and law, in particular the tackling of problem of legal duration.
In this paper, we describe a software system for learning graph-based reasoning. the system is designed for learning Peircean graphs in an interactive fashion that allows each student to proceed in his or her own pace...
详细信息
In this work, the notion of provability for first order linear temporal logic over finite time structures, FO-LTLfin, is studied. We show that the validity problem for such a logic is not recursively enumerable, hence...
详细信息
ISBN:
(纸本)3540664920
In this work, the notion of provability for first order linear temporal logic over finite time structures, FO-LTLfin, is studied. We show that the validity problem for such a logic is not recursively enumerable, hence FO-LTLfin is not recursively axiomatizable. this negative result however does not hold in the case of bounded validity, that is truth in all temporal models where the object domain is possibly infinite, but the underlying sequence of time points does not exceed a given size. A formula is defined to be A-valid if it is true in all tempered models whose underlying time frtime is not greater them κ, where κ is any fixed positive integer. In this work a tableau calculus is defined, that is sound and complete with respect to κ-validity, when given as input the initial formula and the bound κ on the size of the temporal models. the main feature of the system, extending the prepositional calculus defined in [7], is that of explicitly denoting time points and having tableau nodes labelled by either expressions intuitively stating that a formula holds in a given temporal interval or "temporal constraints" i.e. linear inequalities on time points. Branch closure is reduced to unsatisfiability over the integers of the set of temporal constraints in the branch.
Equational problems (i.e.: First-order formulae with quantifier prefix ∃*∀*, whose only predicate symbol is syntactic equality) are an important tool in many areas of automated deduction, e.g.: Restricting the set of ...
详细信息
the proceedings contain 68 papers. the special focus in this conference is on Rough Computing, Rough Set theory and Its Applications. the topics include: Decision rules, bayes’ rule and rough sets;from computation wi...
ISBN:
(纸本)3540666451
the proceedings contain 68 papers. the special focus in this conference is on Rough Computing, Rough Set theory and Its Applications. the topics include: Decision rules, bayes’ rule and rough sets;from computation with measurements to computation with perceptions;on text mining techniques for personalization;a road to discovery science;approximate distributed synthesis and granular semantics for computing with words;discovery of rules about complications;rough genetic algorithms;a rough-fuzzy neural computational approach;toward spatial reasoning in the framework of rough mereology;an algorithm for finding equivalence relations from tables with non-deterministic information;on the extension of rough sets under incomplete information;an alternative formulation;formal rough concept analysis;noise reduction in telecommunication channels using rough sets and neural networks;rough set analysis of electrostimilation test database for the prediction of post-operative profits in cochlear implanted patients;a rough set-based approach to text classification;modular rough fuzzy MLP;correspondence and complexity results;handling missing values in rough set analysis of multi-attribute and multi-criteria decision problems;the generic rough set inductive logicprogramming model and motifs in strings;rough problem settings for inductive logicprogramming;using rough sets with heuristics to feature selection;the discretization of continuous attributes based on compatibility rough set and genetic algorithm;level cut conditioning approach to the necessity measure specification;four c-regression methods and classification functions and context-free fuzzy sets in data mining context.
In this paper we propose an abstract version of the denotational semantics defined in [8]. this leads to a precise goal-independent abstract interpretation of Prolog programs. We deal withthe control rules of Prolog ...
详细信息
ISBN:
(纸本)3540654623
In this paper we propose an abstract version of the denotational semantics defined in [8]. this leads to a precise goal-independent abstract interpretation of Prolog programs. We deal withthe control rules of Prolog and the cut operator. Moreover, we get a simple denotation for negation as finite failure. the abstract analysis is proposed both for computed answers analysis and for call patterns analysis. In both cases the abstract semantics is finitely computable.
暂无评论