Negation: -
Conjunction: &
Disjunction: |
Implication: ->
variable: x or x2 // var if single letter followed by a number
constant: asdf // starts with more than a single letter
Infer
British (x) -> European (x)
friends(x, y) & man(y) & woman(x) -> friends(y, x)
Statement
British (Tim)
-British (Simsung)
Python code
Import
from nltk.sem import Expression
from mltk.inference import ResolutionProver
Read expressions
read_expr = Expression.fromstring
p1 = read_expr('British (x) -> European (x)')
kb=[p1, p2, ...] # imagine you have loads
Query
q = read_expr('British (Tim)')
r = ResolutionProver().prove(q, kb, verbose=True)