The proceedings contain 13 papers. The special focus in this conference is on Extensions of logicprogramming. The topics include: logicprogramming with sequent systems;predicates as parameters in logicprogramming;a...
ISBN:
(纸本)9783540535904
The proceedings contain 13 papers. The special focus in this conference is on Extensions of logicprogramming. The topics include: logicprogramming with sequent systems;predicates as parameters in logicprogramming;a definitional approach to logicprogramming;some applications of gentzen's proof theory in automated deduction;a logic program for transforming sequent proofs to natural deduction proofs;modal provability foundations for negation by failure;extensions to logicprogramming motivated by the construction of a generic theorem prover;a decision procedure for propositional N-prolog;a logicprogramming language with lambda-abstraction, function variables, and simple unification;logicprogramming, functionalprogramming, and inductive definitions;logicprogramming with strong negation;hypothetical reasoning and definitional reflection in logicprogramming;non-monotonicity and conditionals in dialogue logic.
functional completeness of the combinatory logic means that every λ-expression may be translated into an equivalent combinator expression and this is the theoretical basis for the implementation of functional languag...
详细信息
functional completeness of the combinatory logic means that every λ-expression may be translated into an equivalent combinator expression and this is the theoretical basis for the implementation of functional languages on combinator-based abstract machines. To obtain efficient implementations it is important to distinguish between early and late binding times . i.e. to distinguish between compile-time and run-time computations. We therefore introduce a two-level version of the λ-calculus where this distinction is made in an explicit way. Turning to the combinatory logic we only wish to generate combinator-code for the run-timecomputations. The two-level version of the combinatory logic therefore will be a mixed λ-calculus and combinatory logic. A previous paper has shown that (a natural formulation of) the mixed λ-calculus and combinatory logic is not functionally complete but only corresponds to a strict subset of the two-level λ-calculus. In this paper we extend the mixed λ-calculus and combinatory logic with a new combinator, Ψ, and show that this suffices for the mixed λ-calculus and combinatory logic to be functionally complete. However, the new combinator may not always be implementable and we therefore discuss conditions under which it can be dispensed with.
This issue contains 9 conference papers. The topics covered are: algebras, polynomials, and programs;functional polymorphism;fixed points in Cartesian closed categories;guarded theories;categorical fixed point semanti...
详细信息
This issue contains 9 conference papers. The topics covered are: algebras, polynomials, and programs;functional polymorphism;fixed points in Cartesian closed categories;guarded theories;categorical fixed point semantics;functional completeness of mixed lambda-calculus and combinatory logic;recursive programs and denotational semantics in absolute logics of programs;Scott's thesis for domains of information and well-quasi-orderings;generalization of the concept of sketch. All papers are separately indexed and abstracted.
The proceedings contain 29 papers. The special focus in this conference is on Stepwise Refinement of Distributed Systems . The topics include: Composing specifications;a framework for programming in temporal logic;con...
ISBN:
(纸本)9783540525592
The proceedings contain 29 papers. The special focus in this conference is on Stepwise Refinement of Distributed Systems . The topics include: Composing specifications;a framework for programming in temporal logic;constraint-oriented specification in a constructive formal description technique;functional specification of time sensitive communicating systems;modular verification of petri nets;algebraic implementation of objects over objects;refinement of actions in causality based models;transformation of combined data type and process specifications using projection algebras;various simulations and refinements;on decomposing and refining specifications of distributed systems;verifying the correctness of aadl modules using model checking;specialization in logicprogramming: from horn clause logic to prolog and concurrent prolog;analysis of discrete event coordination;refinement and projection of relational specifications;compositional theories based on an operational semantics of contexts;multivalued possibilities mappings;completeness theorems for automata;formal verification of data type refinement -- theory and practice;from trace specifications to process terms;some comments on the assumption-commitment framework for compositional verification of distributed programs;refinement of concurrent systems based on local state transformations;a derivation of a broadcasting protocol using sequentially phased reasoning;verifying atomic data types;predicates, predicate transformers and refinement;and foundations of compositional program refinement - safety properties.
The proceedings contain 10 papers. The special focus in this conference is on foundations of logic and functionalprogramming. The topics include: Typechecking dependent types and subtypes;reducing recursion to iterat...
ISBN:
(纸本)9783540191292
The proceedings contain 10 papers. The special focus in this conference is on foundations of logic and functionalprogramming. The topics include: Typechecking dependent types and subtypes;reducing recursion to iteration by means of pairs and N-tuples;unification revisited;rule rewriting methods for efficient implementations of horn logic;a completeness result for E-unification algorithms based on conditional narrowing;representing domain structure of many-sorted Prolog knowledge bases;horn: An inference engine prototype to implement intelligent systems;PAP: a logicprogramming system based on a constructive logic.
After a brief introduction on the necessity of an explicit domain description for logic knowledge bases and the advantages of many-sorted logics, we argue that domain representation may consist of a separate logic the...
详细信息
This paper treats the problem of implementing efficiently queries expressed in a Horn clause based language when recursive predicates, possibly with function symbols, are present. The proposed approach takes the naive...
详细信息
functionallogic languages are extensions of functional languages with principles derived from logicprogramming. While syntactically they look similar to conventional functional languages, their operational semantics...
详细信息
Unification algorithms for quantified terms are needed for the implementation of extended functional and logicprogramming languages, and also for the implementation of other symbolic computation systems such as theor...
详细信息
暂无评论