DECIDABILITY AND HERBRAND’S UNIVERSE

Get Complete Project Material File(s) Now! »

Introduction to Mathematical Set Theory

Set theory is a foundational theory of mathematics in the sense that many mathematical theorems, including arithmetic and Euclid’s geometry, can be formulated as theorems of set theory (Nerode & Shore 1997). The problem of finding the truth of a mathematical statement can therefore be reduced to a problem of showing that its truth can be derived from the axioms of set theory (Enderton 1977). In this chapter we give an overview of the Zermelo-Fraenkel (ZF) axiomatisation of set theory that allows for the first-order logic representation of set-theoretic problems. In the next section we discuss the use of set theory in formal specification languages.

Zermelo-Fraenkel Set Theory

The concept of a set has been used in mathematic writings since ancient times (Enderton 1977). George Cantor’s work at the end of the 19th century put set theory on a proper mathematical basis with a series of papers published during the period from 1874 to 1897. He is generally regarded as the father of set theory (Enderton 1977). This early set theory originated in a non-axiomatic form that relied on an informal understanding of sets as collections of objects. By the turn of the nineteenth century a number of paradoxes were discovered in set theory. One of these is Russell’s paradox that was discovered in 1901 by Bertrand Russell (Enderton 1977, Potter et al. 1996).

At the heart of automated theorem proving lies the “decision problem” (Leitsch 1997). It is the challenge in symbolic logic to find a general algorithm which decides for any firstorder statement whether it is universally valid or not. As early as the 17th century, Leibniz had the vision of building a machine that would solve this problem. The problem was revived in the early 20th century by Hilbert who posed it as one of several problems to the mathematical community. He called the decision problem the “fundamental problem of mathematical logic” (Leitsch 1997 p. 212). Progress was made in the following years by several mathematicians who found decidable subclasses of predicate logic.

Clausal Form

Many computer implementations of first-order logic use the clausal form to represent formulas (Quaife 1992b), which is an apparently quantifier-free conjunctive normal form. This form was introduced by Davis and Putnam (1960). Formulas are therefore represented by a more restricted syntax-type that enables more efficient inference rules to be defined and makes it easier to control proof search. The clausal form of a formula is not necessarily logically equivalent to the original formula. However, the clausal form has the important property that it is unsatisfiable if and only if the original formula is unsatisfiable (Hamilton 1991).

READ Polarization of the fields and atomic angular momentum in EIT

Tautologies

A tautology is a clause that is valid under all interpretations. A clause is a disjunction of literals therefore a clause is a tautology if and only if it is true or if it contains a complementary pair of literals (Leitsch 1997). The clause P(f(x)) ∨ Q(y) ∨ ¬P(f(x)) is an example of a tautology. This is because either P(f(x)) or its complement will be valid regardless of the interpretation that is used. The tautology rule states that a clause D that is a tautology can be removed from a clause set S resulting in set S – {D}. Since D is satisfied by all interpretations it follows that an interpretation satisfies S if and only if it satisfies S – {D} (Eisinger & Ohlbach 1993).

Contents :

1 INTRODUCTION
- 1.1 MOTIVATION
- 1.2 RESEARCH QUESTION
- 1.3 HYPOTHESIS
- 1.4 APPROACH
- 1.5 DISSERTATION LAYOUT
2 INTRODUCTION TO MATHEMATICAL SET THEORY
- 2.1 ZERMELO-FRAENKEL SET THEORY
  - 2.1.1 Extensionality Axiom
  - 2.1.2 Empty set Axiom
  - 2.1.3 Pairing Axiom
  - 2.1.4 Union Axiom
  - 2.1.5 Subset Axiom
  - 2.1.6 Power set Axiom
  - 2.1.7 Infinity Axiom
  - 2.1.8 Axiom of replacement
  - 2.1.9 Axiom of foundation or regularity
  - 2.1.10 Axiom of choice
  - 2.1.11 Example
- 2.2 LIMITATIONS OF ZF AXIOMS IN AUTOMATED THEOREM PROVING
- 2.3 SUMMARY
3 RESOLUTION
- 3.1 DECIDABILITY AND HERBRAND’S UNIVERSE
- 3.2 RESOLUTION
- 3 RESOLUTION
- 3.1 DECIDABILITY AND HERBRAND’S UNIVERSE
  - 3.2 RESOLUTION
  - 3.2.1 Clausal Form
  - 3.2.2 Resolution in Propositional Logic
  - 3.2.3 Resolution in First-order Predicate Logic
- 3.3 EFFICIENCY ENHANCEMENTS
- 3.4 REFINEMENTS
4 AUTOMATED THEOREM PROVERS
- 4.1 VAMPIRE
- 4.2 GANDALF
- 4.3 SUMMARY
5 EVALUATION OF SET-THEORETIC REASONING HEURISTICS
- 5.1 EQUALITY VERSUS EXTENSIONALITY
- 5.2 NESTED FUNCTORS
- 5.3 DIVIDE-AND-CONQUER
- 5.4 EXEMPLIFICATION
- 5.5 MULTIVARIATE FUNCTORS
- 5.6 INTERMEDIATE STRUCTURE
- 5.7 ELEMENT STRUCTURE
- 5.8 REDUNDANT INFORMATION
- 5.9 SEARCH-GUIDING
- 5.10 RESONANCE
6 AN ORDER MANAGEMENT SYSTEM IN Z
- 6.1 PROBLEM STATEMENT
- 6.2 CONCEPTUAL MODEL
- 6.3 THE Z SPECIFICATION LANGUAGE
- 6.4 SPECIFYING CLASSES AND THEIR ATTRIBUTES
- 6.5 SPECIFYING ASSOCIATIONS
7 DISCHARGING CASE STUDY PROOF OBLIGATIONS
- 7.1 CONVERSION OF Z TO FIRST-ORDER LOGIC
- 7.2 DISCHARGING OF PROOF OBLIGATIONS
8 SUMMARY AND CONCLUSIONS
- 8.1 CONTRIBUTIONS OF THIS DISSERTATION
- 8.2 FUTURE WORK
APPENDIX A – RESOLUTION DEDUCTIONS OF THE FARMER, WOLF, GOAT AND CABBAGE (FWGC) PUZZLE
- A.1 A POSSIBLE REFUTATION DEDUCTION OF THE FWGC PUZZLE
- A.2 LEVEL SATURATION METHOD DEDUCTION OF FWGC PUZZLE
- A.3 UR-RESOLUTION DEDUCTION OF FWGC PUZZLE
- A.4 ILLUSTRATION OF SET-OF-SUPPORT STRATEGY OF FWGC PUZZLE
- A.5 SET-OF-SUPPORT STRATEGY WITH PREDICATE ORDERING
- A.6 SET-OF-SUPPORT STRATEGY WITH SUBSUMPTION
APPENDIX B – THEOREM PROVERS EVALUATED
APPENDIX C – SAMPLE REASONER OUTPUT
- C.1 VAMPIRE
- C.2 GANDALF
APPENDIX D – Z CASE STUDY OF ORDER PROCESSING SYSTEM
- D.1 GIVEN SETS (BASIC TYPES)
- D.2 PRODUCT
- D.3 ORDER
- D.4 ITEM
- D.5 CUSTOMER