nltk.sem.logic module

A version of first order predicate logic, built on top of the typed lambda calculus.

class nltk.sem.logic.AbstractVariableExpression

Bases: Expression

This class represents a variable to be used as a predicate or entity

__init__(variable)

Parameters

variable – Variable, for the variable

findtype(variable)

:see Expression.findtype()

predicates()

See

Expression.predicates()

replace(variable, expression, replace_bound=False, alpha_convert=True)

See

Expression.replace()

simplify()

Returns

beta-converted version of this expression

class nltk.sem.logic.AllExpression

Bases: QuantifiedExpression

getQuantifier()

class nltk.sem.logic.AndExpression

Bases: BooleanExpression

This class represents conjunctions

getOp()

class nltk.sem.logic.AnyType

Bases: BasicType, ComplexType

__init__()

property first

matches(other)

resolve(other)

property second

str()

class nltk.sem.logic.ApplicationExpression

Bases: Expression

This class is used to represent two related types of logical expressions.

The first is a Predicate Expression, such as “P(x,y)”. A predicate expression is comprised of a FunctionVariableExpression or ConstantExpression as the predicate and a list of Expressions as the arguments.

The second is a an application of one expression to another, such as “(x.dog(x))(fido)”.

The reason Predicate Expressions are treated as Application Expressions is that the Variable Expression predicate of the expression may be replaced with another Expression, such as a LambdaExpression, which would mean that the Predicate should be thought of as being applied to the arguments.

The logical expression reader will always curry arguments in a application expression. So, “x y.see(x,y)(john,mary)” will be represented internally as “((x y.(see(x))(y))(john))(mary)”. This simplifies the internals since there will always be exactly one argument in an application.

The str() method will usually print the curried forms of application expressions. The one exception is when the the application expression is really a predicate expression (ie, underlying function is an AbstractVariableExpression). This means that the example from above will be returned as “(x y.see(x,y)(john))(mary)”.

__init__(function, argument)

Parameters

• function – Expression, for the function expression

• argument – Expression, for the argument

property args

Return uncurried arg-list

constants()

See

Expression.constants()

findtype(variable)

:see Expression.findtype()

is_atom()

Is this expression an atom (as opposed to a lambda expression applied to a term)?

property pred

Return uncurried base-function. If this is an atom, then the result will be a variable expression. Otherwise, it will be a lambda expression.

predicates()

See

Expression.predicates()

simplify()

Returns

beta-converted version of this expression

property type

uncurry()

Uncurry this application expression

return: A tuple (base-function, arg-list)

visit(function, combinator)

See

Expression.visit()

class nltk.sem.logic.BasicType

Bases: Type

matches(other)

resolve(other)

class nltk.sem.logic.BinaryExpression

Bases: Expression

__init__(first, second)

findtype(variable)

:see Expression.findtype()

property type

visit(function, combinator)

See

Expression.visit()

class nltk.sem.logic.BooleanExpression

Bases: BinaryExpression

class nltk.sem.logic.ComplexType

Bases: Type

__init__(first, second)

matches(other)

resolve(other)

str()

class nltk.sem.logic.ConstantExpression

Bases: AbstractVariableExpression

This class represents variables that do not take the form of a single character followed by zero or more digits.

constants()

See

Expression.constants()

free()

See

Expression.free()

type = e

class nltk.sem.logic.EntityType

Bases: BasicType

str()

class nltk.sem.logic.EqualityExpression

Bases: BinaryExpression

This class represents equality expressions like “(x = y)”.

getOp()

class nltk.sem.logic.EventType

Bases: BasicType

str()

class nltk.sem.logic.EventVariableExpression

Bases: IndividualVariableExpression

This class represents variables that take the form of a single lowercase ‘e’ character followed by zero or more digits.

type = v

class nltk.sem.logic.ExistsExpression

Bases: QuantifiedExpression

getQuantifier()

exception nltk.sem.logic.ExpectedMoreTokensException

Bases: LogicalExpressionException

__init__(index, message=None)

class nltk.sem.logic.Expression

Bases: SubstituteBindingsI

This is the base abstract object for all logical expressions

applyto(other)

constants()

