First-Order Logic in Artificial Intelligence

Notations of First-Order Logic

Let’s discuss the syntax and notations of First-Order Logic.

Predicates

Predicates are symbols that represent the attributes or connections of things. They are used to construct assertions about things and their properties. For instance, "human(x)" may be a predicate indicating that "x is a human."

Variables

Variables are placeholders in logical statements that allow us to refer to undefined objects. They help in the creation of general statements that may be applied to any object. In the predicate "human(x)," for example, "x" is a variable that represents any human.

Constants 

In First-Order Logic (FOL), a constant is a unique name of a certain item. It is like providing a label for the item in the logical statements.

Notation: Constants are represented using lowercase letters, numerals, or other symbols. For example: "x," "y," "z," "1," "2," etc.

Let’s say x is a constant, and Human(x) is the statement. So, in this, we are using the constant x to represent Humans.

Quantifiers

Quantifiers, namely universal () and existential (), allow us to make general statements about groups of items. The universal quantifier () means that a statement applies to all objects in the particular domain, whereas the existential quantifier denotes that there is at least one item in the particular domain.

Logical Connectives

Logical connectives are basic symbols in logic that are used to combine or transform simple statements to produce more sophisticated logical expressions. These connectives enable us to think about the links between propositions and serve as the foundation for logical arguments and expressions. 

The following are examples of popular logical connectives:

1. AND (^): Denotes a conjunction. 

It is represented by the symbol "^" and is only true when both declarations connected by it are true. 

As an example:

Statement 1: "The weather is nice today."

Statement 2: "I'm going to see a movie."

"I'll go to the movies today ^ the weather is nice." is the Logical Expression

Only if both declarations 1 and 2 are true will the expression be true.

2. OR (∨): Denotes disjunction.

It is represented by the symbol "∨" and is true if at least one of the connected statements is true. 

As an example:

Statement 1: "Stop" 

Statement 2: "I will shoot"

 "Stop ∨ I will shoot" is the Logical Expression

If either statement 1 or statement 2 (or both) is true, the expression is true.
 

3. NOT (¬): Denotes negation. It is represented by the symbol "¬" and reverses a proposition's truth value. As an example:

Statement: "The sky is blue"

"¬The sky is blue." is the Logical Expression

If the sky is not blue, the term is correct.
 

4. IMPLIES (→):  This symbol represents implication. It represents a conditional connection between two propositions and is symbolised by the symbol "→". As an example:

Statement 1: "If I study hard, I will get good grades."

Statement 2: "I studied very hard for the exam."

          "If I study hard → I will get good grades" is the Logical Expression

Quantifiers in First-Order Logic

In First-Order Logic, quantifiers allow us to discuss collections of objects, qualities, or relationships as a group. They help us in expressing our thoughts on whether particular statements apply to all members of a group or apply to particular members that fit a specified requirement.

Assume you're discussing a large group of items, such as all the animals at a zoo or all the students in a class. In First-Order Logic, quantifiers help you talk about these groupings.

Universal Quantifier (∀): 

The Universal Quantifier is a logic concept that allows you to make statements about each and every individual member in a group. It's equivalent to stating "for all" or "for every". It states a condition that holds true for every member of a set or collection in mathematical and logical terms.

Statement: "In every classroom, all students have notebooks."

Meaning: This statement conveys that within every classroom, each and every student has a notebook.

Existential Quantifier (∃):

The Existential Quantifier (∃) is a key idea in logic that allows you to say that at least one member in a group or domain meets a certain condition. In other words, it's the same as stating "there is" or "there exists" in daily speech. It states the presence of at least one member who fits a specific requirement in logical terms.

For Example, "There is a garden in the neighbourhood with colourful flowers."

Consider a neighbourhood that has a variety of gardens. When we apply the Existential Quantifier (∃), we mean that among all of these gardens, at least one stands out because of its gorgeous flowers. We may not know which garden it is, but we are certain that it exists.

Rules of Inference in First-Order Logic

Let’s discuss the rules that are to be followed in First-Order Logic:

1. Modus Ponens 

If you have a statement, "P implies Q" (P → Q), and you also know that "P" is true, then you can correctly conclude that "Q" is true.
Example: 

