neurolang.logic.horn_clauses module¶

Translation from First Order Logic to Horn clauses.

This module defines the HornClause expression class and algorithms to translate First Order Logic expressions to a union of Horn clauses. Between the algorithms here are implemented a translation from FOL sentences to an equivalent expression in safe range normal form, how to obtain the set of range restricted variables of an expression, how to check if the expression is safe range and, if so, how to translate the expression to a union of horn clauses. Furthermore the resulting horn clauses can be translated to a datalog expression block to use in a solver. The theory behind this is mostly taken from the chapter 4 of [1].

[1]

Abiteboul, Hull, and Vianu, Foundations of Databases: The Logical Level.

class neurolang.logic.horn_clauses.ConvertSRNFToHornClause(*args, **kwargs)¶

Bases: PatternWalker

Converts a expression in safe range normal form into the atoms of a horn clause and a list of auxiliar queries remaining to be processed.

See convert_srnf_to_horn_clauses.

Attributes:

patterns: Property holding an iterator of triplets (pattern, guard, action).

Methods

`match`(expression)	Find the action for a given expression by going through the `patterns`.
`pattern_match`(pattern, expression)	Return `True` if `pattern` matches `expression`.
`type`

atom
conjunction
disjunction
existential
negated_atom
negated_existential
pattern_match_expression
pattern_match_expression_parameters
pattern_match_expression_tuple
pattern_match_tuple
unknown
walk

atom(exp)¶

conjunction(exp)¶

disjunction(exp)¶

existential(exp)¶

negated_atom(exp)¶

negated_existential(exp)¶

type = typing.Any¶

unknown(exp)¶

class neurolang.logic.horn_clauses.Fol2DatalogMixin(*args, **kwargs)¶

Bases: PatternWalker

Attributes:

patterns: Property holding an iterator of triplets (pattern, guard, action).

Methods

`match`(expression)	Find the action for a given expression by going through the `patterns`.
`pattern_match`(pattern, expression)	Return `True` if `pattern` matches `expression`.
`type`

pattern_match_expression
pattern_match_expression_parameters
pattern_match_expression_tuple
pattern_match_tuple
translate_implication
walk

translate_implication(imp)¶

type = typing.Any¶

exception neurolang.logic.horn_clauses.Fol2DatalogTranslationException¶: Bases: NeuroLangException

class neurolang.logic.horn_clauses.HornClause(head, body)¶

Bases: LogicOperator

Expression of the form P(X) ← (Q(X) ⋀ … ⋀ S(X))

Methods

`__call__`(args, *kwargs)	Call self as a function.
`apply`(*args)	Builds a new expression using a tuple of its parameters
`type`
`unapply`()	Returns a tuple of parameters used to build the expression.

cast
change_type
get_wrapped_attribute

type = typing.Any¶

class neurolang.logic.horn_clauses.HornFact(head)¶

Bases: HornClause

Expression of the form P(X) ← TRUE

Methods

`__call__`(args, *kwargs)	Call self as a function.
`apply`(*args)	Builds a new expression using a tuple of its parameters
`type`
`unapply`()	Returns a tuple of parameters used to build the expression.

cast
change_type
get_wrapped_attribute

type = typing.Any¶

class neurolang.logic.horn_clauses.MoveNegationsToAtomsOrExistentialQuantifiers(*args, **kwargs)¶

Bases: MoveNegationsToAtoms

Attributes:

patterns: Property holding an iterator of triplets (pattern, guard, action).

Methods

`match`(expression)	Find the action for a given expression by going through the `patterns`.
`pattern_match`(pattern, expression)	Return `True` if `pattern` matches `expression`.
`type`

negated_conjunction
negated_disjunction
negated_existential
negated_universal
pattern_match_expression
pattern_match_expression_parameters
pattern_match_expression_tuple
pattern_match_tuple
remove_double_negation
remove_single
walk
walk_constant
walk_function
walk_implication
walk_nary
walk_negation
walk_quantifier
walk_symbol

negated_existential(negation)¶

type = typing.Any¶

exception neurolang.logic.horn_clauses.NeuroLangTranslateToHornClauseException¶: Bases: NeuroLangException

class neurolang.logic.horn_clauses.RangeRestrictedVariables(*args, **kwargs)¶

