src.fol package

Submodules

src.fol.data_utils module

class src.fol.data_utils.DataUtils(lark_path, lang_base_path, dataset_type='kandinsky', dataset='twopairs')

Bases: object

Utilities about logic.

A class of utilities about first-order logic.

Parameters

• dataset_type (str) – A dataset type (kandinsky or clevr).

• dataset (str) – A dataset to be used.

Attrs:

base_path: The base path of the dataset.

get_bk(lang)

get_clauses(lang)

load_atoms(path, lang)

Read lines and parse to Atom objects.

load_clauses(path, lang)

Read lines and parse to Atom objects.

load_consts(path)

load_language()

Load language, background knowledge, and clauses from files.

load_neural_preds(path)

load_preds(path)

parse_clause(clause_str, lang)

parse_const(line)

Parse string to function symbols.

parse_funcs(line)

Parse string to function symbols.

parse_neural_pred(line)

Parse string to predicates.

parse_pred(line)

Parse string to predicates.

src.fol.exp_parser module

class src.fol.exp_parser.ExpTree(lang)

Bases: Transformer

Functions to parse strings into logical objects using Lark

Attrs:

lang (language): the language of first-order logic.

args(content)

atom(trees)

body(trees)

clause(trees)

const(name)

functor(name)

predicate(alphas)

small_chars(content)

term(content)

variable(name)

src.fol.exp_parser.flatten(x)

src.fol.language module

class src.fol.language.DataType(name)

Bases: object

Data type in first-order logic.

A class of data types in first-order logic.

Parameters

name (str) – The name of the data type.

Attrs:

name (str): The name of the data type.

class src.fol.language.Language(preds, funcs, consts)

Bases: object

Language of first-order logic.

A class of languages in first-order logic.

Parameters

• preds (List[Predicate]) – A set of predicate symbols.

• funcs (List[FunctionSymbol]) – A set of function symbols.

• consts (List[Const]) – A set of constants.

Attrs:

preds (List[Predicate]): A set of predicate symbols. funcs (List[FunctionSymbol]): A set of function symbols. consts (List[Const]): A set of constants.

get_by_dtype(dtype)

Get constants that match given dtypes.

Parameters

dtype (DataType) – The data type.

Returns

List of constants whose data type is the given data type.

get_by_dtype_name(dtype_name)

Get constants that match given dtype name.

Parameters

dtype_name (str) – The name of the data type to be used.

Returns

List of constants whose datatype has the given name.

get_const_by_name(const_name)

Get the constant by its name.

Parameters

const_name (str) – The name of the constant.

Returns

The matched constant with the given name.

Return type

Const

get_pred_by_name(pred_name)

Get the predicate by its name.

Parameters

pred_name (str) – The name of the predicate.

Returns

The matched preicate with the given name.

Return type

Predicate

get_var_and_dtype(atom)

Get all variables in an input atom with its dtypes by enumerating variables in the input atom.

Note

with the assumption with function free atoms.

Parameters

atom (Atom) – The atom.

Returns

List of tuples (var, dtype)

term_index(term)

Get the index of a term in the language.

Parameters

term (Term) – The term to be used.

Returns

The index of the term.

Return type

int

src.fol.logic module

class src.fol.logic.Atom(pred, terms)

Bases: object

Atoms in first-oder logic.

A class of atoms: p(t1, …, tn)

pred

A predicate of the atom.

Type

Predicate

terms

The terms for the atoms.

Type

List[Term]

all_consts()

all_funcs()

all_vars()

get_terms_by_dtype(dtype)

Return terms that have type of dtype. Returns: (list(Term))

max_depth()

min_depth()

neg()

size()

subs(target_var, const)

class src.fol.logic.Clause(head, body)

Bases: object

Clauses in first-oder logic.

A class of clauses in first-order logic: A :- B1, …, Bn.

head

The head atom.

Type

Atom

body

The atoms for the body.

Type

List[Atom]

all_consts()

all_funcs()

all_vars()

all_vars_by_dtype(dtype)

Get all variables in the clause that has given data type. Returns: list(Var)

count_by_predicate(pred)

is_duplicate()

is_tautology()

max_depth()

min_depth()

size()

subs(target_var, const)

class src.fol.logic.Const(name, dtype=None)

Bases: Term

Constants in first-order logic.

A class of constants in first-oder logic.

name

Name of the term.

Type

str

dtype

Data type of the term.

Type

datatype

all_consts()

all_funcs()

all_vars()

get_ith_term(i)

head()

is_var()

max_depth()

min_depth()

size()

subs(target_var, const)

to_list()

class src.fol.logic.FuncSymbol(name, arity)

Bases: object

Function symbols in first-order logic.

A class of function symbols in first-oder logic.

name

Name of the function.

Type

str

class src.fol.logic.FuncTerm(func_symbol, args)

Bases: Term

Term with a function symbol f(t_1, …, t_n)

A class of terms that cosist of a function symbol in first-oder logic.

func_symbol

A function symbolc in the term.

Type

FuncSymbol

args

arguments for the function symbol.

Type

List[Term]

all_consts()

all_funcs()

all_vars()

get_ith_symbol(i)

get_ith_term(i)

head()

is_var()

max_depth()

