Index

_

__call__() (yapsap.substitution.Substitution method)

__init__() (yapsap.substitution.Substitution method) (yapsap.yapsa_prover.YapsaProver method)

A

all_paramodulants_from_clause() (in module yapsap.paramodulation) all_paramodulants_from_list() (in module yapsap.paramodulation)

all_possible_factors() (in module yapsap.factoring) all_possible_reflexivity_resolvents() (in module yapsap.reflexivity_resolution) all_possible_resolvents() (in module yapsap.resolution)

C

clause_length() (in module yapsap.utils)

F

factoring() (in module yapsap.factoring)

G

get_variable_list() (in module yapsap.utils)

I

is_subproposition() (in module yapsap.utils)

is_tautology() (in module yapsap.utils)

M

module yapsap.factoring yapsap.paramodulation yapsap.reflexivity_resolution yapsap.resolution yapsap.substitution yapsap.unification yapsap.utils yapsap.yapsa_prover

most_general_unifier() (in module yapsap.unification)

N

NonUnifiableError

NoSubtermFound

P

paramodulation() (in module yapsap.paramodulation) proof_attempt() (yapsap.yapsa_prover.YapsaProver method)

proof_found (yapsap.yapsa_prover.YapsaProver property) proposition_length() (in module yapsap.utils)

R

reflexivity_resolution() (in module yapsap.reflexivity_resolution) reindex_variables() (in module yapsap.utils)

replace_subterm_by_index() (in module yapsap.utils) resolution() (in module yapsap.resolution)

S

substitute_in_clause() (yapsap.substitution.Substitution method)

Substitution (class in yapsap.substitution) subterm_by_index() (in module yapsap.utils)

T

TermSelfReplace

Y

yapsap.factoring module yapsap.paramodulation module yapsap.reflexivity_resolution module yapsap.resolution module

yapsap.substitution module yapsap.unification module yapsap.utils module yapsap.yapsa_prover module YapsaProver (class in yapsap.yapsa_prover)