Return a set of individual constants (non-predicates). :return: set of Variable objects

equiv(other, prover=None)

Check for logical equivalence. Pass the expression (self <-> other) to the theorem prover. If the prover says it is valid, then the self and other are equal.

Parameters

• other – an Expression to check equality against

• prover – a nltk.inference.api.Prover

findtype(variable)

Find the type of the given variable as it is used in this expression. For example, finding the type of “P” in “P(x) & Q(x,y)” yields “<e,t>”

Parameters

variable – Variable

free()

Return a set of all the free (non-bound) variables. This includes both individual and predicate variables, but not constants. :return: set of Variable objects

classmethod fromstring(s, type_check=False, signature=None)

make_VariableExpression(variable)

negate()

If this is a negated expression, remove the negation. Otherwise add a negation.

normalize(newvars=None)

Rename auto-generated unique variables

predicates()

Return a set of predicates (constants, not variables). :return: set of Variable objects

replace(variable, expression, replace_bound=False, alpha_convert=True)

Replace every instance of ‘variable’ with ‘expression’ :param variable: Variable The variable to replace :param expression: Expression The expression with which to replace it :param replace_bound: bool Should bound variables be replaced? :param alpha_convert: bool Alpha convert automatically to avoid name clashes?

simplify()

Returns

beta-converted version of this expression

substitute_bindings(bindings)

Returns

The object that is obtained by replacing each variable bound by bindings with its values. Aliases are already resolved. (maybe?)

Return type

(any)

typecheck(signature=None)

Infer and check types. Raise exceptions if necessary.

Parameters

signature – dict that maps variable names to types (or string representations of types)

Returns

the signature, plus any additional type mappings

variables()

Return a set of all the variables for binding substitution. The variables returned include all free (non-bound) individual variables and any variable starting with ‘?’ or ‘@’. :return: set of Variable objects

visit(function, combinator)

Recursively visit subexpressions. Apply ‘function’ to each subexpression and pass the result of each function application to the ‘combinator’ for aggregation:

return combinator(map(function, self.subexpressions))

Bound variables are neither applied upon by the function nor given to the combinator. :param function: Function<Expression,T> to call on each subexpression :param combinator: Function<list<T>,R> to combine the results of the function calls :return: result of combination R

visit_structured(function, combinator)

Recursively visit subexpressions. Apply ‘function’ to each subexpression and pass the result of each function application to the ‘combinator’ for aggregation. The combinator must have the same signature as the constructor. The function is not applied to bound variables, but they are passed to the combinator. :param function: Function to call on each subexpression :param combinator: Function with the same signature as the constructor, to combine the results of the function calls :return: result of combination

class nltk.sem.logic.FunctionVariableExpression

Bases: AbstractVariableExpression

This class represents variables that take the form of a single uppercase character followed by zero or more digits.

constants()

See

Expression.constants()

free()

See

Expression.free()

type = ?

class nltk.sem.logic.IffExpression

Bases: BooleanExpression

This class represents biconditionals

getOp()

exception nltk.sem.logic.IllegalTypeException

Bases: TypeException

__init__(expression, other_type, allowed_type)

class nltk.sem.logic.ImpExpression

Bases: BooleanExpression

This class represents implications

getOp()

exception nltk.sem.logic.InconsistentTypeHierarchyException

Bases: TypeException

__init__(variable, expression=None)

class nltk.sem.logic.IndividualVariableExpression

Bases: AbstractVariableExpression

This class represents variables that take the form of a single lowercase character (other than ‘e’) followed by zero or more digits.

constants()

See

Expression.constants()

free()

See

Expression.free()

property type

class nltk.sem.logic.IotaExpression

Bases: QuantifiedExpression

getQuantifier()

class nltk.sem.logic.LambdaExpression

Bases: VariableBinderExpression

property type

class nltk.sem.logic.LogicParser

Bases: object

A lambda calculus expression parser.

__init__(type_check=False)

Parameters

type_check (bool) – should type checking be performed to their types?

assertNextToken(expected)

assertToken(tok, expected)

attempt_ApplicationExpression(expression, context)

Attempt to make an application expression. The next tokens are a list of arguments in parens, then the argument expression is a function being applied to the arguments. Otherwise, return the argument expression.

