tailieunhanh - Lecture Formal methods in software engineering: Propositional logic

Lecture Formal methods in software engineering: Propositional logic. After studying this chapter you will be able to understand: Propositional logic, atomic propositions, connectives, truth tables, precedence, inference rules, arguments, presentation, transitivity,. | Using Z 2–1 Propositional logic Using Z Jim Davies & Jim Woodcock Using Z 2–2 Propositional logic • deals with propositions: statements that must be either true or false • propositions may be combined using logical connectives • the meaning of a combination is determined by the meanings of the propositions involved Using Z 2–3 Atomic propositions Atomic propositions are statements without logical connectives. In our language, an atomic proposition will state either • that an object is a member of a set, or • that it is equal to another object. We will see how to formalise these statements later. Using Z 2–4 Examples • jaffa cakes are biscuits • your cat is rich • your dog is good looking • 2+2=5 • tomorrow = tuesday Using Z 2–5 Connectives ¬ negation (not) ∧ conjunction (and) ∨ disjunction (or) ⇒ implication (implies or only if) a equivalence (iff or if and only .