nltk.sem.logic module

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

class nltk.sem.logic.Tokens

Bases: object

LAMBDA = '\\'

LAMBDA_LIST = ['\\']

EXISTS = 'exists'

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

ALL = 'all'

ALL_LIST = ['all', 'forall']

IOTA = 'iota'

IOTA_LIST = ['iota']

DOT = '.'

OPEN = '('

CLOSE = ')'

COMMA = ','

NOT = '-'

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

AND = '&'

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

OR = '|'

OR_LIST = ['or', '|']

IMP = '->'

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

IFF = '<->'

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

EQ = '='

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

NEQ = '!='

NEQ_LIST = ['!=']

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

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

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

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

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

nltk.sem.logic.boolean_ops()

Boolean operators

nltk.sem.logic.equality_preds()

Equality predicates

nltk.sem.logic.binding_ops()

Binding operators

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?

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

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_quoted_token(data_idx, data)

get_all_symbols()

This method exists to be overridden

inRange(location)

Return TRUE if the given location is within the buffer

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.

isvariable(tok)

process_next_expression(context)

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

handle(tok, context)

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

attempt_adjuncts(expression, context)

handle_negation(tok, context)

make_NegatedExpression(expression)

handle_variable(tok, context)

get_next_token_variable(description)

handle_lambda(tok, context)

handle_quant(tok, context)

get_QuantifiedExpression_factory(tok)

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

make_QuanifiedExpression(factory, variable, term)

handle_open(tok, context)

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.

make_EqualityExpression(first, second)

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

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.

get_BooleanExpression_factory(tok)

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

make_BooleanExpression(factory, first, second)

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.

make_ApplicationExpression(function, argument)

make_VariableExpression(name)

make_LambdaExpression(variable, term)

has_priority(operation, context)

assertNextToken(expected)

assertToken(tok, expected)

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)

class nltk.sem.logic.Variable

Bases: object

__init__(name)

Parameters

name – the name of the variable

substitute_bindings(bindings)

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

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

Return a skolem function over the variables in univ_scope param univ_scope

class nltk.sem.logic.Type

Bases: object

classmethod fromstring(s)

class nltk.sem.logic.ComplexType

Bases: Type

__init__(first, second)

matches(other)

resolve(other)

str()

class nltk.sem.logic.BasicType

Bases: Type

matches(other)

resolve(other)

class nltk.sem.logic.EntityType

Bases: BasicType

str()

class nltk.sem.logic.TruthValueType

Bases: BasicType

str()

class nltk.sem.logic.EventType

Bases: BasicType

str()

class nltk.sem.logic.AnyType

Bases: BasicType, ComplexType

__init__()

property first

property second

matches(other)

resolve(other)

str()

nltk.sem.logic.read_type(type_string)

exception nltk.sem.logic.TypeException

Bases: Exception

__init__(msg)

exception nltk.sem.logic.InconsistentTypeHierarchyException

Bases: TypeException

__init__(variable, expression=None)

exception nltk.sem.logic.TypeResolutionException

Bases: TypeException

__init__(expression, other_type)

exception nltk.sem.logic.IllegalTypeException

Bases: TypeException

__init__(expression, other_type, allowed_type)

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)

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.Expression

Bases: SubstituteBindingsI

This is the base abstract object for all logical expressions

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

applyto(other)

negate()

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

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

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

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

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?

normalize(newvars=None)

Rename auto-generated unique variables

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

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

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

constants()

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

predicates()

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

simplify()

Returns

beta-converted version of this expression

make_VariableExpression(variable)

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

simplify()

Returns

beta-converted version of this expression

property type

findtype(variable)

:see Expression.findtype()

constants()

See

Expression.constants()

predicates()

See

Expression.predicates()

visit(function, combinator)

See

Expression.visit()

uncurry()

Uncurry this application expression

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

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.

property args

Return uncurried arg-list

is_atom()

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

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

simplify()

Returns

beta-converted version of this expression

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

See

Expression.replace()

findtype(variable)

:see Expression.findtype()

predicates()

See

Expression.predicates()

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.

property type

free()

See

Expression.free()

constants()

See

Expression.constants()

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.

type = ?

free()

See

Expression.free()

constants()

See

Expression.constants()

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.ConstantExpression

Bases: AbstractVariableExpression

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

type = e

free()

See

Expression.free()

constants()

See

Expression.constants()

nltk.sem.logic.VariableExpression(variable)

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

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

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

See

Expression.replace()

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

free()

See

Expression.free()

findtype(variable)

:see Expression.findtype()

visit(function, combinator)

See

Expression.visit()

visit_structured(function, combinator)

See

Expression.visit_structured()

class nltk.sem.logic.LambdaExpression

Bases: VariableBinderExpression

property type

class nltk.sem.logic.QuantifiedExpression

Bases: VariableBinderExpression

property type

class nltk.sem.logic.ExistsExpression

Bases: QuantifiedExpression

getQuantifier()

class nltk.sem.logic.AllExpression

Bases: QuantifiedExpression

getQuantifier()

class nltk.sem.logic.IotaExpression

Bases: QuantifiedExpression

getQuantifier()

class nltk.sem.logic.NegatedExpression

Bases: Expression

__init__(term)

property type

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

visit(function, combinator)

See

Expression.visit()

negate()

See

Expression.negate()

class nltk.sem.logic.BinaryExpression

Bases: Expression

__init__(first, second)

property type

findtype(variable)

:see Expression.findtype()

visit(function, combinator)

See

Expression.visit()

class nltk.sem.logic.BooleanExpression

Bases: BinaryExpression

class nltk.sem.logic.AndExpression

Bases: BooleanExpression

This class represents conjunctions

getOp()

class nltk.sem.logic.OrExpression

Bases: BooleanExpression

This class represents disjunctions

getOp()

class nltk.sem.logic.ImpExpression

Bases: BooleanExpression

This class represents implications

getOp()

class nltk.sem.logic.IffExpression

Bases: BooleanExpression

This class represents biconditionals

getOp()

class nltk.sem.logic.EqualityExpression

Bases: BinaryExpression

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

getOp()

exception nltk.sem.logic.LogicalExpressionException

Bases: Exception

__init__(index, message)

exception nltk.sem.logic.UnexpectedTokenException

Bases: LogicalExpressionException

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

exception nltk.sem.logic.ExpectedMoreTokensException

Bases: LogicalExpressionException

__init__(index, message=None)

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.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_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.demo()

nltk.sem.logic.demo_errors()

nltk.sem.logic.demoException(s)

nltk.sem.logic.printtype(ex)