this paper surveys category-based equational logic, which generalises boththe theoretical and computational aspects of equational logic and its model theory (general algebra) far beyond terms, so as to include: Horn ...
详细信息
logic programs augmented with delay declarations form a higly expressive programming language in which dynamic networks of processes that communicate asynchronously by means of multiparty channeis can be easily create...
详细信息
We illustrate the use of a declarative programming paradigm based upon three kinds of program clauses: equational, subset, and general relational clauses. the implemented language is called SURE, which is an acronym f...
详细信息
this paper introduces a logic for a class of properties - in particular variable aliasing - used in static analysis of logic programs. the logic is shown to be sound, complete and decidable. Moreover, it is illustrate...
详细信息
this paper studies the relationship between logic programs and term rewriting systems (TRSs). A compositional transform is defined which given a logic program computes a TRS. For a relevant class of logic programs, ca...
详细信息
We study how to preserve universal termination besides computed answer substitutions while transforming definite programs. We consider the unfold operation both alone and combined withthe introduction of a new defini...
详细信息
We describe LC, a formalism based on the proof theory of linear logic, whose aim is to specify concurrent computations and whose language restriction (as compared to other linear logic language) provides a simpler ope...
详细信息
Multiset rewriting has proved to be a useful presentation of process synchronization [1, 2, 3, 6]. Since sequent calculus presentations of logics that do not use the structural rules of contractions and weakening are ...
详细信息
ISBN:
(纸本)9783540584315
Multiset rewriting has proved to be a useful presentation of process synchronization [1, 2, 3, 6]. Since sequent calculus presentations of logics that do not use the structural rules of contractions and weakening are based on using multisets of formulas as left and right contexts, it is natural to identify processes with formulas, multisets with sequent contexts, and multiset rewriting as an inference rule. Given earlier work on using sequent calculus to describe logicprogramming as goal-directed search for proofs [8], it is most natural to use right-hand contexts of sequents to represent multisets of processes. this choice requires the identification of the multiset constructor and the empty multiset withthe multiplicative disjunction and false (the and ⊥ of linear logic [4]), and backchaining with a single step of multiset rewriting. While the logicprogramming language λ Prolog [10] and its linear logic refinement Lolli [5] contain rich sources of abstraction (such as modular programming, abstract data types, and higher-order programming), they contain no primitives for specifying concurrency, communications, or synchronization. If multiset rewriting is added to Lolli via the logical connectives and ⊥, the result is a language that contains primitives for both abstraction and concurrency. Surprisingly, the resulting logic, called Forum [7], is a presentation of all of linear logic in the sense that all of the connectives of linear logic can be defined via logical equivalences using only the connectives of Forum. thus the rich meta-theory of linear logic, for example, the de Morgan dualities and cut-elimination, can be applied to the analysis of Forum programs. Several examples to illustrate the expressiveness of this presentation of linear logic will be given. these examples will involve a specification of sequent calculi for object-level logics, a specification of the π-calculus [9], and a specification of a functional programming language that contains side-e
作者：
Bidoit, MichelHennicker, RolfLIENS
C.N.R.S. U.R.A. 1327 & Ecole Normale Supérieure 45 Rue d’Ulm Paris Cedex 05F-75230 France Institut für Informatik
Ludwig-Maximilians-Universität München Leopoldstr. 11B MünchenD-80802 Germany
Behavioural logic is a generalization of first-order logic where the equality predicate is interpreted by a behavioural equality of objects (and not by their identity). We establish simple and general sufficient condi...
详细信息
Birkhoff’s HSP theorem is that the models of a set of algebraic equations form a variety, i.e. a category of algebras which admits homomorphic images, subalgebras and products. We show here first, that every equation...
详细信息
暂无评论