Bases: WalkLogicProgramAggregatingSets

The set of variables which are range restricted in a expression.

The range restricted variables are defined recursively as follows: - For atoms: The variables occurring in the arguments. - For negation: The empty set. - For existential predicates: The restricted variables of the body without

the head.

For conjunction: The union of the restricted variables of the involved expressions.
For disjunction: The intersection of the restricted variables of the involved expressions.

Also, if an existentially quantified variable is not restricted in the body of its predicate then the expression does not have a restricted range. This also counts for existentials inside negations.

Attributes:

patterns: Property holding an iterator of triplets (pattern, guard, action).

Methods

`match`(expression)	Find the action for a given expression by going through the `patterns`.
`pattern_match`(pattern, expression)	Return `True` if `pattern` matches `expression`.
`type`

conjunction
disjunction
existential
function
logic_operator
negation
pattern_match_expression
pattern_match_expression_parameters
pattern_match_expression_tuple
pattern_match_tuple
quantifier
union
walk
walk_binary_logic_expression
walk_nary

conjunction(exp)¶

disjunction(exp)¶

existential(exp)¶

function(exp)¶

negation(exp)¶

type = typing.Any¶

class neurolang.logic.horn_clauses.TranslateHornClausesToDatalog(*args, **kwargs)¶

Bases: LogicExpressionWalker

Attributes:

patterns: Property holding an iterator of triplets (pattern, guard, action).

Methods

`match`(expression)	Find the action for a given expression by going through the `patterns`.
`pattern_match`(pattern, expression)	Return `True` if `pattern` matches `expression`.
`type`

horn_fact
horn_rule
pattern_match_expression
pattern_match_expression_parameters
pattern_match_expression_tuple
pattern_match_tuple
quantifier
union
walk
walk_constant
walk_function
walk_implication
walk_nary
walk_negation
walk_quantifier
walk_symbol

horn_fact(exp)¶

horn_rule(exp)¶

quantifier(exp)¶

type = typing.Any¶

union(exp)¶

neurolang.logic.horn_clauses.convert_srnf_to_horn_clauses(head, expression)¶

Converts a safe range query into an union of horn clauses.

Given a query represented by an _answer_ head and a range restricted expression in safe range normal form, returns an union of horn clauses in which the result set given to head is equivalent. Also, it is required that all the variables appear free in the body.

The algorithm is implemented using a stack of queries to process, which starts with the query given as parameter. In each iteration, a query is processed and the result is a Horn clause with a remainder of auxiliar queries which appear in the clause. The clause is then added to the result and the remainder queries are added to the stack.

The cases where auxiliar queries are needed are the negation over an existential predicate and the disjunction. For the disjunction an auxiliar query is introduced for each formula in the disjunction, but all with the same head. For a negated existential another query is added because negation can only be applied over atoms.

Care must be taken to ensure that the auxiliar queries are also range restricted. To do so, a set of the positive atoms which appear in the parent expressions is added alongside each query in the stack. Those atoms are precisely the ones that restrict the range of the variables. If is the case that a query is not range restricted then some of those atoms are added to the body of the query to ensure the range restriction. This restricts the result set of the auxiliar queries but does not alter the equivalence for the overall query because the range of those variables was already restricted in some of its parents.

neurolang.logic.horn_clauses.convert_to_srnf(e)¶

Convert an expression to safe range normal form.

Safe range normal form is an equivalent expression but where the there are no implications or universal quantifiers and also the negations are only applied over atoms or existential quantifiers.

neurolang.logic.horn_clauses.fol_query_to_datalog_program(head, exp)¶

Returns a datalog program for a given query in first order logic.

Given a query represented by an _answer_ head and an expression in first order logic, converts the expression to safe range normal form and then, if the query is safe range, returns an ExpressionBlock with the equivalent program in datalog. Throw a NeuroLangTranslateToHornClauseException otherwise.

neurolang.logic.horn_clauses.is_safe_range(expression)¶

Return true if an expression is safe range.

This function receives an expression in safe range normal form and returns true if all its free variables are range restricted.

neurolang.logic.horn_clauses.range_restricted_variables(e)¶

neurolang.logic.horn_clauses.translate_horn_clauses_to_datalog(horn_clauses)¶: Straightforward translation from Horn clauses a datalog expression block.