By Edmund Burke and Eric Foxley

Departments of Computer Science and Mathematics, University of Nottingham

For more details Click here to send E-mail to Edmund Burke.

Chapter 1: Propositional Calculus

• Informal introduction
• Logical connectives
• Negation (not)
• Conjunction (and)
• Disjunction (or)
• Implication
• Equivalence
• Sum and product notations
• Priorities of operators
• Truth-tables of formulae
• How to construct the truth-table of a formula
• Identical truth-tables
• Interpretations and models
• Tautologies, absurdities and mixed formulae
• Two rules concerning the truth-values of formulae
• Other logical connectives
• Truth functions
• Monadic operators
• Dyadic operators
• Triadic operators
• Representing truth functions in terms of dyadic and monadic operators
• Manipulating propositional formulae
• Standard identities
• Complete sets of connectives
• Other complete sets of connectives
• Sheffer functions
• Normal forms
• The negation of propositional formulae
• Definition
• Generalised De Morgan's law
• Extended disjunction and conjunction
• Duality
• Arguments and argument forms
• Some definitions associated with formulae
• Some rules for WFFs
• The validity of an argument
• Mathematical if-and-only-if proofs
• A theorem
• Another theorem
• Summary
• Worked examples
• Exercises

Chapter 2: Formal Approach to Propositional Logic

• Introduction
• Formal systems of propositional logic
• Proofs and deductions
• Constructing formal systems
• The relationship between formal systems and interpretations
• The formal propositional logic system L
• The construction of system L
• Proofs in system L
• Deductions in system L
• Derived rules of inference in system L
• Examples
• Notation for rules
• The soundness and completeness theorems for system L
• Introduction
• The soundness theorem for system L
• The completeness theorem for system L
• Independence of axioms and rules
• Lemmon's system of propositional logic
• An introduction to the system
• Proofs and deductions in Lemmon's system
• Examples of deductions in Lemmon's system
• Summary
• Worked examples
• Exercises

Chapter 3: Applications to Logic Design

• Introduction
• Simplification techniques
• A simple example
• Karnaugh maps
• Quine-McClusky minimisation
• Definition
• A few 4-variable universal decision elements
• Logic design
• Binary arithmetic adders
• Sequential logic
• Summary
• Worked examples
• Exercises

Chapter 4: Predicate Logi

• Informal introduction
• Background
• Universal and existential quantifiers
• Translating between first order languages and the English language
• Hints for translating from English to Logic
• Examples
• Summary
• Exercises
• The semantics of predicate logic
• First order languages
• Interpretations
• Satisfaction
• Truth-tables of interpretations
• Herbrand interpretations
• Summary
• Worked examples
• Exercises
• Syntactical systems of Predicate Logic
• The system K of predicate logic
• Discussion of the system K
• First Order Theories
• Summary
• Worked example
• Exercises
• Soundness and Completeness
• Introduction
• The soundness of system K
• Consistency
• The completeness of system K
• Summary
• Worked examples
• Exercises

Chapter 5: Logic Programming

• Introduction
• Programming with propositional logic
• Definitions for propositional logic
• Propositional resolution
• Refutation and deductions
• Negation in logic programming
• SLD-resolution
• Clausal form for predicate logic
• Prenex form
• Clausal form
• Horn clauses
• The semantics of logic programming
• Horn clauses and their Herbrand models
• Logic programs and their Herbrand models
• Least Herbrand models
• Construction of least Herbrand models
• Unification and answer substitutions
• Substitutions
• Unification
• Practicalities
• Programming with predicate logic
• The resolution rule
• The proof strategy of Prolog: SLD-resolution
• Negation in logic programming: The closed world assumption
• Concluding remarks
• Worked examples
• Exercises

Chapter 6 : Formal System Specification

• Introduction
• A simple example
• A state schema
• Operations or events and their schema
• Pre- and post- conditions
• Notational Differences
• The Z specification language
• Basic type definitions
• Free type definitions
• Schema inclusion
• Schema types
• Example - A computer file system
• Axiom schema
• Schema algebra
• Linear notation
• Schema extension
• Some other types of definition
• Schema inclusion
• The TUPLE and PRED operators
• Ornamentation of schema names
• Logical operations on schema
• Schema quantification
• Identifier renaming
• Identifier hiding
• Schema pre-condition
• Schema composition
• Schema piping
• Axiomatic descriptions
• Summary
• Worked examples
• Some simple examples
• Case study: A car ferry terminal
• Exercises

Appendix A : Mathematical Background

• Induction proofs
• Set theory
• Comprehensive specification of a set
• Operations involving sets
• Bags
• Relations
• Domain and range
• Composition
• Domain and range operations
• Override operation
• Set image
• Equivalence relations
• Functions
• Sequences

Appendix B : Alternative notations

• Alternative notations
• Polish notation
• Worked examples
• Exercises

Appendix C : Symbols used in the text

• Truth values
• Logical operators
• Metasymbols
• Substitutions
• Formal specification using Z

Index