How predicate calculus is used in computing
Joshua Mendel
As defined by Wikipedia, predicate calculus, also known as first order logic, is a collection of formal systems used in mathematics and computer science. [1] Predicate calculus has had a considerable impact on computer science in the world of artificial intelligence, such as with the creation of Prolog, a logic programming language mainly used for natural language processing in AI. [2] Since the advent of AI, there have been many attempts by computer scientists to write programs that could prove theorems automatically. All attempts failed because there seemed to be no way of deriving new theorems. Then, in 1965, the resolution method was discovered. J. A Robinson described a technique which he termed the ‘ resolution method ’ , [3] which changed everything. Resolution, which uses predicate calculus, allows new theorems to be derived and can be used to prove formulas by showing that the negation of the formula cannot be satisfied. Predicate calculus uses symbols to denote different parts of axioms. Uppercase letters symbolize predicates, whereas lowercase letters symbolize functions and variables. ∧ (conjunction), ∨ (disjunction), → , ⇔ , ¬, represent AND, OR, IMPLICATION, BICONDITIONAL, NEGATION, respectively. Two extra symbols, which make predicate calculus different to propositional logic, are the ∃ and ∀ symbols, which are the existential and universal quantifiers respectively. A predicate calculus formula is defined recursively as shown below: [1]
1.
An atomic formula is a formula.
2.
If β is a formula, then ¬( β ) is a formula.
3. If φ and ψ are formulas, then ( φ ∧ ψ ) is a formula, along with ( φ ∨ ψ ) and ( φ → ψ ). Similar rules apply for other connectives. 4. If β is a formula, and α is a variable, then ∀ αβ and ∃ αβ are also formulas.
An atomic formula is a formula that contains no binary logic connectives ( ∧ , ∨ etc.). ∀ αβ and ∃ αβ are equivalent to: (for all α , β is true) and (there exists α such that β is true) respectively. Parentheses are also often used in formulas to ensure readability, but there is no strict convention of where to use them, so it is often left to the author to decide where to place them. In light of this, a common convention was created to show the order of operations involving logical operators. This means that parentheses may be excluded in some cases. The convention is as follows: [1]
¬ is evaluated first
•
∧ and ∨ are then evaluated
•
Quantifiers are evaluated next
•
→ is evaluated last
•
I will be following this convention throughout.
226
Made with FlippingBook - Online catalogs