Given: If it's raining (P), then I'll take an umbrella (Q).

Statement 1: It's raining (P).

Conclusion: I'll take an umbrella (Q).

2. Modus Tollens  

If you have a statement "P implies Q", and you also know that "Q" is not true (¬Q), then you can infer that "P" is not true (¬P).
Example:

Given: If I study hard (P), then I'll pass the exam (Q).

Given: I didn't pass the exam (¬Q).

Conclusion: I didn't study hard (¬P).

3. Universal Instantiation 

If you have a statement that says something is true for all instances, like "For all x, P(x)," and you have a specific individual "a," you can conclude that "P(a)" is true.
Example:

Given: All dogs (∀x Dog(x)) bark (P(x)).

Conclusion: Fido barks (Dog(Fido) → Bark(Fido)).

4. Universal Generalization  

If you have a statement that's true for a specific individual "a," like "P(a)," you can generalise it to say that it's true for all instances, or "For all x, P(x)."
Example:

Statement: "Riya aced the Science test."

Conclusion: "All students as good as Riya aced the Science test."

Explanation: Starting with the Statement that "Riya aced the Science test," we can apply Universal Generalization to make a broader statement. The conclusion "All students as good as Riya aced the Science test" depicts that any student who possesses the same level of skill as Riya also aced the Science test. This demonstrates how Universal Generalization allows us to generalise from a specific case to a more general statement that applies to a group with similar attributes.

5. Existential Instantiation

If you have a statement that says something exists, like "There exists an x such that P(x)," and you introduce a new variable "a," you can conclude that "P(a)" is true.
Example:

Given Statement: "At least one student in the class speaks German.”

Inference: "Jerry is a student in the class who speaks German."

The initial statement indicates that there's a student in the class who knows how to speak German. Applying Existential Instantiation, we can pinpoint a specific individual, Jerry, who fulfils this condition. This showcases how Existential Instantiation helps us identify particular instances that satisfy the requirement mentioned in the given statement.

6. Existential Generalisation 

If you have a statement that's true for a specific individual "a," like "P(a)," you can generalise it to say that something exists for all instances, or "There exists an x such that P(x)."
Example:

Given Statement: "One student scored the highest marks in the exam."

Statement: "There exists a student who scored the highest marks in the exam."

Explanation: Let's say there are 20 students in the class. The given statement asserts that among these 20 students, there's at least one who achieved the highest marks. 

By using Existential Generalisation, we can conclude that out of the entire group of students, there exists at least one student who indeed secured the top marks in the exam.

Unification in First-Order Logic

Unification in First-Order Logic deals with finding a common substitution for variables in different terms to make them match. The goal of unification is to make two expressions identical by assigning values to variables in a way that preserves their meanings. It involves substituting terms for variables in a way that the resulting expressions match.

Conditions for Unification

1. The predicate symbol must be the same.
2. The number of arguments in both expressions must be identical.
3. If two similar variables are present in the same expression, then unification fails.

Pseudocode of Unification

function unify(expression1, expression2):
	if expression1 is the same as expression2:
		return "SUCCESS" 
		
	if expression1 is a variable: 
		return substitute(expression1, expression2) 
		
	if expression2 is a variable: 
		return substitute(expression2, expression1) 
		
	if both expressions are terms and not equal:
		return "FAILURE" 
		
	if both expressions are functions or predicates with matching name and arity: 
		for each corresponding argument (arg1, arg2): 
			result <- unify(arg1, arg2) 
		
		if result is "FAILURE": 
			return "FAILURE"
		
	return "SUCCESS"
		
 function substitute(variable, expression): 
 	if variable occurs in expression: 
 		return "FAILURE" 
	else: 
 		return {variable / expression}

Explanation: The provided pseudocode describes the process of unification in First-Order Logic using simplified code. It checks for identical expressions, handles cases involving variables, terms, functions, and predicates, and ensures consistency in variable substitutions. The substitute function handles variable replacements and checks for valid substitutions.

Example of Unification in First-Order Logic

Consider the following phrases, which must be unified:

"Eats(x, Apple)" is an expression.

"Eats(Riya, y)" is an expression.