min_depth()

pre_order(i)

size()

subs(target_var, const)

to_list()

class src.fol.logic.NeuralPredicate(name, arity, dtypes)

Bases: Predicate

Neural predicats.

A class of neural predicates, which are associated with a differentiable function.

name

A name of the predicate.

Type

str

arity

The arity of the predicate.

Type

int

dtypes

The data types of the arguments for the predicate.

Type

List[DataTypes]

class src.fol.logic.Predicate(name, arity, dtypes)

Bases: object

Predicats in first-order logic.

A class of predicates in first-order logic.

name

A name of the predicate.

Type

str

arity

The arity of the predicate.

Type

int

dtypes

The data types of the arguments for the predicate.

Type

List[DataTypes]

class src.fol.logic.Term

Bases: ABC

Terms in first-order logic.

An abstract class of terms in first-oder logic.

name

Name of the term.

Type

str

dtype

Data type of the term.

Type

datatype

abstract all_consts()

abstract all_funcs()

abstract all_vars()

abstract is_var()

abstract max_depth()

abstract min_depth()

abstract size()

class src.fol.logic.Var(name)

Bases: Term

Variables in first-order logic.

A class of variable in first-oder logic.

name

Name of the variable.

Type

str

all_consts()

all_funcs()

all_vars()

get_ith_term(i)

head()

is_var()

max_depth()

min_depth()

size()

subs(target_var, const)

to_list()

src.fol.logic.flatten(x)

src.fol.logic_ops module

src.fol.logic_ops.find_subs_term(subs_var, disagree_set)

Find term where the var does not occur

Inputs

subs_var : .logic.Var disagree_set : List[.logic.Term]

returns

• flag (bool)

• term (.logic.Term)

src.fol.logic_ops.get_disagree_index(terms)

get the desagreement index in the unification algorithm details in [Foundations of Inductive Logic Programming. Nienhuys-Cheng, S.-H. et.al. 1997.]

Inputs

termsList[Term]

Term : .logic.FuncTerm .logic.Const .logic.Var list of terms

returns

• disagree_flag (bool) – flag of disagreement

• disagree_index (int) – index of the disagreement term in the args of predicates

src.fol.logic_ops.get_disagreements(terms)

get desagreements in the unification algorithm details in [Foundations of Inductive Logic Programming. Nienhuys-Cheng, S.-H. et.al. 1997.]

Inputs

temrsList[Term]

Term : .logic.FuncTerm .logic.Const .logic.Var list of terms

returns

• disagree_flag (bool) – flag of disagreement

• disagree_terms (List[Term]) – Term : .logic.FuncTerm .logic.Const .logic.Var terms of disagreement

src.fol.logic_ops.is_entailed(e, clause, facts, n)

decision function of ground atom is entailed by a clause and facts by n-step inference

Inputs

e.logic.Atom

ground atom

clause.logic.Clause

clause

factsList[.logic.Atom]

set of facts

nint

infer step

returns

flag – ${clause} cup facts models e$

rtype

bool

src.fol.logic_ops.is_singleton(atoms)

returns whether all the input atoms are the same or not

Inputs

atoms: List[.logic.Atom]

[a_1, a_2, …, a_n]

returns

flag – a_1 == a_2 == … == a_n

rtype

bool

src.fol.logic_ops.occur_check(variable, term)

occur check function details in [Foundations of Inductive Logic Programming. Nienhuys-Cheng, S.-H. et.al. 1997.]

Inputs

variable : .logic.Var term : Term

Term : .logic.FuncTerm .logic.Const .logic.Var

returns

occur_flag – flag ofthe occurance of the variable

rtype

bool

src.fol.logic_ops.subs(exp, target_var, const)

Substitute var = const

Inputs

exp.logic.CLause .logic.Atom .logic.FuncTerm .logic.Const .logic.Var

logical expression atom, clause, or term

target_var.logic.Var

target variable of the substitution

const.logic.Const

constant to be substituted

returns

exp – result of the substitution logical expression atom, clause, or term

rtype

.logic.CLause .logic.Atom .logic.FuncTerm .logic.Const .logic.Var

src.fol.logic_ops.subs_list(exp, theta_list)

src.fol.logic_ops.t_p(clause, facts)

T_p operator limited to clauses with one body atom

Inputs

clause.logic.Clause

clause

factsList[.logic.Atom]

set of facts

returns

S – set of ground atoms entailed by one step forward-chaining inference

rtype

List[.logic.Atom]

src.fol.logic_ops.t_p_n(clause, facts, n)

applying the T_p operator n-times taking union of results

Inputs

clause.logic.Clause

clause

factsList[.logic.Atom]

set of facts

nint

infer step

returns

G – set of ground atoms entailed by ${clause} cup facts$

rtype

Set[.logic.Atom]

src.fol.logic_ops.unify(atoms)

Unification of first-order logic expressions details in [Foundations of Inductive Logic Programming. Nienhuys-Cheng, S.-H. et.al. 1997.]

Inputs

atoms : List[.logic.Atom]

returns

• flag (bool) – unifiable or not

• unifier (List[(.logic.Var, .logic.Const)]) – unifiable - unifier (list of substitutions) not unifiable - empty list

Module contents