Reasoning

This section provides several illustrative reasoning examples using the LNN. Each problem consists of the natural language description of the background knowledge and the query. The logical representations of the background knowledge and query follows in First-order Logic. Finally, code snippets showing the direct mapping to the LNN representation are provided. There are examples typically found in the theorem proving literature. The goal is to prove that the background knowledge entails the query.

The problems can be parsed into First-order Logic using any semantic parsing modules. The output of semantic parsing is facts and rules. We extract predicates , constants (or objects ) and logical connectives (→, ∀, etc.). Facts are made of predicates and constants . Here, we manually parse each text into FOL to illustrative theorem proving.

Simple Geometry reasoning example

The first example shows how to apply theorem proving, and LNN in particular, on a simple geometric example. The background knowledge contains some general rules about shapes of objects, and facts about some given objects. The goal is to prove geometrical properties of existing objects.

Problem in Natural Language

Background knowledge: All square objects are rectangular . All rectangular objects have four sides . The object c is a square . The object k is a square .

Query: Is there any object with four sides ?

We extract the following predicates: Square , Rectangle and Fourside ; and two objects (constants): c and k .

Problem in First-order Logic

Background knowledge

Square(c)

Square(k)

∀x Square(x) → Rectangle(x)

∀x Rectangle(x) → Fourside(x)

Query

∃x Fourside(x) ?

LNN Code

Since the LNN has a one-to-one mapping with First-order Logic, the problem can be directly translated to the LNN representation. The following code snippet shows how to build an LNN model for the above problem and performance inference to answer queries.

from lnn import (Predicate, Variable,
                 Exists, Implies, Forall, Model, Fact, World)

model = Model()

# Variablle
x = Variable('x')

# Predicate declarations
square = Predicate('square')
rectangle = Predicate('rectangle')
foursides = Predicate('foursides')

# Axioms declarations
square_rect = Forall(x, Implies(square(x), rectangle(x)))
rect_foursides = Forall(x, Implies(rectangle(x), foursides(x)))

# Query
query = Exists(x, foursides(x))

# Add predicates and rules to the model
model.add_knowledge(square, rectangle, square_rect, rect_foursides, query)

# Add facts to the model
model.add_data({square: {'c': Fact.TRUE, 'k': Fact.TRUE}})

# Perform inference
steps, facts_inferred = model.infer()

# Inspect the query node
print(model['foursided_objects'].true_groundings)

Expected output: {'c', 'k'}

More complex reasoning example

Problem in Natural Language

Background knowledge: The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono , an enemy of America , and other countries Gotham and Wakanda all have some missiles . Nono ’s missiles were sold to it by Colonel West , who is American .

Query: Prove that Colonel West is a criminal .

We manually extract the following predicates: Owns , Missile , American , Enemy , Weapon , Sells , and Hostile ; and the following objects: nono , m1 , m2 , m3 , west and america . Below is the problem in FOL.

Problem in First-order Logic

Owns(nono,m1)

Missile(m1)

Missile(m2)

Missile(m3)

American(west)

Enemy(nono,america)

Enemy(wakanda,america)

Enemy(gotham,america)

∀ x,y,z American(x) ∧ Weapon(y) ∧ Sells(x,y,z) ∧ Hostile(z) → Criminal(x)

∀ x Missile(x) ∧ Owns(nono,x) → Sells(west,x,nono)

∀ x Missile(x) → Weapon(x)

∀ x Enemy(x,america) → Hostile(x)

LNN Code

The code snippet below shows the declaration of the model and all the predicates.

from lnn import (Predicate, Variable, Join, And,
                 Exists, Implies, Forall, Model, Fact, World)

model = Model()  # Instantiate a model.
x, y, z, w = map(Variable, ['x', 'y', 'z', 'w'])

# Define and add predicates to the model.
owns = model['owns'] = Predicate('owns', 2)  # binary predicate
missile = model['missile'] = Predicate('missile')
american = model['american'] = Predicate('american')
enemy = model['enemy'] = Predicate('enemy', 2)
hostile = model['hostile'] = Predicate('hostile')
criminal = model['criminal'] = Predicate('criminal')
weapon = model['weapon'] = Predicate('weapon')
sells = model['sells'] = Predicate('sells', 3)  # ternary predicate

The code snippet below shows an example of adding the background knowledge into the model. All the other rules can be added to the model similarly.

# Define and add the background knowledge to  the model.
america_enemies = (
    Forall(x, Implies(enemy(x, (y, 'America')), 
                      hostile(x),
                      ),
           world=World.AXIOM)
    )
model.add_knowledge(america_enemies)

The code snippet below shows how to add the query into the model.

# Define queries
query = Exists(x, criminal(x))
model.add_knowledge(query)

Finally, we can add facts into the model.

# Add facts to model.
model.set_facts({
    owns: {('Nono', 'M1'): Fact.TRUE},
    missile: {'M1': Fact.TRUE},
    american: {'West': Fact.TRUE},
    enemy: {('Nono', 'America'): Fact.TRUE},
})

Then we are ready to perform inference and answer queries (aka theorem proving):

model.infer()
print(model[query].true_groundings)

Expected output: {west} .