attempt_BooleanExpression(expression, context)

Attempt to make a boolean expression. If the next token is a boolean operator, then a BooleanExpression will be returned. Otherwise, the parameter will be returned.

attempt_EqualityExpression(expression, context)

Attempt to make an equality expression. If the next token is an equality operator, then an EqualityExpression will be returned. Otherwise, the parameter will be returned.

attempt_adjuncts(expression, context)

get_BooleanExpression_factory(tok)

This method serves as a hook for other logic parsers that have different boolean operators

get_QuantifiedExpression_factory(tok)

This method serves as a hook for other logic parsers that have different quantifiers

get_all_symbols()

This method exists to be overridden

get_next_token_variable(description)

handle(tok, context)

This method is intended to be overridden for logics that use different operators or expressions

handle_lambda(tok, context)

handle_negation(tok, context)

handle_open(tok, context)

handle_quant(tok, context)

handle_variable(tok, context)

has_priority(operation, context)

inRange(location)

Return TRUE if the given location is within the buffer

isvariable(tok)

make_ApplicationExpression(function, argument)

make_BooleanExpression(factory, first, second)

make_EqualityExpression(first, second)

This method serves as a hook for other logic parsers that have different equality expression classes

make_LambdaExpression(variable, term)

make_NegatedExpression(expression)

make_QuanifiedExpression(factory, variable, term)

make_VariableExpression(name)

parse(data, signature=None)

Parse the expression.

Parameters

• data – str for the input to be parsed

• signature – dict<str, str> that maps variable names to type strings

Returns

a parsed Expression

process(data)

Split the data into tokens

process_next_expression(context)

Parse the next complete expression from the stream and return it.

process_quoted_token(data_idx, data)

token(location=None)

Get the next waiting token. If a location is given, then return the token at currentIndex+location without advancing currentIndex; setting it gives lookahead/lookback capability.

type_check

A list of tuples of quote characters. The 4-tuple is comprised of the start character, the end character, the escape character, and a boolean indicating whether the quotes should be included in the result. Quotes are used to signify that a token should be treated as atomic, ignoring any special characters within the token. The escape character allows the quote end character to be used within the quote. If True, the boolean indicates that the final token should contain the quote and escape characters. This method exists to be overridden

exception nltk.sem.logic.LogicalExpressionException

Bases: Exception

__init__(index, message)

class nltk.sem.logic.NegatedExpression

Bases: Expression

__init__(term)

findtype(variable)

Find the type of the given variable as it is used in this expression. For example, finding the type of “P” in “P(x) & Q(x,y)” yields “<e,t>”

Parameters

variable – Variable

negate()

See

Expression.negate()

property type

visit(function, combinator)

See

Expression.visit()

class nltk.sem.logic.OrExpression

Bases: BooleanExpression

This class represents disjunctions

getOp()

class nltk.sem.logic.QuantifiedExpression

Bases: VariableBinderExpression

property type

class nltk.sem.logic.SubstituteBindingsI

Bases: object

An interface for classes that can perform substitutions for variables.

substitute_bindings(bindings)

Returns

The object that is obtained by replacing each variable bound by bindings with its values. Aliases are already resolved. (maybe?)

Return type

(any)

variables()

Returns

A list of all variables in this object.

class nltk.sem.logic.Tokens

Bases: object

ALL = 'all'

ALL_LIST = ['all', 'forall']

AND = '&'

AND_LIST = ['and', '&', '^']

BINOPS = ['and', '&', '^', 'or', '|', 'implies', '->', '=>', 'iff', '<->', '<=>']

CLOSE = ')'

COMMA = ','

DOT = '.'

EQ = '='

EQ_LIST = ['=', '==']

EXISTS = 'exists'

EXISTS_LIST = ['some', 'exists', 'exist']

IFF = '<->'

IFF_LIST = ['iff', '<->', '<=>']

IMP = '->'

IMP_LIST = ['implies', '->', '=>']

IOTA = 'iota'

IOTA_LIST = ['iota']

LAMBDA = '\\'

LAMBDA_LIST = ['\\']

NEQ = '!='

NEQ_LIST = ['!=']

NOT = '-'

