Prover#

class tensor_theorem_prover.ResolutionProver(knowledge=None, max_proof_depth=10, max_resolvent_width=None, max_resolution_attempts=None, similarity_func=<function cosine_similarity>, min_similarity_threshold=0.5, cache_similarity=True, skip_seen_resolvents=False, find_highest_similarity_proofs=True, num_workers=None, eval_batch_size=5000)[source]#

Core theorem prover class that uses input resolution to prove a goal

extend_knowledge(knowledge)[source]#: Add more knowledge to the prover

prove(goal, extra_knowledge=None)[source]#: Find the proof for the given goal with highest similarity score

prove_all(goal, extra_knowledge=None, max_proofs=None, skip_seen_resolvents=None)[source]#: Find all possible proofs for the given goal, sorted by similarity score

prove_all_with_stats(goal, extra_knowledge=None, max_proofs=None, skip_seen_resolvents=None)[source]#: Find all possible proofs for the given goal, sorted by similarity score. Return the proofs and the stats for the proof search.

reset()[source]#: Clear all knowledge from the prover and wipe the similarity cache

class tensor_theorem_prover.Proof(goal, similarity, stats, proof_steps, depth, substitutions)[source]#

Respresentation of a successful proof of a goal

depth#

classmethod from_rust(rust_proof)[source]#

goal#

proof_steps#

similarity#

stats#

substitutions#

class tensor_theorem_prover.ProofStep(source, target, source_unification_literal, target_unification_literal, source_substitutions, target_substitutions, resolvent, similarity, running_similarity, depth)[source]#

A single step in a proof of a goal

depth#

classmethod from_rust(rust_proof_step)[source]#

resolvent#

running_similarity#

similarity#

source#

source_substitutions#

source_unification_literal#

target#

target_substitutions#

target_unification_literal#

class tensor_theorem_prover.ProofStats(attempted_resolutions=0, successful_resolutions=0, max_resolvent_width_seen=0, max_depth_seen=0, discarded_proofs=0)[source]#

Stats on how complex a proof was to compute

attempted_resolutions = 0#

discarded_proofs = 0#

classmethod from_rust(rust_proof_stats)[source]#

max_depth_seen = 0#

max_resolvent_width_seen = 0#

successful_resolutions = 0#