The following is an explanation of the unification process:

Comparison

Expression A ("Eats(x, Apple)") is compared to Expression B ("Eats(Riya, y)"

Substitution Variable

We can see that Expression A's first parameter is a variable "x," and the second argument is a constant "Apple."

The first parameter in Expression B is a constant "Riya," while the second argument is a variable "y."

Unifying Variables

We unify the variable "x" in Expression A with "Riya" in Expression B. This results in the substitution: x = Riya.

We also unify the variable "y" in Expression B with the constant "Apple." This gives us the substitution: y = Apple.

Applying Substitutions

After substitutions, Expression A becomes "Eats(Riya, Apple)."

Expression B remains the same: "Eats(Riya, Apple)."

Unified Expression

Both expressions are now identical: "Eats(John, Apple)."

Unification is successful, and the unified expression is "Eats(Riya, Apple)."

Resolution in First-Order-Logic

In First-Order Logic (FOL), resolution is a fundamental inference method for theorem proving and logical reasoning. It's very beneficial for showing the truth of statements through contradiction. The resolution principle helps in the generation of new clauses from old ones, resulting in the resolution of difficult logical issues. 

Steps for Resolution

1. Conversion to Clausal Form: The statements in FOL are transformed into clausal form, where each statement becomes a collection of literals (positive or negated atomic formulas) joined together by logical disjunction (OR).
 

2. Application of Negation Normal Form (NNF): If necessary, statements are converted into Negation Normal Form, ensuring negations only relate to atomic formulas.
 

3. Resolution Process: Selection of Clause Pair: Two clauses are chosen for resolution. These clauses generally contain a pair of complementary literals (one positive, one negated).

Literal Resolution: Complementary literals are identified within the selected clauses.

Resolution Step: By merging the chosen clauses and removing the resolved literals, a new clause is created. This new clause is a disjunction of the remaining literals.
 

4. Iterative Iteration: The resolution rule is iteratively applied to yield new clauses. If an empty clause (contradiction) emerges, the original statements are shown to be inconsistent, thus substantiating the theorem.

Example of Resolution in First-Order-Logic

Consider the following situation with a family and their relationships. Based on the facts provided, we wish to prove that "John is Sarah's grandfather."

Given facts: 

John is Alice's father.

Sarah's mother is Alice.

Goal: Demonstrate that "John is Sarah's grandfather."

Steps to Resolve

Clausal Form Conversion:

Fact 1: "Father(John, Alice)" transforms into "Father(John, Alice) True.

Fact 2: "Mother(Alice, Sarah)" transforms into "Mother(Alice, Sarah) True.

Process of Resolution:

Choose "Father(John, Alice) True" and "Mother(Alice, Sarah) True."

Determine the complementary literals "Father(John, Alice)" and "Father(John, Alice)."

The resolved clause is "True True," which is shortened to "True."

Conclusion: 

The resolution method returns "True," indicating that the objective "John is the grandfather of Sarah" is correct based on the information provided. 

First-Order Logic VS Propositional Logic

Frequently Asked Questions

What is first-order logic in simple terms?

First-order logic (FOL) uses quantifiers like "forall" and "exists," along with predicates, to describe relationships between objects in a logical system.

What is first-order logic and modal logic?

First-order logic (FOL) uses quantifiers and predicates to describe relationships between objects. Modal logic extends FOL by adding modalities like necessity and possibility.

What is zero order logic in AI?

Zero-order logic, also known as propositional logic, deals only with simple true/false statements without using quantifiers or variables.

Conclusion

First-Order Logic (FOL) is like a language for computers to understand and talk about complex ideas. It's great because it lets us use variables, talk about groups of things, and say things about them. We can use it to solve puzzles, teach computers about the world, and make them smarter. While FOL can do a lot, it's also a bit tricky and can sometimes take a lot of computer power. But as we learn more, FOL keeps getting better and helps computers understand our world in smarter ways.

You can read these articles to learn more.

• Logic Propositional
• Propositional and First-Order Logic Part 1
• Propositional and First-Order Logic Part 2
• Propositional and First-Order Logic Part 3

You can also check out our other blogs on Code360.