# Logic in Computer Science : Modelling and Reasoning about by Michael Huth

By Michael Huth

The second one version of this winning textbook maintains to supply a transparent advent to formal reasoning suitable to the wishes of contemporary machine technology and sufficiently exacting for functional functions. advancements were made all through with many new and elevated textual content sections. The assurance of model-checking has been considerably up to date and extra routines are incorporated. net help comprises labored recommendations for instructor routines and version ideas to a couple scholar routines. First version Hb (2000): 0-521-65200-6 First variation Pb (2000): 0-521-65602-8

Similar microprocessors & system design books

Designing Embedded Systems with PIC Microcontrollers: Principles and Applications

This e-book is a hands-on creation to the foundations and perform of embedded method layout utilizing the PIC microcontroller. full of beneficial examples and illustrations, it provides an in-depth therapy of microcontroller layout, programming in either meeting language and C, and lines complicated subject matters resembling networking and real-time working platforms.

Logic and Language Models for Computer Science

This article makes in-depth explorations of a wide variety of theoretical issues in desktop technological know-how. It plunges into the purposes of the summary ideas for you to confront and deal with the skepticism of readers, and instill in them an appreciation for the usefulness of concept. A two-part presentation integrates good judgment and formal language—both with functions.

Extra resources for Logic in Computer Science : Modelling and Reasoning about Systems

Example text

I. 21 We put these rules in action, demonstrating that the sequent p → q, p → ¬q ¬p is valid: 1 p→q premise 2 p → ¬q premise 3 p assumption 4 q →e 1, 3 5 ¬q →e 2, 3 6 ⊥ ¬e 4, 5 7 ¬p ¬i 3−6 Lines 3–6 contain all the work of the ¬i rule. 2 Derived rules When describing the proof rule modus tollens (MT), we mentioned that it is not a primitive rule of natural deduction, but can be derived from some of the other rules. Here is the derivation of φ → ψ ¬ψ ¬φ MT 1 Propositional logic 24 from →e, ¬e and ¬i: 1 φ→ψ premise 2 ¬ψ premise 3 φ assumption 4 ψ →e 1, 3 5 ⊥ ¬e 4, 2 6 ¬φ ¬i 3−5 We could now go back through the proofs in this chapter and replace applications of MT by this combination of →e, ¬e and ¬i.

18 From boolean algebra, or circuit theory, you may know that disjunctions distribute over conjunctions. We are now able to prove this in natural deduction. The following proof: 1 p ∧ (q ∨ r) premise 2 p ∧e1 1 3 q∨r ∧e2 1 4 q assumption 5 p∧q ∧i 2, 4 6 (p ∧ q) ∨ (p ∧ r) ∨i1 5 7 r assumption 8 p∧r ∧i 2, 7 9 (p ∧ q) ∨ (p ∧ r) ∨i2 8 10 (p ∧ q) ∨ (p ∧ r) ∨e 3, 4−6, 7−9 veriﬁes the validity of the sequent p ∧ (q ∨ r) (p ∧ q) ∨ (p ∧ r) and you are encouraged to show the validity of the ‘converse’ (p ∧ q) ∨ (p ∧ r) p ∧ (q ∨ r) yourself.

N ψ is valid. Do we have any evidence that these rules are all correct in the sense that valid sequents all ‘preserve truth’ computed by our truth-table semantics? Given a proof of φ1 , φ2 , . . , φn ψ, is it conceivable that there is a valuation in which ψ above is false although all propositions φ1 , φ2 , . . , φn are true? Fortunately, this is not the case and in this subsection we demonstrate why this is so. Let us suppose that some proof in our natural deduction calculus has established that the sequent φ1 , φ2 , .