1,721,452 research outputs found
Program transformation: Theoretical foundations and basic techniques. Part 1
No full text[No abstract available
First order predicate calculus and logic programming. Fourth Edition
No full textThese lecture notes are intended to introduce the reader to the
basic notions of the first order predicate calculus and logic programming.
We present the axioms and the inference rules of the first order predicate
calculus in two different styles: (i) the Classical style (à la Hilbert),
and (ii) the Natural Deduction style (à la Gentzen). We also present
the semantics of this calculus following Tarski's approach. The Skolem Theorem,
the Herbrand Theorem, and the Robinson Theorem are the three steps which
lead us to the study of the Definite Logic programs. For these programs we
give the denotational semantics via the least Herbrand models, the fixpoint
semantics via the so called T_P operator, and the operational semantics
via SLD trees. Finally, we consider the issue of deriving negative information
from Definite Logic programs, and we present the theory of normal programs
and the theory of programs as conjunctions of statements.
Sections are devoted to the Gödel Completeness Theorem, the first order
predicate calculus with equality, and the Peano Arithmetic
Totally correct logic program transformations via well-founded annotations
Full text linkWe address the problem of proving the total correctness of transformations of definite logic programs. We consider a general transformation rule, called clause replacement,
which consists in transforming a program P into a new program Q by replacing a set Γ1 of
clauses occurring in P by a new set Γ2 of clauses, provided that Γ1 and Γ2 are equivalent in the least Herbrand model M(P) of the program P.
We propose a general method for proving that transformations based on clause replacement are totally correct, that is, M(P) = M(Q). Our method consists in showing that the
transformation of P into Q can be performed by: (i) adding extra arguments to predicates,
thereby deriving from the given program P an annotated program P, (ii) applying a variant
of the clause replacement rule and transforming the annotated program P into a terminating
annotated program Q, and (iii) erasing the annotations from Q, thereby getting Q.
Our method does not require that either P or Q are terminating and it is parametric with
respect to the annotations. By providing different annotations we can easily prove the total correctness of program transformations based on various versions of the popular unfolding, folding, and goal replacement rules, which can all be viewed as particular cases of our clause replacement rule
The Post-Vatican II Council and its history: Crossroads, chronologies, new perspectives of studies
No full textTransformations of logic programs with goals as arguments
No full textWe consider a simple extension of logic programming where variables may range over goals and goals may be arguments of predicates. In this language we can write logic programs which use goals as data. We give practical evidence that, by exploiting this capability when transforming programs, we can improve program efficiency. We propose a set of program transformation rules which extend the familiar unfolding and folding rules and allow us to manipulate clauses with goals which occur as arguments of predicates. In order to prove the correctness of these transformation rules, we formally define the operational semantics of our extended logic programming language. This semantics is a simple variant of LD-resolution. When suitable conditions are satisfied this semantics agrees with LD-resolution and, thus, the programs written in our extended language can be run by ordinary Prolog systems. Our transformation rules are shown to preserve the operational semantics and termination
First order predicate calculus and logic programming (Second edition)
No full textThis book introduces the reader to the basic ideas of First Order Predicate Calculus and Logic Programming
Meccanismi di sostituzione delle specie vegetali in ambienti lagunari
No full textNel lavoro vengono investigati , utilizzando modelli idraulici e di eutrofizzazione, i meccanismi di selezione delle specie algali tipiche degli ambienti lagunari. L'applicazione alla laguna di Tortolì dei suddetti modelli dimostra il ruolo dell'idrodinamica lagunare e dell'immissione di nutrienti nel contenere o favorire i processi di sostituzione di specie radicate ( quali la Zostera m.) con specie algali flottanti ( Ulva )
Derivation of efficient logic programs by specialization and reduction of nondeterminism
No full textProgram specialization is a program transformation methodology which improves program efficiency by exploiting the information about the input data which are available at compile time. We show that current techniques for program specialization based on partial evaluation do not perform well on nondeterministic logic programs. We then consider a set of transformation rules which extend the ones used for partial evaluation, and we propose a strategy for guiding the application of these extended rules so to derive very efficient specialized programs. The efficiency improvements which sometimes are exponential, are due to the reduction of nondeterminism and to the fact that the computations which are performed by the initial programs in different branches of the computation trees, are performed by the specialized programs within single branches. In order to reduce nondeterminism we also make use of mode information for guiding the unfolding process. To exemplify our technique, we show that we can automatically derive very efficient matching programs and parsers for regular languages. The derivations we have performed could not have been done by previously known partial evaluation techniques. © 2005 Springer Science + Business Media, Inc
Future directions in program transformation
No full textThe program transformation methodology can provide valuable techniques and tools for the development of programs from specifications and the reuse and customization of software products. Also various approaches to program optimization and program verification can be based on transformation techniques
- …
