文档介绍：THE KLUWER INTERNATIONAL SERIES
IN ENGINEERING PUTER SCIENCE
LOGIC PROGRAM SYNTHESIS
FROM PLETE INFORMATION
LOGIC PROGRAM SYNTHESIS
FROM PLETE INFORMATION
by
Pierre Flener
Bilkent University
"~.
SPRINGER-SCIENCE+BUSINESS MEDIA, .
ISBN 978-1-4613-5925-8 ISBN 978-1-4615-2205-8 (eBook)
DOI -1-4615-2205-8
Library of Congress Cataloging-in-Publication Data
A . Catalogue record for this book is available
from the Library of Congress.
Copyright © 1995 by Springer Science+Business Media Dordrecht
Originally published by Kluwer Academic Publishers in 1995
Softcover reprint ofthe hardcover lst edition 1995
AU rights reserved. No part of this publication may be reproduced, stored in
a retrieval system or transmitted in any form or by any means, mechanical,
photo-copying, recording, or otherwise, without the prior written permission of
the publisher, Springer Science+Business Media, B. V.
Printed on acid1ree paper.
Table of Contents
Lists of Logic Algorithms, Figures, and Tables ....... .. . · .. ix
Foreword. · .. xi
Preface .. · . xiii
I STATE OF THE ART
1 Automatic Programming. . . . . . . . . . . . . . ... 3
The Grand Aim of Automatic Programming . . . . 3
Specification, Algorithm, and Programming Languages 6
A Classification of Synthesis Mechanisms. . . . . . . . .10
Requirements and Promises of Automatic Programming .11
Sample Problems . . . . . . . . . . . . . . . . . . .13
2 Deductive Inference in Automatic Programming ... . .15
Specifications by Axioms ..... .15
Deductive Inference . . . . . . . . . . .18
Transfonnational Synthesis. . . 18
Proofs-as-Programs Synthesis .19
Schema-Guided Synthesis . . .21
Functional Program Synthesis from Axioms .21
Transfonnational Synthesis of LISP Programs . . .21
Proofs-as-Programs Synthesis of LISP Programs .22
Schema-Guided Synthesis of LISP Pro