Handbook Of Practical Logic And Automated – John Harrison

For other predicate symbols applied to variables, we similarly have: holds M′ v (P(x1, . . . , xn)) = M(termval M′ v x1, . . . , termval M′ v xn)) = M(v(x1), . . . , v(xn)) = PM(v(x1), . . . , v(xn)) = PM(v(x1), . . . , v(xn)) = PM(termval M v x1, . . . , termval M v xn) = holds M v (P(x1, . . . , xn)). It now follows by induction on the structure of P that we can extend the basic result to the whole formula (which is quantifier-free by hypothesis): holds M ′ v P = holds M v P However, since M is a model of P, the RHS is simply ‘true’, and therefore so is the left.

But v was arbitrary, and therefore the theorem is proved. Brand’s ‘E-modification’ applies the flattening transformation to clauses, adding new negative literals ¬(t = wi) for the extra variable definitions included. It follows that if we perform E-modification and then S- and T- modifications, the resulting set of clauses plus the reflexive law x = x has a model iffthe original formula has a normal model. We have thus succeeded in transforming the input clauses to eliminate the need for any equality axioms besides reflexivity.

Implementation First we define functions to identify non-variables: let is_nonvar = function (Var x) -> false | _ -> true;; and hence find a nested non-variable subterm where possible: 4.8 Equality elimination let find_nestnonvar tm = match tm with Var x -> failwith “findnvsubt” | Fn(f,args) -> find is_nonvar args;; Now we can identify a non-variable subterm that we want to pull out in flattening; in the case of equality this is a nested non-variable subterm, while for the other predicate symbols it is any non-variable subterm: let rec find_nvsubterm fm = match fm with Atom(R(“=”,[s;t])) -> tryfind find_nestnonvar [s;t] | Atom(R(p,args)) -> find is_nonvar args | Not p -> find_nvsubterm p;; Having found such a non-variable subterm, we want to replace it with a new variable.

The sheer complexity of computer systems has meant that automated rea- soning, i.e. the use of computers to perform logical inference, has become a vital component of program construction and of programming language design. This book meets the demand for a self-contained and broad-based account of the concepts, the machinery and the use of automated reasoning. The mathematical logic foundations are described in conjunction with their practical application, all with the minimum of prerequisites.

The approach is constructive, concrete and algorithmic: a key feature is that methods are described with reference to actual implementations (for which code is supplied) that readers can use, modify and experiment with. This book is ideally suited for those seeking a one-stop source for the gen- eral area of automated reasoning. It can be used as a reference, or as a place to learn the fundamentals, either in conjunction with advanced courses or for self study.

John Harrison is a Principal Engineer at Intel Corporation in Portland, Oregon. He specialises in formal verification, automated theorem proving, floating-point arithmetic and mathematical algorithms. HANDBOOK OF PRACTICAL LOGIC AND AUTOMATED REASONING JOHN HARRISON CAMBRIDGE UNIVERSITY PRESS Cambridge, New York, Melbourne, Madrid, Cape Town, Singapore, São Paulo Cambridge University Press The Edinburgh Building, Cambridge CB2 8RU, UK First published in print format ISBN-13 978-0-521-89957-4 ISBN-13 978-0-511-50865-3 © J. Harrison 2009 2009 Information on this title: www.cambridge.org/9780521899574 This publication is in copyright.

Subject to statutory exception and to the provision of relevant collective licensing agreements, no reproduction of any part may take place without the written permission of Cambridge University Press. Cambridge University Press has no responsibility for the persistence or accuracy of urls for external or third-party internet websites referred to in this publication, and does not guarantee that any content on such websites is, or will remain, accurate or appropriate. Published in the United States of America by Cambridge University Press, New York www.cambridge.org eBook (NetLibrary) hardback To Porosusha When a man Reasoneth, hee does nothing else but conceive a summe totall, from Addition of parcels.

For as Arithmeticians teach to adde and substract in numbers; so the Geome- tricians teach the same in lines, figures (solid and superficiall,) angles, proportions, times, degrees of swiftnesse, force, power, and the like; The Logicians teach the same in Consequences of words; adding together two Names, to make an Affirma- tion; and two Affirmations, to make a Syllogisme; and many Syllogismes to make a Demonstration; and from the summe, or Conclusion of a Syllogisme, they substract one Proposition, to finde the other.

For REASON, in this sense, is nothing but Reckoning (that is, Adding and Sub- stracting) of the Consequences of generall names agreed upon, for the marking and signifying of our thoughts.

This is a short excerpt from the opening of “” by Unknown, quoted for review and introduction purposes. All rights belong to the copyright holders.

Book Information

• Unique ID: 4ab37929c895d360
• File Extension: .pdf
• File Size: 3,129,948 bytes (2.985 MB)
• Title: –
• Author: Unknown
• ISBN: 9780521899574, 9780511508653
• Pages: 704
• Language: English (en)

Reading & Word Statistics

• Estimated Reading Time: 1326.57 minutes
• Total Words: 265,314
• Total Characters: 1,509,459
• Average Words per Page: 376.87
• Average Characters per Page: 2144.12

Most Frequent Words

let (1510), formula (991), set (776), one (754), function (697), theorem (678), logic (675), imp (627), true (612), proof (600), since (518), formulas (504), forall (485), false (464), example (434), form (432), using (426), list (404), holds (403), also (395), first (365), use (354), two (347), term (342), variables (340), clauses (335), exists (330), see (325), fun (324), case (320), following (312), theory (311), however (302), now (301), model (296), propositional (295), terms (288), int (280), functions (278), need (274), used (273), even (273), vars (266), atom (261), first-order (257), resolution (257), clause (255), variable (254), new (250), match (249), var (245), result (243), given (241), note (240), rules (239), axiom (233), equality (232), general (232), many (229), procedure (226), map (225), problem (223), finite (223), rule (221), number (219), consider (218), axioms (216), order (213), string (213), problems (212), equivalent (212), prove (205), rec (204), computer (203), subst (201), language (195), add (194), like (193), show (190), relation (190), logical (188), numbers (187), quantifier (185), proving (182), print (179), ocaml (179), way (176), section (176), fact (175), polynomial (173), often (172), rather (171), define (171), equations (169), mathematical (167), elimination (161), it’s (159), literals (159), right (158), instances (158).

PDF Download