A Computational Logic - UT Computer Science

can be proved that p\=F. Of course, calling a term a “theorem” is an abuse of ...... Structures,” CS Report STAN-CS-78-678, Stanford Univer- sity, 1978.
998KB Sizes 20 Downloads 440 Views
A Computational Logic

This is a volume in the ACM MONOGRAPH SERIES Editor: THOMAS A. STANDISH, University of California at Irvine

A complete list of titles in this series appears at the end of this volume.

A Computational Logic Robert S. Boyer and J Strother Moore SRI International Menlo Park, California

ACADEMIC PRESS A subsidiary of Harcourt Brace Jovanovich, Publishers New York London Toronto Sydney San Francisco

Copyright (C) 1979 by Academic Press no part of this publication may be reproduced or transmitted in any form or by any means, electronic or mechanical, including photocoppy, recording, or any information storage and retrieval system, without permission in writing from the publisher.

ACADEMIC PRESS, INC. 111 Fifth Avenue, New York, New York 10003

United Kindom Edition published by ACADEMIC PRESS, INC. (LONDON) LTD. 24/28 Oval Road, London NW1 7DX

Library of Congress Cataloging in Publication Data Boyer, Robert S. A Computational Logic (ACM monographs series) Includes bibliographic references and index. 1. Automatic theorem proving. I. Moore, J Strother, Date joint author. II. Title. III. Series: Association of Computing Machinery. ACM monograph series. QA76.9.A96B68 519.4 79-51693 ISBN 0-12-122950-5

printed in the united states of america 79 81 81 82

987654321

To our wives, Anne and Liz

Contents Preface

vii

1 Introduction 1.1 Motivation . . . . . . . . . . . . . 1.2 Our Formal Theory . . . . . . . . 1.3 Proof Techniques . . . . . . . . . 1.4 Examples . . . . . . . . . . . . . 1.5 Our Mechanical Theorem Prover 1.6 Artificial Intelligence or Logic? . . 1.7 Organization . . . . . . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

2 A Sketch of the Theory and Two Simple Examples 2.1 An Informal Sketch of the Theory . . . 2.2 A Simple Inductive Proof . . . . . . . . 2.3 A More Difficult Problem . . . . . . . 2.4 A More Difficult Proof . . . . . . . . . 2.5 Summary . . . . . . . . . . . . . . . . 2.6 Notes . . . . . . . . . . . . . . . . . . .

1 2 3 3 3 5 6 7 9 9 18 20 23 26 27

3 A Precise Definition of the Theory 29 3.1 Syntax . . . . . . . . . . . . . . . . . . 29 v

vi

CONTENTS

3.2 3.3 3.4 3.5 3.6 3.7 3.8 3.9 3.10 3.11 3.12

The Theory of If and Equal Well-founded Relations . . . Induction . . . . . . . . . . Shells . . . . . . . . . . . . . Natural Numbers . . . . . . Literal Atoms . . . . . . . . Ordered Pairs . . . . . . . . Definitions . . . . . . . . . . Lexicographic Relations . . Lessp and Count . . . . . . Conclusion . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

31 32 34 37 41 42 44 45 53 54 57

4 The Correctness of a Tautology Checker 59 4.1 Informal Development . . . . . . . . . 60 4.2 Formal Specification of the Problem . . 63 4.3 The Formal Definition of Tautology.checker 66 4.4 The Mechanical Proofs . . . . . . . . . 71 4.5 Summary . . . . . . . . . . . . . . . . 88 4.6 Notes . . . . . . . . . . . . . . . . . . . 90 5 An Overview of How We Prove Theorems 5.1 The Role of the User . . . . . . . . . . 5.2 Clausal Representation of Conjectures 5.3 The Organization of our Heuristics . . 5.4 The Organization of our Presentation .

91 91 92 93 95

6 Using Type Information to Simplify Formulas 97 6.1 Type Sets . . . . . . . . . . . . . . . . 97 6.2 Assuming Expressions True or False . . 100

CONTENTS

6.3 6.4 6.5 6.6

Computing Type Sets . Type Prescriptions . . Summary . . . . . . . Notes . . . . . . . . . .

vii

. . . .

. . . .

. . . .

. . . .

. . . .
<