NOT_LIST = ['not', '-', '!']

OPEN = '('

OR = '|'

OR_LIST = ['or', '|']

PUNCT = ['.', '(', ')', ',']

QUANTS = ['some', 'exists', 'exist', 'all', 'forall', 'iota']

SYMBOLS = ['&', '^', '|', '->', '=>', '<->', '<=>', '=', '==', '!=', '\\', '.', '(', ')', ',', '-', '!']

TOKENS = ['and', '&', '^', 'or', '|', 'implies', '->', '=>', 'iff', '<->', '<=>', '=', '==', '!=', 'some', 'exists', 'exist', 'all', 'forall', 'iota', '\\', '.', '(', ')', ',', 'not', '-', '!']

class nltk.sem.logic.TruthValueType

Bases: BasicType

str()

class nltk.sem.logic.Type

Bases: object

classmethod fromstring(s)

exception nltk.sem.logic.TypeException

Bases: Exception

__init__(msg)

exception nltk.sem.logic.TypeResolutionException

Bases: TypeException

__init__(expression, other_type)

exception nltk.sem.logic.UnexpectedTokenException

Bases: LogicalExpressionException

__init__(index, unexpected=None, expected=None, message=None)

class nltk.sem.logic.Variable

Bases: object

__init__(name)

Parameters

name – the name of the variable

substitute_bindings(bindings)

class nltk.sem.logic.VariableBinderExpression

Bases: Expression

This an abstract class for any Expression that binds a variable in an Expression. This includes LambdaExpressions and Quantified Expressions

__init__(variable, term)

Parameters

• variable – Variable, for the variable

• term – Expression, for the term

alpha_convert(newvar)

Rename all occurrences of the variable introduced by this variable binder in the expression to newvar. :param newvar: Variable, for the new variable

findtype(variable)

:see Expression.findtype()

free()

See

Expression.free()

replace(variable, expression, replace_bound=False, alpha_convert=True)

See

Expression.replace()

visit(function, combinator)

See

Expression.visit()

visit_structured(function, combinator)

See

Expression.visit_structured()

nltk.sem.logic.VariableExpression(variable)

This is a factory method that instantiates and returns a subtype of AbstractVariableExpression appropriate for the given variable.

nltk.sem.logic.binding_ops()

Binding operators

nltk.sem.logic.boolean_ops()

Boolean operators

nltk.sem.logic.demo()

nltk.sem.logic.demoException(s)

nltk.sem.logic.demo_errors()

nltk.sem.logic.equality_preds()

Equality predicates

nltk.sem.logic.is_eventvar(expr)

An event variable must be a single lowercase ‘e’ character followed by zero or more digits.

Parameters

expr – str

Returns

bool True if expr is of the correct form

nltk.sem.logic.is_funcvar(expr)

A function variable must be a single uppercase character followed by zero or more digits.

Parameters

expr – str

Returns

bool True if expr is of the correct form

nltk.sem.logic.is_indvar(expr)

An individual variable must be a single lowercase character other than ‘e’, followed by zero or more digits.

Parameters

expr – str

Returns

bool True if expr is of the correct form

nltk.sem.logic.printtype(ex)

nltk.sem.logic.read_logic(s, logic_parser=None, encoding=None)

Convert a file of First Order Formulas into a list of {Expression}s.

Parameters

• s (str) – the contents of the file

• logic_parser (LogicParser) – The parser to be used to parse the logical expression

• encoding (str) – the encoding of the input string, if it is binary

Returns

a list of parsed formulas.

Return type

list(Expression)

nltk.sem.logic.read_type(type_string)

nltk.sem.logic.skolem_function(univ_scope=None)

Return a skolem function over the variables in univ_scope param univ_scope

nltk.sem.logic.typecheck(expressions, signature=None)

Ensure correct typing across a collection of Expression objects. :param expressions: a collection of expressions :param signature: dict that maps variable names to types (or string representations of types)

nltk.sem.logic.unique_variable(pattern=None, ignore=None)

Return a new, unique variable.

Parameters

• pattern – Variable that is being replaced. The new variable must be the same type.

• term – a set of Variable objects that should not be returned from this function.

Return type

Variable