First-Order Logic in Python

This tutorial is an introduction to first-order logic in Python. I am going to show you how to create a knowledge base, how to make inferences with forward chaining and how to make inferences with backward chaining.

First-order logic (FOL) is a language with objects, functions, variables and symbols. FOL is used to represent knowledge and to make inference from knowledge. You can add sentences (facts and rules) to a knowledge base and then ask questions to the knowledge base. The connection symbols used in first-order logic is listed below.

Symbol	Code	Example	Explanation
¬	~	~Has(Letter)	Negation, is not or does not exist
^	&	A & B	And, both terms must be true
∨	|	A | B	Or, one of the terms must be true
⇒	==>	Connected(x,y) ==> Connected(y,x)	Implies, if the first term is true then the second term is true
⇔	<=>	C <=> D	Equivalence, if and only if. C is true if and only if D is true.

A first-order logic knowledge base can only contain definite clauses. A definite clause is a clause with at most one positive literal, you can use parentheses to ensure that your clauses are definite.

I am using code from aima-python in this tutorial (download package), these modules include all the necessary classes and functions for first-order logic in python. The knowledge base is created from the following sentence: The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missiles were sold to it by Colonel West, who is American.

Backward Chaining

A backward chaining algorithm starts from the goal and chains through rules to find facts that support the goal. This backward algorithm will only find the first fact that supports the goal, even if it exists multiple answers in the knowledge base.

# Import libraries
import aima.utils
import aima.logic

# The main entry point for this module
def main():

    # Create an array to hold clauses
    clauses = []

    # Add first-order logic clauses (rules and fact)
    clauses.append(aima.utils.expr("(American(x) & Weapon(y) & Sells(x, y, z) & Hostile(z)) ==> Criminal(x)"))
    clauses.append(aima.utils.expr("Enemy(Nono, America)"))
    clauses.append(aima.utils.expr("Owns(Nono, M1)"))
    clauses.append(aima.utils.expr("Missile(M1)"))
    clauses.append(aima.utils.expr("(Missile(x) & Owns(Nono, x)) ==> Sells(West, x, Nono)"))
    clauses.append(aima.utils.expr("American(West)"))
    clauses.append(aima.utils.expr("Missile(x) ==> Weapon(x)"))

    # Create a first-order logic knowledge base (KB) with clauses
    KB = aima.logic.FolKB(clauses)

    # Add rules and facts with tell
    KB.tell(aima.utils.expr('Enemy(Coco, America)'))
    KB.tell(aima.utils.expr('Enemy(Jojo, America)'))
    KB.tell(aima.utils.expr("Enemy(x, America) ==> Hostile(x)"))

    # Get information from the knowledge base with ask
    hostile = KB.ask(aima.utils.expr('Hostile(x)'))
    criminal = KB.ask(aima.utils.expr('Criminal(x)'))

    # Print answers
    print('Hostile?')
    print(hostile)
    print('\nCriminal?')
    print(criminal)
    print()

# Tell python to run main method
if __name__ == "__main__": main()

Hostile?
{v_5: Nono, x: Nono}

Criminal?
{v_9: West, x: West, v_20: M1, v_10: M1, v_27: M1, v_11: Nono, v_39: Nono}

Forward Chaining

A forward chaining algorithm looks at each rule in the knowledge base to see if the goal can be satisfied. This algorithm uses unification to form new sentences, new sentences are added to the knowledge base and this process is repeated until the question can be answered or until no more sentences can be added. A query can have multiple answers with forward chaining.

# Import libraries
import aima.utils
import aima.logic

# The main entry point for this module
def main():

    # Create an array to hold clauses
    clauses = []

    # Add first-order logic clauses (rules and fact)
    clauses.append(aima.utils.expr("(American(x) & Weapon(y) & Sells(x, y, z) & Hostile(z)) ==> Criminal(x)"))
    clauses.append(aima.utils.expr("Enemy(Nono, America)"))
    clauses.append(aima.utils.expr("Owns(Nono, M1)"))
    clauses.append(aima.utils.expr("Missile(M1)"))
    clauses.append(aima.utils.expr("(Missile(x) & Owns(Nono, x)) ==> Sells(West, x, Nono)"))
    clauses.append(aima.utils.expr("American(West)"))
    clauses.append(aima.utils.expr("Missile(x) ==> Weapon(x)"))

    # Create a first-order logic knowledge base (KB) with clauses
    KB = aima.logic.FolKB(clauses)

    # Add rules and facts with tell
    KB.tell(aima.utils.expr('Enemy(Coco, America)'))
    KB.tell(aima.utils.expr('Enemy(Jojo, America)'))
    KB.tell(aima.utils.expr("Enemy(x, America) ==> Hostile(x)"))

    # Get information from the knowledge base with ask
    hostile = aima.logic.fol_fc_ask(KB, aima.utils.expr('Hostile(x)'))
    criminal = aima.logic.fol_fc_ask(KB, aima.utils.expr('Criminal(x)'))

    # Print answers
    print('Hostile?')
    print(list(hostile))
    print('\nCriminal?')
    print(list(criminal))
    print()

# Tell python to run main method
if __name__ == "__main__": main()

Hostile?
[{x: Coco}, {x: Nono}, {x: Jojo}]

Criminal?
[{x: West}]