Source code for nltk.sem.skolemize

# Natural Language Toolkit: Semantic Interpretation
#
# Author: Ewan Klein <ewan@inf.ed.ac.uk>
#
# Copyright (C) 2001-2017 NLTK Project
# URL: <http://nltk.org/>
# For license information, see LICENSE.TXT

from nltk.sem.logic import (AllExpression, AndExpression, ApplicationExpression,
                            EqualityExpression, ExistsExpression, IffExpression,
                            ImpExpression, NegatedExpression, OrExpression,
                            VariableExpression, skolem_function, unique_variable)

[docs]def skolemize(expression, univ_scope=None, used_variables=None): """ Skolemize the expression and convert to conjunctive normal form (CNF) """ if univ_scope is None: univ_scope = set() if used_variables is None: used_variables = set() if isinstance(expression, AllExpression): term = skolemize(expression.term, univ_scope|set([expression.variable]), used_variables|set([expression.variable])) return term.replace(expression.variable, VariableExpression(unique_variable(ignore=used_variables))) elif isinstance(expression, AndExpression): return skolemize(expression.first, univ_scope, used_variables) &\ skolemize(expression.second, univ_scope, used_variables) elif isinstance(expression, OrExpression): return to_cnf(skolemize(expression.first, univ_scope, used_variables), skolemize(expression.second, univ_scope, used_variables)) elif isinstance(expression, ImpExpression): return to_cnf(skolemize(-expression.first, univ_scope, used_variables), skolemize(expression.second, univ_scope, used_variables)) elif isinstance(expression, IffExpression): return to_cnf(skolemize(-expression.first, univ_scope, used_variables), skolemize(expression.second, univ_scope, used_variables)) &\ to_cnf(skolemize(expression.first, univ_scope, used_variables), skolemize(-expression.second, univ_scope, used_variables)) elif isinstance(expression, EqualityExpression): return expression elif isinstance(expression, NegatedExpression): negated = expression.term if isinstance(negated, AllExpression): term = skolemize(-negated.term, univ_scope, used_variables|set([negated.variable])) if univ_scope: return term.replace(negated.variable, skolem_function(univ_scope)) else: skolem_constant = VariableExpression(unique_variable(ignore=used_variables)) return term.replace(negated.variable, skolem_constant) elif isinstance(negated, AndExpression): return to_cnf(skolemize(-negated.first, univ_scope, used_variables), skolemize(-negated.second, univ_scope, used_variables)) elif isinstance(negated, OrExpression): return skolemize(-negated.first, univ_scope, used_variables) &\ skolemize(-negated.second, univ_scope, used_variables) elif isinstance(negated, ImpExpression): return skolemize(negated.first, univ_scope, used_variables) &\ skolemize(-negated.second, univ_scope, used_variables) elif isinstance(negated, IffExpression): return to_cnf(skolemize(-negated.first, univ_scope, used_variables), skolemize(-negated.second, univ_scope, used_variables)) &\ to_cnf(skolemize(negated.first, univ_scope, used_variables), skolemize(negated.second, univ_scope, used_variables)) elif isinstance(negated, EqualityExpression): return expression elif isinstance(negated, NegatedExpression): return skolemize(negated.term, univ_scope, used_variables) elif isinstance(negated, ExistsExpression): term = skolemize(-negated.term, univ_scope|set([negated.variable]), used_variables|set([negated.variable])) return term.replace(negated.variable, VariableExpression(unique_variable(ignore=used_variables))) elif isinstance(negated, ApplicationExpression): return expression else: raise Exception('\'%s\' cannot be skolemized' % expression) elif isinstance(expression, ExistsExpression): term = skolemize(expression.term, univ_scope, used_variables|set([expression.variable])) if univ_scope: return term.replace(expression.variable, skolem_function(univ_scope)) else: skolem_constant = VariableExpression(unique_variable(ignore=used_variables)) return term.replace(expression.variable, skolem_constant) elif isinstance(expression, ApplicationExpression): return expression else: raise Exception('\'%s\' cannot be skolemized' % expression)
[docs]def to_cnf(first, second): """ Convert this split disjunction to conjunctive normal form (CNF) """ if isinstance(first, AndExpression): r_first = to_cnf(first.first, second) r_second = to_cnf(first.second, second) return r_first & r_second elif isinstance(second, AndExpression): r_first = to_cnf(first, second.first) r_second = to_cnf(first, second.second) return r_first & r_second else: return first | second