In this paper, we study termination properties of input-consuming derivations of moded logicprograms. Input-consuming derivations can be used to model the behavior of logicprograms using dynamic scheduling and emplo...
详细信息
the goal of automated programsynthesis is to bridge the gap between what is easy for people to describe and what is possible to execute on a computer. In this paper, we present a framework for synthesis of rule-based...
ISBN:
(纸本)3540404384
the goal of automated programsynthesis is to bridge the gap between what is easy for people to describe and what is possible to execute on a computer. In this paper, we present a framework for synthesis of rule-based solvers for constraints given their logical specification. this approach takes advantage of the power of tabled resolution for constraint logicprogramming, in order to check the validity of the rules. Compared to previous work [8,19,2,5,3], where different methods for automatic generation of constraint solvers have been proposed, our approach enables the generation of more expressive rules (even recursive and splitting rules).
Over the last decade I have worked with colleagues on different projects to develop, implement, and automate the use of calculi for programsynthesis and transformation. these projects had different motivations and go...
详细信息
Scientists and engineers face recurring problems of constructing, testing and modifying numerical simulation programs. the process of coding and revising such simulators is extremely time-consuming, because they are a...
ISBN:
(纸本)3540678395
Scientists and engineers face recurring problems of constructing, testing and modifying numerical simulation programs. the process of coding and revising such simulators is extremely time-consuming, because they are almost always written in conventional programming languages. Scientists and engineers can therefore benefit from software that facilitates construction of programs for simulating physical systems. Our research adapts the methodology of deductive programsynthesis to the problem of constructing numerical simulation codes. We have focused on simulators that can be represented as second order functional programs composed of numerical integration and root extraction routines. We have developed a system that uses first order Horn logic to synthesize numerical simulators built from these components. Our approach is based on two ideas: First, we axiomatize only the relationship between integration and differentiation. We neither attempt nor require a complete axiomatization of mathematical analysis. Second, our system uses a representation in which functions are reified as objects. Function objects are encoded as lambda expressions. Our knowledge base includes an axiomatization of term equality in the lambda calculus. It also includes axioms defining the semantics of numerical integration and root extraction routines. We use depth bounded SLD resolution to construct proofs and synthesize programs. Our system has successfully constructed numerical simulators for computational design of jet engine nozzles and sailing yachts, among others. Our results demonstrate that deductive synthesis techniques can be used to construct numerical simulation programs for realistic applications [EM98].
Schema-basedprogramsynthesis and transformation techniques tend to be either pragmatic, designed for carrying out real programtransformation or synthesis operations but lacking the logical basis to ensure correctne...
ISBN:
(数字)9783540489580
ISBN:
(纸本)3540657657
Schema-basedprogramsynthesis and transformation techniques tend to be either pragmatic, designed for carrying out real programtransformation or synthesis operations but lacking the logical basis to ensure correctness of the programs they synthesise/transform, or rigorous, with strong theoretical foundations, but generating proof obligations which are difficult to satisfy.
the proceedings contain 19 papers. the special focus in this conference is on logicprogramsynthesis and transformation. the topics include: Preserving characteristic trees without constraints;memoing evaluation by s...
ISBN:
(纸本)3540609393
the proceedings contain 19 papers. the special focus in this conference is on logicprogramsynthesis and transformation. the topics include: Preserving characteristic trees without constraints;memoing evaluation by source-to-source transformation;transformation of left terminating programs;derivation of concurrent algorithms in tempo;an argumentation-theoretic approach to logicprogramtransformation;complexity of horn programs;studying the cost of logic languages in an abstract interpretation framework for granularity analysis;ideal refinement of datalog programs;guiding program development systems by a connection based proof strategy;towards an object-oriented methodology for deductive synthesis of logicprograms;logicprogramsynthesis by induction over horn clauses;logicprogramtransformationthrough generalization schemata;an opportunistic approach for logicprogram analysis and optimisation using enhanced schema-basedtransformations;solving deductive planning problems using program analysis and transformation;towards a complete proof procedure to prove properties of normal logicprograms under the completion;termination of logicprograms using semantic unification;on the mechanics of metasystem hierarchies in programtransformation and efficient translation of lazy functional logicprograms into prolog.
the proceedings contain 25 papers. the special focus in this conference is on programming. the topics include: Procedures and concurrency: A study in proof;another characterization of weakest preconditions;powerdomain...
ISBN:
(纸本)9783540114949
the proceedings contain 25 papers. the special focus in this conference is on programming. the topics include: Procedures and concurrency: A study in proof;another characterization of weakest preconditions;powerdomains and nondeterministic recursive definitions;optimizing for a multiprocessor: Balancing synchronization costs against parallelism in straight-line code;the simple semantics for Coppo-Dezani-Sallé types;proving the correctness of implementations of shared data abstractions;specification of communicating processes and process implementation correctness;a system for reasoning within and about algebraic specifications;tuning algebraic specifications by type merging;a machine-level semantics for nondeterministic, parallel programs;communicating agents for applicative concurrent programming;on effective computations of non-deterministic schemes;Specification and verification of concurrent systems in CESAR;proof of separability A verification technique for a class of security kernels;a method for programsynthesis;the use of transformations to implement an algorithm;a formalized proof system for total correctness of while programs;automatic programtransformation viewed as theorem proving;an enlarged definition and complete axiomatization of observational congruence of finite processes;perluette : A compilers producing system using abstract data types;a weakest precondition semantics for communicating processes;from abstract model to efficient compilation of patterns;computer-basedsynthesis of logicprograms.
暂无评论